ross at soi.city.ac.uk
Mon Dec 19 05:16:03 EST 2005
As a termination test, how about no restrictions on context and head
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.
More information about the Glasgow-haskell-users