Hmm… Seems similar to the ideas in the "Can we make a knob" section from Aaron's post that you linked. But as he said:
But saying that you can never repeat a type within a specialization would be very restrictive.
Also reminds me of Haskell's typeparameter roles, which I compared to Rust's situation recently. In fact, I believe that requiring a particular impl to be "always applicable" is equivalent (in some formal sense) to requiring that all its type parameters be representational (AKA parametric), versus nominal. And putting #[specialization_predicate]
on a trait is equivalent to requiring that its Self 'parameter' is parametric. However, Niko's proposed rules provide more flexibility than Haskell's in some cases, which I think is sound, as I'll describe later.
In both languages, we want a generic definition to stay representationally equivalent if you change one of its parameter between two types/lifetimes that are themselves representationally equivalent. In both languages, there's a specific language feature that provides a "base case" for representational equivalence  if two different struct definitions happen to have the same field types, that doesn't count; we only care about a case where the language guarantees that two types have the same representation.

In Haskell, that's newtype:
newtype A = B
defines a typeA
which is equivalent toB
. The closest Rust equivalent would be something like#[repr(transparent)] struct A(B);
. Importantly, Haskell lets you coerce between any two types with a representational equivalence guarantee. So you can coerce betweenA
andB
, and also betweenFoo A
andFoo B
ifFoo
's parameter is representational. (This was originally an accidental consequence of GeneralizedNewtypeDeriving, but later became an explicit feature.) 
In Rust, that's lifetimes. Trans's blindness to lifetimes effectively allows you to coerce from
Foo<'a>
toFoo<'anonymous>
, though it's not as general as Haskell's coercion mechanism.
So let's look at Haskell's rules for inferring representational versus nominal. To copy and paste from the GHC wiki page:
Next, we descend into each defining equation of the type family and inspect the lefthand and righthand sides. The righthand sides are analyzed just like the fields of a data constructor; see the Role inference section above for more details.
This example isn't on that page, but if you write something like
type family Foo x where
Foo x = Bar x
where Bar
is an existing type family, Foo
's parameter inherits the representational/nominal decision from Bar
. So if Bar
's parameter is nominal, Foo
's parameter is implied to be nominal, and ditto for representational.
This is roughly equivalent to "Condition 1: Relies only on implied bounds." By default, type parameters to Rust traits are nominal (i.e. not required to be parametric), including the Self 'parameter', so adding random trait bounds to an alwaysapplicable impl would force its parameters to be nominal as well, contradicting the requirement that they be representational. But since marking a trait as #[specialization_predicate]
asserts that its Self parameter is representational, it's okay to depend on those.
How is a restriction on bounds equivalent to a restriction on the righthand side? Well, type families aren't the same as traits  they're basically a typetotype lookup table, most directly analogous a trait with one associated type, which happens to be implemented for all types. As it happens, Haskell has a much much closer equivalent of traits, namely typeclasses, and they can even have associated types. But GeneralizedNewtypeDeriving has a blanket ban on typeclasses with associated types, regardless of representationalness, so I can't use those as an example.
But there's a pretty simple transformation to simulate a predicate trait using a type family. This code:
trait SomeTrait {}
impl SomeTrait for isize {}
could be implemented as:
// define two types named True and False
data True
data False
// and the lookup table:
type family IsSomeTraitImplemented x where
IsSomeTraitImplemented Int = True
IsSomeTraitImplemented _ = False
And then if you want to add a "bound",
trait AnotherTrait {}
impl<T> AnotherTrait for T where T: SomeTrait {}
could be
type family IsAnotherTraitImplemented x where
IsAnotherTraitImplemented x = IsSomeTraitImplemented x
(and you could define an "and" combinator if you wanted to simulate multiple bounds, etc.)
So the "bound" T: SomeTrait
turns into a type expression IsSomeTraitImplemented x
on the righthand side.
Anyway, continuing on with the Haskell rules:
The more interesting analysis comes when inspecting the lefthand sides. We want to mark any type variable that is scrutinized as nominal. By "scrutinized", we mean a variable that is being used in a nonparametric fashion. [..]
To accomplish this, we check for any occurences of the either of the following sorts of scrutinization:
[I'm going to quote these out of order:]
Type patterns that are syntactically equal are all marked as nominal. For instance:
type family Eq w x y z where Eq a b (Either b a) c = a
Here, we have two variable names that are used in multiple places:
a
andb
. As a result, the type variables which they inhabit (w
,x
, andy
) are all marked asnominal
.
That's easy: it corresponds to "Condition 3: Each type parameter can only be used once."
A type pattern that is not a single type variable. For instance, all of these equations provde examples of type patterns which do scrutinize a particular type variable:
type family Inspect x where Inspect Int = Bool Inspect (Either a b) = a Inspect (f a) = a
Any type variable that is scrutinized in this fashion (
x
in the above example) is marked asnominal
.
This is the part where Niko's proposed rules are more flexible.
For lifetime parameters, this is covered by "Condition 2: Fully generic with respect to lifetimes." Similarly to how the above disallows Inspect Int = Bool
, using a concrete type where we want a type parameter, an alwaysapplicable impl can't say impl SomeTrait for Foo<'static>
, using a concrete lifetime where we want a lifetime parameter.
But Niko's rules do allow for a more direct equivalent to the above example: we could impl SomeTrait for isize
, and separately impl<A, B> SomeTrait for Either<A, B>
. This is safe, though, and I think it would be safe in Haskell as well  i.e. Haskell is being overly conservative. After all, in both languages we know that Int
and Either a b
cannot possibly be representationally equivalent:
 In Haskell, that's because
Int
is not a newtype ofEither
or vice versa; they are distinct data types. (Though there may be backwardscompatibility concerns, generally speaking, in allowing code to make these kinds of assumptions. It's unlikely thatInt
's implementation would ever be changed into a newtype ofEither
, but you could imagine that happening for other pairs of types...)  In Rust, that's because
isize
andEither<A, B>
are not identical barring lifetimes. (No backwardscompatibiliy concerns here, since there's no newtype feature. Transparent structs don't count, because the type system doesn't treat them specially.)
Therefore, it should be fine for Inspect Int
and Inspect (Either a b)
to also not be representationally equivalent. (edit: but I might be missing something, in which case I’d love to be corrected.)
Is there a point to this post?
Maybe. If Niko's plan is equivalent in some sense to a simplified version of type roles, then that suggests it's on good theoretical ground. And it opens the possibility of moving toward a more fullfeatured version, either now or (more likely) as a backwardscompatible extension.
On the other hand, I'll again quote @glaebhoerl, regarding Haskell type roles:
The opinion of many leading members of the Haskell community is that this solution was illconceived and brings more complexity than it’s worth.
So perhaps, even if they are equivalent, that should be regarded as an unfortunate coincidence rather than a path for future exploration.