relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[Ross Paterson]

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.