src/Symantic/Typer/Eq.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE PolyKinds #-}
   3
   4 module Symantic.Typer.Eq where
   5
   6 import Data.Kind (Type)
   7 import Data.Maybe (Maybe (..))
   8 import Type.Reflection ((:~~:) (..))
   9
  10 class EqTy (x :: xK -> Type) (y :: yK -> Type) where
  11   -- | /Heterogeneous type equality/:
  12   -- return two proofs when two types are equals:
  13   -- one for the type and one for the kind.
  14   eqTy :: x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)