module Language.Symantic.Typing.Kind where
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import qualified Data.Kind as K
import Language.Symantic.Grammar
data Kind src k where
KiType :: src -> Kind src K.Type
KiConstraint :: src -> Kind src K.Constraint
KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb)
infixr 5 `KiFun`
type instance SourceOf (Kind src k) = src
instance Source src => Sourced (Kind src k) where
sourceOf (KiType src) = src
sourceOf (KiConstraint src) = src
sourceOf (KiFun src _a _b) = src
setSource (KiType _loc) src = KiType src
setSource (KiConstraint _loc) src = KiConstraint src
setSource (KiFun _loc a b) src = KiFun src a b
instance Show (Kind src k) where
show KiType{} = "*"
show KiConstraint{} = "Constraint"
show (KiFun _src a b) = "(" ++ show a ++ " -> " ++ show b ++ ")"
instance TestEquality (Kind src) where
testEquality = eqKind
eqKind :: Kind xs x -> Kind ys y -> Maybe (x:~:y)
eqKind KiType{} KiType{} = Just Refl
eqKind KiConstraint{} KiConstraint{} = Just Refl
eqKind (KiFun _xs xa xb) (KiFun _ys ya yb)
| Just Refl <- eqKind xa ya
, Just Refl <- eqKind xb yb
= Just Refl
eqKind _ _ = Nothing
type K (t::kt) = kt
class KindOf (a::kt -> K.Type) where
kindOf :: a t -> Kind (SourceOf (a t)) kt
class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k where
instance (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind k
inj_Kind ::
forall k src.
Source src =>
Inj_Kind k =>
Kind src k
inj_Kind = inj_KindP @(Ty_of_Type k) (noSource @src)
class Inj_KindP k where
inj_KindP :: src -> Kind src (Type_of_Ty k)
instance Inj_KindP K.Constraint where
inj_KindP = KiConstraint
instance Inj_KindP Ty where
inj_KindP = KiType
instance (Inj_KindP a, Inj_KindP b) => Inj_KindP (a -> b) where
inj_KindP src = KiFun src (inj_KindP @a src) (inj_KindP @b src)
data Ty
type family Ty_of_Type (t::K.Type) :: K.Type
type instance Ty_of_Type K.Type = Ty
type instance Ty_of_Type K.Constraint = K.Constraint
type instance Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b
type family Type_of_Ty (t::K.Type) :: K.Type
type instance Type_of_Ty Ty = K.Type
type instance Type_of_Ty K.Constraint = K.Constraint
type instance Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b
data KindK src = forall k. KindK (Kind src k)
instance Eq (KindK src) where
KindK x == KindK y
| Just _ <- eqKind x y = True
_x == _y = False
instance Show (KindK src) where
show (KindK x) = show x
data Con_Kind src
= Con_Kind_Eq (KindK src) (KindK src)
| Con_Kind_Arrow (KindK src)
deriving (Eq, Show)
when_EqKind
:: Inj_Error (Con_Kind src) err
=> Kind src x
-> Kind src y
-> ((x :~: y) -> Either err ret) -> Either err ret
when_EqKind x y k =
case x `eqKind` y of
Just Refl -> k Refl
Nothing -> Left $ inj_Error $ Con_Kind_Eq (KindK x) (KindK y)
when_KiFun ::
Inj_Error (Con_Kind src) err =>
Inj_Source (KindK src) src =>
Kind src x ->
(forall a b. (x :~: (a -> b)) ->
Kind src a ->
Kind src b ->
Either err ret) ->
Either err ret
when_KiFun x k =
case x of
KiFun _src a b -> k Refl (a `source` KindK x) (b `source` KindK x)
_ -> Left $ inj_Error $ Con_Kind_Arrow (KindK x)