termination for FDs and ATs

[Claus Reinke]

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