--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

{-# 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