On Tue, Feb 28, 2006 at 07:53:38PM -0000, Claus Reinke wrote:
class Fail all -- no instances!
class TypeNotEq a b instance Fail a => TypeNotEq a a instance TypeNotEq a b
class Test a b where test :: a -> b -> Bool instance TypeNotEq a b => Test a b where test _ _ = False instance Test a a where test _ _ = True
main = print $ (test True 'c', test True False)
never mind the overlap, the point here is that we redirect from Test a b to TypeNotEq a b, and ghc informs us that the "Constraint is no smaller than the instance head".
it is true that the parameters don't get smaller (same number, same number of constructors, etc.), but they are passed to a "smaller" predicate (in terms of call-graph reachability: there are fewer predicates reachable from TypeNotEq than from Test - in particular, Test is not reachable from TypeNotEq).
Yes, one could waive these restrictions on the constraint and head if they were not part of a cycle. Then when you added an instance that completed a cycle, the restrictions would come into force, on all the instances in the cycle. Non-local criteria are a bit more complex for the programmer, though (ignoring the implementor for the moment). I'll add the possibility to the wiki.
this is a non-local criterion, but a fairly simple one. and it seems very strange to invoke "undecidable instances" for this example (or is there anything undecidable about it?).
Any termination criterion will be necessarily conservative, and will bite in some cases where termination is obvious to the human eye. The question is how far out to push the boundary, trading power for complexity.