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