data EqContext a b = EqContext { safe_coerce :: f(a,b) -> f(b,a) }
I haven't seen the original post, so take the following with a grain of salt. It seems that you are looking for a type that models safe coercions. Here is one, the type a :=: b defined below goes back to Leibniz's principle of substituting equals for equals: in every context `f' you can replace an `a' by a `b'. Cheers, Ralf --- Type equality.
module TypeEq ((:=:), refl, symm, trans, (<>), list, pair, coerce, from, to) where
The type of type equality: |a :=: b| is non-empty iff |a = b|.
newtype a :=: b = Proof { apply :: forall f . f a -> f b }
Equality is reflexive, symmetric, transitive and congruent.
refl :: forall a . a :=: a refl = Proof id
newtype Flip f a b = Flip { unFlip :: f b a }
symm :: forall a b . a :=: b -> b :=: a symm p = unFlip (apply p (Flip refl))
trans :: forall a b c . a :=: b -> b :=: c -> a :=: c trans p q = Proof (apply q . apply p)
(<>) = trans
newtype List f a = List { unList :: f [a] }
list :: a :=: b -> [a] :=: [b] list p = Proof (unList . apply p . List)
newtype Pair1 f b a = Pair1 { unPair1 :: f (a, b)} newtype Pair2 f a b = Pair2 { unPair2 :: f (a, b)}
pair :: a :=: c -> b :=: d -> (a, b) :=: (c, d) pair p1 p2 = Proof (unPair2 . apply p2 . Pair2 . unPair1 . apply p1 . Pair1)
Special casts.
coerce = apply
newtype Id a = Id { unId :: a }
from :: forall a b . a :=: b -> (a -> b) from ep = \ a -> unId (apply ep (Id a))
newtype Inv a b = Inv { unInv :: b -> a }
to :: forall a b . a :=: b -> (b -> a) to ep = unInv (apply ep (Inv id))