Ross, and Martin, Thanks! But I'm not certain that your fix is correct. Let's ask Martin. I've added comments below. | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Ross Paterson | Sent: 06 February 2006 11:36 | To: Simon Peyton-Jones; glasgow-haskell-users@haskell.org | Subject: Re: instance inference | | A patch implementing a relaxed termination constraint is at | | http://www.soi.city.ac.uk/~ross/instance-termination.patch | | Here is the description: | | With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4 | requires that instances be of the following form: | | (1-GHC) each assertion in the context must constrain distinct variables | mentioned in the head, and | | (2-GHC) at least one argument of the head must be a non-variable type. Yes, (1-GHC) certainly contradicts the FD paper that Martin and I wrote. I think (1) should be: (1-fixed) Each assertion in the context must constrain type variables, and those type variables must all be mentioned in the head. That is, there is no requirement that the type variables should be distinct (they can be repeated). But they must all appear in the HEAD. Do you agree, Martin? For example class D a b | a -> b instance C a b b a => D a b where ... is fine. Now, you propose something new and interesting: | This patch replaces these rules with the requirement that each | assertion in the context satisfy | | (1-Ross) no variable has more occurrences in the assertion than in the | head, and | | (2-Ross) the assertion has fewer constructors and variables (taken together | and counting repetitions) than the head. | | This allows all instances permitted by the old rule, plus such | instances as | | instance C a | instance Show (s a) => Show (Sized s a) | instance (Eq a, Show b) => C2 a b | instance C2 Int a => C3 Bool [a] | instance C2 Int a => C3 [a] b | instance C4 a a => C4 [a] [a] | | but still ensures that under any substitution assertions in the context | will be smaller than the head, so context reduction must terminate. Your (1-Ross) ensures that every variable in the assertion does occur in the head. But I'm not sure that the size-reduction argument is watertight in the presence of fundeps. (E.g. in example 15 it *looks* as if the size goes down, but it doesn't.) I bet Martin could tell us if it's watertight though. It certainly looks useful. However, notice that (1-Ross) is more also more restrictive than (1-fixed), because it rules out the C/D example I give above. So is it a win? Simon