[Haskell-cafe] Type constructor variables no longer injective in GHC 7.2.1?

[Daniel Schüssler]

Hello Cafe,

say we take these standard definitions:

> {-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}

> data a :=: b where 
>     Refl :: a :=: a

> subst :: a :=: b -> f a -> f b
> subst Refl = id 

Then this doesn't work (error message at the bottom):

> inj1 :: forall f a b. f a :=: f b -> a :=: b
> inj1 Refl = Refl

But one can still construct it with a trick that Oleg used in the context of 
Leibniz equality:

> type family Arg fa

> type instance Arg (f a) = a

> newtype Helper fa fa' = Helper { runHelper :: Arg fa :=: Arg fa' }

> inj2 :: forall f a b. f a :=: f b -> a :=: b
> inj2 p = runHelper (subst p (Helper Refl :: Helper (f a) (f a)))
                  
So, it seems to me that either rejecting inj1 is a bug (or at least an 
inconvenience), or GHC is for some reason justified in not assuming type 
constructor variables to be injective, and accepting inj2 is a bug. I guess 
it's the former, since type constructor variables can't range over type 
functions AFAIK.

The error message for inj1 is:

    Could not deduce (a ~ b)
    from the context (f a ~ f b)
      bound by a pattern with constructor
                 Refl :: forall a. a :=: a,
               in an equation for `inj1'
      at /tmp/inj.lhs:12:8-11
      `a' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at /tmp/inj.lhs:12:3
      `b' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at /tmp/inj.lhs:12:3
    Expected type: a :=: b
      Actual type: a :=: a
    In the expression: Refl
    In an equation for `inj1': inj1 Refl = Refl


Cheers,
Daniel