termination for FDs and ATs

[Simon Peyton-Jones]

| On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:
| > So the MR raises the reverse
| > question: can you be sure that every tautologous constraint is
reducible?
| 
| I think the answer is no.  Consider:
| 
| 	class C a where
| 		type Result a
| 		method :: a -> Result a
| 
| 	instance C (Maybe a) where {
| 		type Result (Maybe a) = Bool
| 
| 	f = \ b x -> if b then Just (method x) else x
| 
| The AT algorithm will stop after inferring the following type for f:
| 
| 	(a = Maybe (Result a), C a) => Bool -> a -> a
| 
| Since the constraint set is non-empty, this definition will be
rejected
| by the monomorphism restriction.

Actually, it won't.  The spec just says that the function is monomorphic
in 'a'.  That is, 'a' can be instantiated only one way.  So if f is
called, say (f True True), then that fixes 'a' to be Bool and all is
well.  Only if f is exported (with no calls inside the module) will the
program be rejected, and even then it'll be rejected on the grounds that
'a' is ambiguous.

But these are details.  Your general point is well taken: the FD
improvement rule will infer
	f :: Bool -> Bool -> Bool
without seeing any calls.

Simon