{-# LANGUAGE Safe #-}
{-# LANGUAGE GADTs, KindSignatures #-}
module Copilot.Core.Type.Equality
( Equal (..)
, EqualType (..)
, coerce
, refl
, trans
, symm
, cong
) where
data Equal :: * -> * -> * where
Refl :: Equal a a
class EqualType t where
(=~=) :: t a -> t b -> Maybe (Equal a b)
coerce :: Equal a b -> a -> b
coerce :: Equal a b -> a -> b
coerce Equal a b
Refl a
x = a
b
x
refl :: Equal a a
refl :: Equal a a
refl = Equal a a
forall a. Equal a a
Refl
symm :: Equal a b -> Equal b a
symm :: Equal a b -> Equal b a
symm Equal a b
Refl = Equal b a
forall a. Equal a a
Refl
trans :: Equal a b -> Equal b c -> Equal a c
trans :: Equal a b -> Equal b c -> Equal a c
trans Equal a b
Refl Equal b c
Refl = Equal a c
forall a. Equal a a
Refl
cong :: Equal a b -> Equal (f a) (f b)
cong :: Equal a b -> Equal (f a) (f b)
cong Equal a b
Refl = Equal (f a) (f b)
forall a. Equal a a
Refl