{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

-- | Equality of types and witnesses.
module Eq1 where

-- | Equality proof of types.
data (a :=: a') where
  Refl :: a :=: a

-- | Equality type class for type witnesses.
class Eq1 f where
  -- | Returns a proof of equality if the witnesses are equal or Nothing if they are not.
  eq1 :: f a -> f a' -> Maybe (a :=: a')