module Data.Equal where

import Control.Monad
import Data.Type
import Generics.Pointless.Functors

data Equal a b where
    Eq :: Equal a a

teq :: MonadPlus m => Type a -> Type b -> m (Equal a b)
feq :: MonadPlus m => Fctr f -> Fctr g -> m (Equal (Fix f) (Fix g))
coerce :: MonadPlus m => Type a -> Type b -> a -> m b
geq :: Type a -> a -> a -> Bool