{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Safe #-}
module Copilot.Core.Type.Equality
{-# DEPRECATED "This module is deprecated in Copilot 3.12. Use base:Data.Type.Equality instead." #-}
( 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 :: forall a b. Equal a b -> a -> b
coerce Equal a b
Refl a
x = a
x
refl :: Equal a a
refl :: forall a. Equal a a
refl = forall a. Equal a a
Refl
symm :: Equal a b -> Equal b a
symm :: forall a b. Equal a b -> Equal b a
symm Equal a b
Refl = forall a. Equal a a
Refl
trans :: Equal a b -> Equal b c -> Equal a c
trans :: forall a b c. Equal a b -> Equal b c -> Equal a c
trans Equal a b
Refl Equal b c
Refl = forall a. Equal a a
Refl
cong :: Equal a b -> Equal (f a) (f b)
cong :: forall a b (f :: * -> *). Equal a b -> Equal (f a) (f b)
cong Equal a b
Refl = forall a. Equal a a
Refl