%!TEX root = ../Main.tex

\section{Kinds of Types}

\begin{small}
\begin{code}
Inductive KIND : kienv -> ty -> ki -> Prop :=
 | KIConFun
   :  forall ke
   ,  KIND ke (TCon TyConFun) (KFun KStar (KFun KStar KStar))

 | KIConData
   :  forall ke i k
   ,  KIND ke (TCon (TyConData i k)) k

 | KIVar
   :  forall ke i k
   ,  get i ke = Some k
   -> KIND ke (TVar i) k

 | KIForall
   :  forall ke t
   ,  KIND (ke :> KStar) t           KStar
   -> KIND ke            (TForall t) KStar

 | KIApp 
   :  forall ke t1 t2 k11 k12
   ,  KIND ke t1 (KFun k11 k12)
   -> KIND ke t2 k11
   -> KIND ke (TApp t1 t2) k12.
\end{code}
\end{small}
