This has been an interesting thread, starting here http://www.haskell.org//pipermail/haskell-prime/2006-April/001466.html Here is what I conclude so far. 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'. http://www.haskell.org//pipermail/haskell-prime/2006-April/001501.html 2. This solution is not the same as stopping after a fixed number N of iterations. It's more principled than that. 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. 4. As Ross shows below, we may thereby infer a qualified type when there is a unique, completely un-qualified solution. But that does little harm, I think. The only time you can even tell it has happened is if (a) the defn falls under the MR (in particular, no type signature is given), (b) the function is exported, and (c) it is not called inside the module. 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. 6. I don't think we yet know whether *all* non-termination is thereby eliminated from the AT-inference story. Manuel and Martin and I are starting to write down the formal story for an AT system that covers both data types, type synonyms, and various other small extensions to ATs, so we hope to find out soon. (In this world, "small extensions" are easy to describe, but sometimes have a big effect. So formalising it is important.) 7. In particular, Martin writes "We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs." But so far I don't see why we might need a more clever analysis than the rule I describe in (1) above. I'm not denying that such a thing might exist, but I wonder if you have anything in mind? http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html Simon | -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of | Ross Paterson | Sent: 03 May 2006 09:37 | To: haskell-prime@haskell.org | Subject: Re: termination for FDs and ATs | | On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote: | > So the MR raises the reverse | > question: can you be sure that every tautologous constraint is reducible? | | I think the answer is no. Consider: | | class C a where | type Result a | method :: a -> Result a | | instance C (Maybe a) where { | type Result (Maybe a) = Bool | | f = \ b x -> if b then Just (method x) else x | | The AT algorithm will stop after inferring the following type for f: | | (a = Maybe (Result a), C a) => Bool -> a -> a | | Since the constraint set is non-empty, this definition will be rejected | by the monomorphism restriction. | | However, this constraint set has exactly the same set of solutions as | a = Maybe Bool, which is trivially solvable. (The corresponding FD | version will reduce to this, thanks to instance improvement.) | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://haskell.org/mailman/listinfo/haskell-prime