ref: ac0c51a3279123d2a911e918cb87e8151a529c1a
dir: /lib/Data/Type/Equality.hs/
module Data.Type.Equality(module Data.Type.Equality) where import Prelude data a :~: b = (a ~ b) => Refl instance forall a b . Eq (a :~: b) where Refl == Refl = True instance forall a b . Show (a :~: b) where show Refl = "Refl" sym :: forall a b . (a :~: b) -> (b :~: a) sym Refl = Refl trans :: forall a b c . (a :~: b) -> (b :~: c) -> (a :~: c) trans Refl Refl = Refl castWith :: forall a b . (a :~: b) -> a -> b castWith Refl x = x -- Problem: :~: is not polykinded --apply :: forall (f :: Type -> Type) (g :: Type -> Type) a b . (f :~: g) -> (a :~: b) -> (f a :~: g b) --apply Refl Refl = Refl