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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
