So, the condition that was supposed to ensure termination in my previous post is most certainly wrong. The idea was to prevent tautological impls like the following:
impl<A: Foo> A: Foo { ... }
Such impls, given a naive algorithm, would loop infinitely trying to
decide if a type T
implemented Foo
. You can imagine: it would
ask, does `T` implement `Foo`? Well, if I map `A` to `T` then this
impl applies, but only if `T` implements `Foo`. Hmm. That puts me
back where I started from. Oh well, better try it again!
Obviously a
less naive algorithm could keep a stack and then fail to execute, but
it was precisely the logic of this stack that I was trying to capture
in that restriction.
Just as obviously, the restriction I proposed is insufficient. One could write:
impl<A: Bar> A: Foo { ... }
impl<A: Foo> A: Bar { ... }
This leads to the same scenario but violates no restriction.
Anyway, there are no conclusions in this post. Just some intermediate thoughts along the way I wanted to jot down.
What is the algorithm, anyway?
In its full gory detail, the naive algorithm is something like this:
fn Implements(Tr, N, Tn*) > bool
:Does the type `Tr` implement `N
`? If so, here is the impl that proves it  Here I am ignoring type parameters and trait instances
 Is
Tr <: N<Tn*>
?  Then
Tr
is a trait instance  Does
N
refer to theself
type in a method parameter or return type? No: return true > Note: in the future, we could allow it in the case where it appears only in return types by wrapping the return value
 Is
Tr
a bounded parameter type?  Is
N<Tn*>
(or a subtype ofN<Tn*>
) among the bounds? Yes: return true
 For each impl
Impl = impl<VD*> Ts: M<Tm*>
:  Is there a substitution
S
for the variables declared inVD*
such thatTr <: S Ts
andN<Tn*> <: M<S Tm*>
? For each variable declaration
VD = X: M<...>*
:  Let
Ta = S X
be the type inferred for this variable  For each of the bounds
M<Tb*>
inVD
:Implements(Ta, M, S Tb*)
? No: return false
 return true
 For each variable declaration
You can more or less ignore the first two cases and force on the final
one. Also, here I am assuming another requirement that I forgot to
write down in my previous post: all instance variables declared on an
impl must appear in either the self type, the trait type, or both.
That ensures that we can use inference to find the substitution S
.
Clearly the dangerous case for termination is the recursive call to
Implements()
that occurs when checking the bounds. We must somehow
guarantee that this call will not itself generate an infinite number
of subcalls.
Simple technique for termination
One simple condition that guarantees termination is to require that the variables declared on the impl appear within the self type (not as the self type, as in these examples). That means that these impls would be fine:
1 2 3 

But the following impls are illegal because the type variable X
is
not a part of the self type:
1 2 3 4 

Given this requirement, one can make an inductive argument based on
the depth of the receiver type Tr
. If Tr
has depth 1 (such as
with the type int
), then the impl can take no type parameters, so
there are no recursive calls. In every other case, the recursive call
occurs on the value of some type variable, the depth of the type bound
to each type variable is always less than the self type, hence they
hold by the inductive hypothesis.
This is in fact very similar to
the requirement that is used in Haskell 98, which requires
that all variables in the instance assertion
must appear in the
instance head
. GHC now supports a flag XFlexibleContexts
to
loosen this rule. It then imposes some, well, different constraints.
Haskell’s rules
Given the XFlexibleContexts
flag, Haskell imposes what it calls the
Paterson Conditions (there is one other set of conditions as well that
have to do with functional dependencies):
 For each assertion in the context
 No type variable has more occurrences in the assertion than in the head
 The assertion has fewer constructors and variables (taken together and counting repetitions) than the head
I can vaguely imagine the inductive hypothesis that these conditions are enforcing, but I don’t yet have a real understanding of these rules, and certainly not any sort of intuitive feeling. I’ll write another post once I’ve grokked this better. I think I’ve exceeded my quota for thinking about this at the moment.