module DDC.Type.Check
(
checkType
, kindOfType
, takeSortOfKiCon
, kindOfTwCon
, kindOfTcCon
, Error(..))
where
import DDC.Type.Check.CheckError
import DDC.Type.Check.CheckCon
import DDC.Type.Compounds
import DDC.Type.Predicates
import DDC.Type.Transform.LiftT
import DDC.Type.Exp
import DDC.Base.Pretty
import Data.List
import Control.Monad
import DDC.Type.Check.Monad (throw, result)
import DDC.Type.Pretty ()
import DDC.Type.Env (Env)
import qualified DDC.Type.Sum as TS
import qualified DDC.Type.Env as Env
import qualified DDC.Type.Check.Monad as G
type CheckM n = G.CheckM (Error n)
checkType :: (Ord n, Pretty n) => Env n -> Type n -> Either (Error n) (Kind n)
checkType env tt = result $ checkTypeM env tt
kindOfType :: (Ord n, Pretty n) => Type n -> Either (Error n) (Kind n)
kindOfType tt = result $ checkTypeM Env.empty tt
checkTypeM :: (Ord n, Pretty n) => Env n -> Type n -> CheckM n (Kind n)
checkTypeM env tt
=
checkTypeM' env tt
checkTypeM' env (TVar u)
= do let tBound = typeOfBound u
let mtEnv = Env.lookup u env
let mkResult
| Just tEnv <- mtEnv
, isBot tBound
= return tEnv
| Just tEnv <- mtEnv
, UIx i _ <- u
, tBound == liftT (i + 1) tEnv
= return tBound
| Just tEnv <- mtEnv
, tBound == tEnv
= return tBound
| Just tEnv <- mtEnv
= throw $ ErrorVarAnnotMismatch u tEnv
| _ <- mtEnv
= throw $ ErrorUndefined u
mkResult
checkTypeM' _env tt@(TCon tc)
= case tc of
TyConSort _ -> throw $ ErrorNakedSort tt
TyConKind kc
-> case takeSortOfKiCon kc of
Just s -> return s
Nothing -> throw $ ErrorUnappliedKindFun
TyConWitness tcw -> return $ kindOfTwCon tcw
TyConSpec tcc -> return $ kindOfTcCon tcc
TyConBound u -> return $ typeOfBound u
checkTypeM' env tt@(TForall b1 t2)
= do _ <- checkTypeM env (typeOfBind b1)
k2 <- checkTypeM (Env.extend b1 env) t2
when ( (not $ isDataKind k2)
&& (not $ isWitnessKind k2))
$ throw $ ErrorForallKindInvalid tt t2 k2
return k2
checkTypeM' env (TApp (TApp (TCon (TyConKind KiConFun)) k1) k2)
= do _ <- checkTypeM env k1
s2 <- checkTypeM env k2
return s2
checkTypeM' env tt@(TApp (TApp (TCon (TyConWitness TwConImpl)) t1) t2)
= do k1 <- checkTypeM env t1
k2 <- checkTypeM env t2
if isWitnessKind k1 && isWitnessKind k2
then return kWitness
else if isWitnessKind k1 && isDataKind k2
then return kData
else throw $ ErrorWitnessImplInvalid tt t1 k1 t2 k2
checkTypeM' env tt@(TApp t1 t2)
= do k1 <- checkTypeM env t1
k2 <- checkTypeM env t2
case k1 of
TApp (TApp (TCon (TyConKind KiConFun)) k11) k12
| k11 == k2 -> return k12
| otherwise -> throw $ ErrorAppArgMismatch tt k1 k2
_ -> throw $ ErrorAppNotFun tt t1 k1 t2 k2
checkTypeM' env (TSum ts)
= do ks <- mapM (checkTypeM env) $ TS.toList ts
k <- case nub ks of
[] -> return $ TS.kindOfSum ts
[k] -> return k
_ -> throw $ ErrorSumKindMismatch
(TS.kindOfSum ts) ts ks
if (k == kEffect || k == kClosure)
then return k
else throw $ ErrorSumKindInvalid ts k