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

module Symantic.Typer.Eq where

import Data.Kind (Type)
import Data.Maybe (Maybe (..))
import Type.Reflection ((:~~:) (..))

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 :: x (xT :: xK) -> y (yT :: yK) -> Maybe (xT :~~: yT)