{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}

module Symantic.Typer.Eq where

import Data.Kind (Type)
import Data.Maybe (Maybe (..))
import GHC.Stack (HasCallStack)
import Type.Reflection (TypeRep, eqTypeRep, (:~~:) (..))

class EqTy (x :: xK -> Type) (y :: yK -> Type) where
  -- | /Heterogeneous type equality/:
  -- return two proofs when two types are equals:
  -- one for the type and one for the kind.
  eqTy :: HasCallStack => x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)
instance EqTy TypeRep TypeRep where
  eqTy = eqTypeRep