I'm not sure whether it is a bug, but there have been two recent reports of ghc-7.2.1 not treating type constructor variables as injective. First, by Daniel Schüssler,

{-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}
module DTest where

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)))

{-
DTest.hs:13:13:
    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 DTest.hs:13:6-9
      `a' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
      `b' is a rigid type variable bound by
          the type signature for inj1 :: (f a :=: f b) -> a :=: b
          at DTest.hs:13:1
    Expected type: a :=: b
      Actual type: a :=: a
    In the expression: Refl
    In an equation for `inj1': inj1 Refl = Refl
-}

compiles fine with ghc-7.0.4. Second, by Sjoerd Visscher,

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

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

{-
STest.hs:12:32:
    Could not deduce (a1 ~ a)
    from the context (Monad m)
      bound by the instance declaration at STest.hs:11:10-59
    or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
      bound by a pattern with constructor
                 CatchError :: forall (m :: * -> *) e a.
                               (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
               in an equation for `fin'
      at STest.hs:12:8-19
      `a1' is a rigid type variable bound by
           a pattern with constructor
             CatchError :: forall (m :: * -> *) e a.
                           (e -> m a) -> ErrorEff ((e -> m a) -> m a) m,
           in an equation for `fin'
           at STest.hs:12:8
      `a' is a rigid type variable bound by
          the instance declaration at STest.hs:11:46
    Expected type: e1 -> m a1
      Actual type: e -> m a
    In the first argument of `f', namely `h'
    In the expression: f h
-}

also compiles fine with 7.0.4. ghc-7.3.20111026 behaves like 7.2.1. Which version behaves correctly?