Why does GHC think that this type variable is not injective?

Question

I have this piece of code:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

This doesn't compile, with this type error in the last line:

Could not deduce (a1 ~ a)
from the context (Monad m)
[...]
or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
[...]

If I change m to [] it compiles fine, so apparently GHC thinks that m is not injective. (Although it doesn't warn about injectivity like it does with type families.)

My version of GHC is 7.2.1.

Edit: If I change (e -> m a) to e it works, if I change it to m a it doesn't, and neither for (m a -> e).

Answer 1

It's not exactly a bug, but it is a long story...

The Story

In 7.0 there used to be a coercion constructor called right which worked like this:

g : f a ~ f b
---------------
right g : a ~ b

That is, if g is a coercion between f a and f b, then right g is a coercion between a and b. This is only sound if f is guaranteed to be injective: otherwise we might legitimately have, say, f Int ~ f Char and then we would be able to conclude Int ~ Char, which would be Bad.

But of course, type synonyms and type families are not necessarily injective; for example:

type T a = Int

type family F a :: *
type instance F Int  = Bool
type instance F Char = Bool 

So how is this guarantee possible? Well, this is precisely the reason why partial applications of type synonyms and type families are not allowed. Partial applications of type synonyms and type families may not be injective, but saturated applications (even ones which result in a higher kind) always are.

Of course, the restriction on partial applications is annoying. So in 7.2, in an attempt to move in the direction of allowing partial application (and because it simplifies the theory and implementation of the coercion language), the right constructor was replaced by a constructor nth, with the accompanying rule

g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi

That is, nth only applies to a coercion g which is between two types which are known to be saturated applications of a type constructor T. In theory, this allows for partial applications of type synonyms and families, because we cannot decompose equalities until we know that they are between applications of a (necessarily injective) type constructor. In particular, nth does not apply to a coercion f a ~ f b because f is a type variable, not a type constructor.

It was thought at the time of the change that no one would really notice, but obviously this was wrong!

Interestingly, the Olegian trick outlined in the haskell-cafe message from Daniel Schüssler shows that the implementation of type families was not changed accordingly! The problem is that a definition like

type family Arg fa
type instance Arg (f a) = a

should not be allowed if f could be non-injective; in that case the definition does not even make sense.

Next Steps

I think the right thing to do is to reinstate right (or something equivalent), since people clearly want it! Hopefully this will be done soon.

In the meantime, it would still be really cool to allow partially applied type synonyms and families. It seems the Right Way (tm) to do that would be to track injectivity in the kind system: that is, each arrow kind would be annotated with its injectivity. This way when encountering an equality f a ~ f b we could look at the kind of f to determine whether it is safe to decompose it into the equality a ~ b. Not coincidentally, I am currently trying to work out the design of such a system. =)

Answer 2

I'm not sure about the cause, but I reduced your testcase to:

{-# LANGUAGE GADTs #-}

data ErrorEff x where
  CatchError :: m a -> ErrorEff (m a)

fin :: ErrorEff (m a) -> m a
fin (CatchError h) = h

which compiles in GHC 7.0.3 but not 7.3.20111021.

This is definitely a compiler bug.

It compiles after changing:

data ErrorEff x where
  CatchError :: x -> ErrorEff x

And the function "fin" can be recovered with record syntax:

data ErrorEff x where
  CatchError :: { fin :: m a } -> ErrorEff (m a)