fundeps for extended Monad definition

[Simon Peyton-Jones]

Interesting example

| class Monad2 m a ma | m a -> ma, ma -> m a where
|   return2 :: a -> ma
|   bind2   :: Monad2 m b mb =3D> ma -> (a -> mb) -> mb
|   _unused :: m a -> ()
|   _unused  =3D \_  -> ()

| instance Monad2 [] a [a] where
|	bind2 =3D error "urk"

The functional dependencies say=20
	m a -> ma

Instantiating this with the instance declaration
	instance Monad2 [] a [a]
we can deduce that
	given any constraint (Monad2 t1 t2 t3),
	if t1 =3D [], then t3 must be [t2]

In the instance declaration, we instantiate the type of bind2 to get
the type of bind2 needed for this particular instance declaration:

	bind2 :: forall b mb. Monad2 [] b mb =3D> ma -> (a -> mb) -> mb

Now the rule above says "that means mb must be [b]" and that gives rise
to the error.
GHC is consistent about this --- if you don't supply an defn for bind2,
it makes one up, and complains in more or less the same way.


Here's a less complicated variant of the same problem:

	class C a b | a -> b where {}

	instance C Int Int where {}

	f :: (C Int b) =3D> Int -> b
	f x =3D x

Is the defn of f legal?  Both GHC and Hugs reject it because the
inferred type of f is more like
	C Int Int =3D> Int -> Int
Functional dependencies tell us that 'b' must be Int, so in fact the two
types are equivalent.  In this example the programmer could write the
'correct' type, but in your case you can't because the type signature
arises by instantiating the one in the class declaration.


I'm really not sure what to do about this.  GHC has an excellent way of
keeping me honest in type-checking: the type checker has to produce a
translation of the program into the (typed) core language.  What could
f's translation look like.  It must presumably be
	f (d::C Int Int) (x::Int) =3D x
giving f the type
	f :: C Int Int -> Int -> Int

Another translation could be
	f  b (d::C Int b) (x::Int) =3D x
(the 'b' is a type variable, a big-lambda binding)  giving f the type
	f :: forall b. C Int b -> Int -> Int

But what I *cannot* get is the type
	f : forall b. C Int b -> Int -> b
how could I write the term?
	f b (d:: C Int b) (x::Int) =3D ?????

I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
saying "in every call to f, b will be Int, so we know that the coercion
is safe".  But that is a scarily global property.  For example, if a
call site of f does not "see" the instance declaration, it might call f
with an argument of type (C Int Bool) or something.  Nor can I see an
easy way to insert the 'right' coercions in general.


Bottom line: excellent point, but I can't see how to fix it.  Maybe
there are some fundep experts out there who can guide us through the
swamp? =20

Simon