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
On Mon, Feb 06, 2006 at 11:53:17AM -0000, Simon Peyton-Jones wrote:
Thanks! But I'm not certain that your fix is correct. Let's ask Martin. I've added comments below.
[...]
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.
Ah, but you added the no-repetition requirement a few weeks ago in response to the example class C a b instance C b b => C (Maybe a) b
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.)
Hmm, "improvement". But this is a problem for the GHC rules too, isn't it?
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?
It might be possible to do slightly better, but only if the assertion with repeated variables is for the same class as in the head. Otherwise we'd need to consider several instances together.
On Mon, Feb 06, 2006 at 12:07:54PM +0000, Ross Paterson wrote:
On Mon, Feb 06, 2006 at 11:53:17AM -0000, Simon Peyton-Jones wrote:
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.)
Hmm, "improvement". But this is a problem for the GHC rules too, isn't it?
Sorry, wrong example (I was thinking of example 6). Example 15 would be ruled out, as the proposed rules ignore functional dependencies. I think this is a bug in GHC, and have already filed it as #681.
participants (2)
-
Ross Paterson -
Simon Peyton-Jones