shithub: MicroHs

ref: 63919e14c893dd09c3dc6ac6211becb794cfa9be
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