see also: http://www.haskell.org//pipermail/haskell-prime/2006-March/000847.html
1. As Manuel explained, in the AT formulation it's possible to avoid non-termination by suspending (leave unsolved) any equality constraint of form (a = ty) where 'a' appears free in a type argument to an associated type in 'ty'.
as both Manuel and myself have pointed out, ensuring that the occurs check covers type-functions as well is not only possible, but implied by working on top of an HM type-system. whether to leave open constraints that run foul of this check, or whether to reject them early, knowing that they can't be fulfilled, is a separate matter. as Manuel explained, the AT system leaves them open because the unification is semantic, ie. further reduction of the type-functions in such equations might eliminate the recursive variable references. as long as the type-functions remain open, the system cannot know whether the constraints can be fulfilled (analogously for an FD system).
2. This solution is not the same as stopping after a fixed number N of iterations. It's more principled than that.
indeed.
3. We may thereby infer a type that can never be satisfied, so that the function cannot be called. (In Martin's vocabulary, "the constraints are inconsistent".) Not detecting the inconsistency immediately means that error messages may be postponed. Adding a type signature would fix the problem, though.
see above. forcing the type by a signature closes the set of type function definitions that may be used (further extension is possible, but not visible at the point of the signature), by which means delayed constraints may be turned into errors (but note that without the signature/MR, there might not be any error, just some type-function definition not yet visible).
5. The effect is akin to dropping the instance-improvement CHR arising from the corresponding FD. But we can't drop the instance-improvement CHR because then lots of essential improvement would fail to take place. It is not obvious to me how to translate the rule I give in (1) into the CHR framework, though doubtless it is possible.
the effect is that of conditionally disabling the instance-improvement CHR, not dropping it completely. improvement CHR introduce unifications, and HM implies that unifications are guarded by occurs-checks, so the CHRs for improvement should be guarded by occurs-checks. that should disable these CHR in the same cases in which the occurs-check disables the type-functions in the AT case. note that the FD-CHR for the class also introduce a unification, hence need to be guarded the same way. cheers, claus