# Termination of trait matching

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<Tn*>`

? 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 the`self`

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

- Then
- Is
`Tr`

a bounded parameter type?- Is
`N<Tn*>`

(or a subtype of`N<Tn*>`

) among the bounds?- Yes: return true

- Is
- For each impl
`Impl = impl<VD*> Ts: M<Tm*>`

:- Is there a substitution
`S`

for the variables declared in`VD*`

such that`Tr <: S Ts`

and`N<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*>`

in`VD`

:`Implements(Ta, M, S Tb*)`

?- No: return false

- return true

- Let

- For each variable declaration

- Is there a substitution

- “Does the type

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:

```
impl<X: ...> Foo<X>: N<...> { ... }
impl<X: ...> ~[X]: N<...> { ... }
impl<X: ...> @X: N<...> { ... }
```

But the following impls are illegal because the type variable `X`

is
not a part of the self type:

```
// Here X *is* the self type, not a *part* of it:
impl<X: N<...>> X: N<...> { ... }
// Here X *is* just unrelated to the type `int`:
impl<X: N<...>> int: N<...> { ... }
```

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.