termination for FDs and ATs

[Manuel M T Chakravarty]

Ross Paterson:
> On Thu, Apr 27, 2006 at 12:40:47PM +0800, Martin Sulzmann wrote:
> > Yes, FDs and ATs have the exact same problems when it comes to termination.
> > The difference is that ATs impose a dynamic check (the occurs check)
> > when performing type inference (fyi, such a dynamic check is sketched
> > in a TR version of the FD-CHR paper).
> 
> Isn't an occurs check unsafe when the term contains functions (type
> synonyms)?  You might reject something that would have been accepted
> if the function had been reduced and discarded the problematic subterm.

We account for that, but before explaining how, please let me emphasis
that the occurs check is not something newly introduced with ATs, it's
already part of plain HM type inference - it's just that it gets more
interesting with ATs.  Hence, I don't agree with Martin's comparison to
FD type inference, where people are discussing "new" dynamic checks.

Now, concerning ATs, the interesting rules is (var_U) of Fig 5 of  
"Associated Type Synonyms" <http://www.cse.unsw.edu.au/~chak/papers/CKP05.html>
All this rule says is that, given an equality of the form

  a = t

we cannot simplify this to the substitution [t/a] iff a \in FV(t).
However, it does *not* say that we have to reject the program at this
point.

If t does not contain any type functions, then we can indeed reject the
program, as the equality cannot be satisfied.  However, as you rightly
point out, this is not generally the case in the presence of type
functions; eg, (a = t) could be equivalent to (a = S a) and we might
have a definition for S reading

  S Int = Int

Then, if a is at some point instantiated to Int, the equality obviously
holds.  In other words, if we have (a = t) with a \in FV(t) and the
occurrence of a in t is below a type function, we don't know yet whether
or not to reject the program.

It is no problem to account for this uncertainty in AT type inference.
The crucial difference between AT type inference and inference for
vanilla type classes is that the constraint context includes equalities
in addition to class predicates; ie, whenever we come across an equality
t1 = t2 that we cannot solve yet (by unification), we put it into the
constraint context.  It may be solved later after some more
substitutions have been applied.  If not, it may end up in the signature
of whatever binding we are currently typing (during generalisation).

Manuel