termination for FDs and ATs

[Manuel M T Chakravarty]

Ross Paterson:
> To ensure termination with FDs, there is a proposed restriction that
> an instance that violates the coverage condition must have a trivial
> instance improvement rule.  Is the corresponding restriction also
> required for ATs, namely that an associated type synonym definition
> may only contain another associated type synonym at the outermost
> level?  If not, wouldn't the non-terminating example from the FD-CHR
> paper (ex. 6, adapted below) also be a problem for ATs?
> 
> 	class Mul a b where
> 		type Result a b
> 		(.*.) :: a -> b -> Result a b
> 
> 	instance Mul a b => Mul a [b] where
> 		type Result a b = [Result a b]
> 		x .*. ys = map (x .*.) ys
> 
> 	f = \ b x y -> if b then x .*. [y] else y

This definition is not quite correct.  The instance would be

  	instance Mul a b => Mul a [b] where
		type Result a [b] = [Result a b]   -- second argument is different
		x .*. ys = map (x .*.) ys

The arguments to the ATs, in an instance def, need to coincide with the
class parameters.

So, in f, we get the context

  Mul a [b], Result a [b] = b                       (*)

which reduces to

  Mul a b, [Result a b] = b

at which point type inference *terminates*.

So, we get the following type for f

  f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b]

Given the instance definitions of that example, you can never satisfy
the equality [Result a b] = b, and hence, never apply the function f.

In other words, AT type inference sidesteps the problem by just not
committing on whether f's type is satisfiable.  It rather gives a
condition under which f can be applied, namely [Result a b] = b.  That
condition will then be checked at any application site.

So, clearly termination for ATs and FDs is *not* the same.  It's quite
interesting to have a close look at where the difference comes from.
The FD context corresponding to (*) above is

  Mul a [b] b

Improvement gives us

  Mul a [[c]] [c] with b = [c]

which simplifies to 

  Mul a [c] c

which is where we loop.  The culprit is really the new type variable c,
which we introduce to represent the "result" of the type function
encoded by the type relation Mul.  So, this type variable is an artifact
of the relational encoding of what really is a function, which brings me
back to my fundamental objection to FDs: We are functional, not logic
programmers.

Manuel