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

Simon Peyton-Jones simonpj at
Wed Mar 1 03:32:14 EST 2006


I urge you to read our paper "Understanding functional dependencies via
Constraint Handling Rules", which you can find here

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.


| -----Original Message-----
| From: Claus Reinke [mailto:claus.reinke at]
| Sent: 28 February 2006 19:54
| To: Simon Peyton-Jones; haskell-prime at
| Subject: relaxed instance rules spec (was: the MPTC Dilemma (please
| >The specification is here:
| 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
|     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
|     call, subject to the very same FD, if that recursive call complies
|     with the (recursive) coverage criterion. in fact, for this
|     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

More information about the Haskell-prime mailing list