cvs commit: fptools/ghc/compiler/typecheck TcMonad.lhs TcSimp lify.lhs fptools/ghc/compiler/types FunDeps.lhs Unify.lhs

Simon Peyton-Jones simonpj@microsoft.com
Tue, 30 Jan 2001 07:04:29 -0800


| Unfortunately this is not accepted:
| 
| class C a b | a -> b
| instance C Char b => C Int b
| instance C Char Bool
| 
| The first instance alone is accepted, which is great, but adding the
| second is an error.

I'm really not sure how to solve this.   Consider

	class C a b | a -> b { op :: a -> b -> Int }
	instance C Char Bool 

Now is this ok?

	f :: forall b. C Char b => Char -> b -> Int
	f x y = op x y

Mark J says yes, that's a principlal type for f.  But I just don't know
how to implement the test.  I instantiate op to get the constraint
	C Char b
then I improve to get (C Char Bool).  And now it looks as if the
type signature variable 'b' has been constrained.  

I can't omit improvement when checking against signatures, because
it may be essential to make the signature match.

Furthermore, suppose I could figure out that actually the type
	f :: C Char Bool => Char -> Bool -> Int
is also principal for f, or even perhaps
	f :: Char -> Bool -> Int

Even if I could conclude that these types are also principal,
their calling convention differs (esp in a typed intermediate language).
This is bad: in the case of polymorphic recursion and instance
decls I use the signature to determine the calling convention, so
I just give it a different type after all.


So I just don't know how to fix this in a way that is not too gruesome 
to implement.

Simon