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

[Claus Reinke]

>The specification is here:
>http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions.html#instance-decls

two questions/suggestions about this:

1. there are other termination criteria one migh think of, though
    many will be out because they are not easy to specify. but here
    is an annoyingly simple example that doesn't fit the current rules 
    even though it is clearly terminating (it's not even recursive):

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).

    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?).

2. the coverage condition only refers to the instance head. this
    excludes programs such as good old record selection (which
    should terminate because it recurses over finite types, and is
    confluent -in fact deterministic- because of best-fit overlap    
    resolution):

-- | field selection
infixl #?

class Select label val rec | label rec -> val where
  (#?) :: rec -> label -> val

instance Select label val ((label,val),r) where
  ((_,val),_) #? label = val

instance Select label val r => Select label val (l,r) where
  (_,r)       #? label = r #? label

    now, it is true that in the second instance declaration, "val" is 
    not covered in {label,(l,r)}. however, it is covered in the recursive
    call, subject to the very same FD, if that recursive call complies 
    with the (recursive) coverage criterion. in fact, for this particular
    task, that is the only place where it could be covered.

    would it be terribly difficult to take such indirect coverage (via
    the instance constraints) into account? there'd be no search 
    involved (the usual argument against looking at the constraints),
    and it seems strange to exclude such straightforward "consume
    a type" recursions, doesn't it?

cheers,
claus