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 GHC.Stack (HasCallStack)
   9 import Type.Reflection (TypeRep, eqTypeRep, (:~~:) (..))
  10
  11 class EqTy (x :: xK -> Type) (y :: yK -> Type) where
  12   -- | /Heterogeneous type equality/:
  13   -- return two proofs when two types are equals:
  14   -- one for the type and one for the kind.
  15   eqTy :: HasCallStack => x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)
  16 instance EqTy TypeRep TypeRep where
  17   eqTy = eqTypeRep