Martin Sulzmann is the world expert on this stuff. Maybe he'll know. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Ross Paterson | Sent: 19 December 2005 10:16 | To: Simon Peyton-Jones | Cc: glasgow-haskell-users@haskell.org | Subject: Re: instance inference | | As a termination test, how about no restrictions on context and head | except: | | Each assertion in the context must satisfy | * the variables of the assertion are a sub-multiset of those of the | head (though they may be the same), and | * the assertion has fewer type constructors and variables (taken | together and counting repetitions) than the head. | | This ensures that under any ground substitution the context assertion has | fewer type constructors than the head. | | It would accept all instances accepted by the current test, plus | | instance C a | instance C (s a) => C (Sized s a) | instance (C1 a, C2 b) => C a b | instance C1 Int a => C2 Bool [a] | instance C1 Int a => C2 [a] b | instance C a a => C [a] [a] | | But not things like | | instance (C1 a, C2 a, C3 a) => C a | | because that would need to check other instances as well. | | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users