shithub: MicroHs

ref: b4a7a0d4c04ad0fb96d0b279d35da2658d58a0e1
dir: /lib/Data/Type/Equality.hs/

View raw version 
module Data.Type.Equality(module Data.Type.Equality) where
import Prelude(); import MiniPrelude

type (:~:) :: forall k . k -> k -> Type
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

apply :: forall f g a b . (f :~: g) -> (a :~: b) -> (f a :~: g b)
apply Refl Refl = Refl