http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extension s.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
Claus, I urge you to read our paper "Understanding functional dependencies via Constraint Handling Rules", which you can find here http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/. It will tell you more than you want to know about why relaxing apparently-conservative rules is entirely non-trivial. It's one of those areas in which it is easy to suggest a plausible-sounding alternative, but much harder to either prove or disprove whether the alternative a sound one. The paper describes rules we are reasonably sure of. It would be great to relax those rules. But you do need to have a proof that the relaxation preserves the properties we want. Go right ahead! The paper provides a good framework for such work, I think. Simon | -----Original Message----- | From: Claus Reinke [mailto:claus.reinke@talk21.com] | Sent: 28 February 2006 19:54 | To: Simon Peyton-Jones; haskell-prime@haskell.org | Subject: relaxed instance rules spec (was: the MPTC Dilemma (please solve)) | | >The specification is here: | 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