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