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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
