X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FLanguage%2FCore%2FCheck.hs;fp=utils%2Fext-core%2FLanguage%2FCore%2FCheck.hs;h=db156018230701bbb522b17821b70245172c87fc;hp=0000000000000000000000000000000000000000;hb=b84b5969798530dbf5be9b8bb795b77e5dfbf042;hpb=70f16d3fb8f21fbd198151d59c4ab29023dd9fda diff --git a/utils/ext-core/Language/Core/Check.hs b/utils/ext-core/Language/Core/Check.hs new file mode 100644 index 0000000..db15601 --- /dev/null +++ b/utils/ext-core/Language/Core/Check.hs @@ -0,0 +1,668 @@ +{-# OPTIONS -Wall -fno-warn-name-shadowing #-} +module Language.Core.Check( + checkModule, envsModule, + checkExpr, checkType, + primCoercionError, + Menv, Venv, Tvenv, Envs(..), + CheckRes(..), splitTy, substl) where + +import Language.Core.Core +import Language.Core.Printer() +import Language.Core.PrimEnv +import Language.Core.Env + +import Control.Monad.Reader +import Data.List +import Data.Maybe + +{- Checking is done in a simple error monad. In addition to + allowing errors to be captured, this makes it easy to guarantee + that checking itself has been completed for an entire module. -} + +{- We use the Reader monad transformer in order to thread the + top-level module name throughout the computation simply. + This is so that checkExp can also be an entry point (we call it + from Prep.) -} +data CheckRes a = OkC a | FailC String +type CheckResult a = ReaderT (AnMname, Menv) CheckRes a +getMname :: CheckResult AnMname +getMname = ask >>= (return . fst) +getGlobalEnv :: CheckResult Menv +getGlobalEnv = ask >>= (return . snd) + +instance Monad CheckRes where + OkC a >>= k = k a + FailC s >>= _ = fail s + return = OkC + fail = FailC + +require :: Bool -> String -> CheckResult () +require False s = fail s +require True _ = return () + +{- Environments. -} +type Tvenv = Env Tvar Kind -- type variables (local only) +type Tcenv = Env Tcon KindOrCoercion -- type constructors +type Cenv = Env Dcon Ty -- data constructors +type Venv = Env Var Ty -- values +type Menv = Env AnMname Envs -- modules +data Envs = Envs {tcenv_::Tcenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs + deriving Show + +{- Extend an environment, checking for illegal shadowing of identifiers (for term + variables -- shadowing type variables is allowed.) -} +data EnvType = Tv | NotTv + deriving Eq + +extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b) +extendM envType env (k,d) = + case elookup env k of + Just _ | envType == NotTv -> fail ("multiply-defined identifier: " + ++ show k) + _ -> return (eextend env (k,d)) + +extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b) +extendVenv = extendM NotTv + +extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b) +extendTvenv = extendM Tv + +lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b +lookupM env k = + case elookup env k of + Just v -> return v + Nothing -> fail ("undefined identifier: " ++ show k) + +{- Main entry point. -} +checkModule :: Menv -> Module -> CheckRes Menv +checkModule globalEnv (Module mn tdefs vdefgs) = + runReaderT + (do (tcenv, cenv) <- mkTypeEnvs tdefs + (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv)) + (eempty,eempty) + vdefgs + return (eextend globalEnv + (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))) + -- avoid name shadowing + (mn, eremove globalEnv mn) + +-- Like checkModule, but doesn't typecheck the code, instead just +-- returning declared types for top-level defns. +-- This is necessary in order to handle circular dependencies, but it's sort +-- of unpleasant. +envsModule :: Menv -> Module -> Menv +envsModule globalEnv (Module mn tdefs vdefgs) = + let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs + e_venv = foldr vdefgTypes eempty vdefgs in + eextend globalEnv (mn, + (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})) + where vdefgTypes :: Vdefg -> Venv -> Venv + vdefgTypes (Nonrec (Vdef (v,t,_))) e = + add [(v,t)] e + vdefgTypes (Rec vds) e = + add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e + add :: [(Qual Var,Ty)] -> Venv -> Venv + add pairs e = foldr addOne e pairs + addOne :: (Qual Var, Ty) -> Venv -> Venv + addOne ((Nothing,_),_) e = e + addOne ((Just _,v),t) e = eextend e (v,t) + +checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv +checkTdef0 tcenv tdef = ch tdef + where + ch (Data (m,c) tbs _) = + do mn <- getMname + requireModulesEq m mn "data type declaration" tdef False + extendM NotTv tcenv (c, Kind k) + where k = foldr Karrow Klifted (map snd tbs) + ch (Newtype (m,c) coVar tbs rhs) = + do mn <- getMname + requireModulesEq m mn "newtype declaration" tdef False + tcenv' <- extendM NotTv tcenv (c, Kind k) + -- add newtype axiom to env + tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs + return tcenv'' + where k = foldr Karrow Klifted (map snd tbs) + +processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv +processTdef0NoChecking tcenv tdef = ch tdef + where + ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k) + where k = foldr Karrow Klifted (map snd tbs) + ch (Newtype tc@(_,c) coercion tbs rhs) = + let tcenv' = eextend tcenv (c, Kind k) in + -- add newtype axiom to env + eextend tcenv' + (snd coercion, Coercion $ DefinedCoercion tbs + (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs)) + where k = foldr Karrow Klifted (map snd tbs) + +envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty + -> CheckResult Tcenv +envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv + (snd coVar, Coercion $ DefinedCoercion tbs + (foldl Tapp (Tcon tyCon) + (map Tvar (fst (unzip tbs))), + rep)) + +checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv +checkTdef tcenv cenv = ch + where + ch (Data (_,c) utbs cdefs) = + do cbinds <- mapM checkCdef cdefs + foldM (extendM NotTv) cenv cbinds + where checkCdef (cdef@(Constr (m,dcon) etbs ts)) = + do mn <- getMname + requireModulesEq m mn "constructor declaration" cdef + False + tvenv <- foldM (extendM Tv) eempty tbs + ks <- mapM (checkTy (tcenv,tvenv)) ts + mapM_ (\k -> require (baseKind k) + ("higher-order kind in:\n" ++ show cdef ++ "\n" ++ + "kind: " ++ show k) ) ks + return (dcon,t mn) + where tbs = utbs ++ etbs + t mn = foldr Tforall + (foldr tArrow + (foldl Tapp (Tcon (Just mn,c)) + (map (Tvar . fst) utbs)) ts) tbs + ch (tdef@(Newtype tc _ tbs t)) = + do tvenv <- foldM (extendM Tv) eempty tbs + kRhs <- checkTy (tcenv,tvenv) t + require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef) + kLhs <- checkTy (tcenv,tvenv) + (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs)))) + require (kLhs `eqKind` kRhs) + ("Kind mismatch in newtype axiom types: " ++ show tdef + ++ " kinds: " ++ + (show kLhs) ++ " and " ++ (show kRhs)) + return cenv + +processCdef :: Cenv -> Tdef -> Cenv +processCdef cenv = ch + where + ch (Data (_,c) utbs cdefs) = do + let cbinds = map checkCdef cdefs + foldl eextend cenv cbinds + where checkCdef (Constr (mn,dcon) etbs ts) = + (dcon,t mn) + where tbs = utbs ++ etbs + t mn = foldr Tforall + (foldr tArrow + (foldl Tapp (Tcon (mn,c)) + (map (Tvar . fst) utbs)) ts) tbs + ch _ = cenv + +mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv) +mkTypeEnvs tdefs = do + tcenv <- foldM checkTdef0 eempty tdefs + cenv <- foldM (checkTdef tcenv) eempty tdefs + return (tcenv, cenv) + +mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv) +mkTypeEnvsNoChecking tdefs = + let tcenv = foldl processTdef0NoChecking eempty tdefs + cenv = foldl processCdef eempty tdefs in + (tcenv, cenv) + +requireModulesEq :: Show a => Mname -> AnMname -> String -> a + -> Bool -> CheckResult () +requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t) +requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t) + +mkErrMsg :: Show a => String -> a -> String +mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t + +checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv) + -> Vdefg -> CheckResult (Venv,Venv) +checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do + mn <- getMname + case vdefg of + Rec vdefs -> + do (e_venv', l_venv') <- makeEnv mn vdefs + let env' = (tcenv,tvenv,cenv,e_venv',l_venv') + mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted) + ("unlifted kind in:\n" ++ show vdef)) env') + vdefs + return (e_venv', l_venv') + Nonrec vdef -> + do let env' = (tcenv, tvenv, cenv, e_venv, l_venv) + checkVdef (\ vdef k -> do + require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef) + require ((not top_level) || (not (k `eqKind` Kunlifted))) + ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef + makeEnv mn [vdef] + + where makeEnv mn vdefs = do + ev <- foldM extendVenv e_venv e_vts + lv <- foldM extendVenv l_venv l_vts + return (ev, lv) + where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs, + not (vdefIsMainWrapper mn (Just m))] + l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs] + checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do + mn <- getMname + let isZcMain = vdefIsMainWrapper mn m + unless isZcMain $ + requireModulesEq m mn "value definition" vdef True + k <- checkTy (tcenv,tvenv) t + checkKind vdef k + t' <- checkExp env e + require (t == t') + ("declared type doesn't match expression type in:\n" + ++ show vdef ++ "\n" ++ + "declared type: " ++ show t ++ "\n" ++ + "expression type: " ++ show t') + +vdefIsMainWrapper :: AnMname -> Mname -> Bool +vdefIsMainWrapper enclosing defining = + enclosing == mainMname && defining == wrapperMainAnMname + +checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv + -> Exp -> Ty +checkExpr mn menv tdefs venv tvenv e = case runReaderT (do + (tcenv, cenv) <- mkTypeEnvs tdefs + -- Since the preprocessor calls checkExpr after code has been + -- typechecked, we expect to find the external env in the Menv. + case (elookup menv mn) of + Just thisEnv -> + checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e + Nothing -> reportError e ("checkExpr: Environment for " ++ + show mn ++ " not found")) (mn,menv) of + OkC t -> t + FailC s -> reportError e s + +checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind +checkType mn menv tdefs tvenv t = case runReaderT (do + (tcenv, _) <- mkTypeEnvs tdefs + checkTy (tcenv, tvenv) t) (mn, menv) of + OkC k -> k + FailC s -> reportError tvenv s + +checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty +checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch + where + ch e0 = + case e0 of + Var qv -> + qlookupM venv_ e_venv l_venv qv + Dcon qc -> + qlookupM cenv_ cenv eempty qc + Lit l -> + checkLit l + Appt e t -> + do t' <- ch e + k' <- checkTy (tcenv,tvenv) t + case t' of + Tforall (tv,k) t0 -> + do require (k' `subKindOf` k) + ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++ + "operator kind: " ++ show k ++ "\n" ++ + "operand kind: " ++ show k') + return (substl [tv] [t] t0) + _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++ + "operator type: " ++ show t') + App e1 e2 -> + do t1 <- ch e1 + t2 <- ch e2 + case t1 of + Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow -> + do require (t2 == t') + ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ + "operator type: " ++ show t' ++ "\n" ++ + "operand type: " ++ show t2) + return t0 + _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++ + "operator type: " ++ show t1) + Lam (Tb tb) e -> + do tvenv' <- extendTvenv tvenv tb + t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e + return (Tforall tb t) + Lam (Vb (vb@(_,vt))) e -> + do k <- checkTy (tcenv,tvenv) vt + require (baseKind k) + ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ + "kind: " ++ show k) + l_venv' <- extendVenv l_venv vb + t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e + require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0) + return (tArrow vt t) + Let vdefg e -> + do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv) + (e_venv,l_venv) vdefg + checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e + Case e (v,t) resultTy alts -> + do t' <- ch e + checkTy (tcenv,tvenv) t + require (t == t') + ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++ + "declared type: " ++ show t ++ "\n" ++ + "expression type: " ++ show t') + case (reverse alts) of + (Acon c _ _ _):as -> + let ok ((Acon c _ _ _):as) cs = do require (notElem c cs) + ("duplicate alternative in case:\n" ++ show e0) + ok as (c:cs) + ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0) + ok [Adefault _] _ = return () + ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0) + ok [] _ = return () + in ok as [c] + (Alit l _):as -> + let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0) + ok ((Alit l _):as) ls = do require (notElem l ls) + ("duplicate alternative in case:\n" ++ show e0) + ok as (l:ls) + ok [Adefault _] _ = return () + ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0) + ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0) + in ok as [l] + [Adefault _] -> return () + _ -> fail ("no alternatives in case:\n" ++ show e0) + l_venv' <- extendVenv l_venv (v,t) + t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts + require (all (== t) ts) + ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++ + "types: " ++ show (t:ts)) + checkTy (tcenv,tvenv) resultTy + require (t == resultTy) ("case alternative type doesn't " ++ + " match case return type in:\n" ++ show e0 ++ "\n" ++ + "alt type: " ++ show t ++ " return type: " ++ show resultTy) + return t + c@(Cast e t) -> + do eTy <- ch e + (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t + require (eTy == fromTy) ("Type mismatch in cast: c = " + ++ show c ++ "\nand eTy = " ++ show eTy + ++ "\n and " ++ show fromTy) + return toTy + Note _ e -> + ch e + External _ t -> + do checkTy (tcenv,eempty) t {- external types must be closed -} + return t + +checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty +checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch + where + ch a0 = + case a0 of + Acon qc etbs vbs e -> + do let uts = f t0 + where f (Tapp t0 t) = f t0 ++ [t] + f _ = [] + ct <- qlookupM cenv_ cenv eempty qc + let (tbs,ct_args0,ct_res0) = splitTy ct + {- get universals -} + let (utbs,etbs') = splitAt (length uts) tbs + let utvs = map fst utbs + {- check existentials -} + let (etvs,eks) = unzip etbs + let (etvs',eks') = unzip etbs' + require (all (uncurry eqKind) + (zip eks eks')) + ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++ + "kinds declared in data constructor: " ++ show eks ++ + "kinds declared in case alternative: " ++ show eks') + tvenv' <- foldM extendTvenv tvenv etbs + {- check term variables -} + let vts = map snd vbs + mapM_ (\vt -> require ((not . isUtupleTy) vt) + ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++ + "pattern type: " ++ show vt)) vts + vks <- mapM (checkTy (tcenv,tvenv')) vts + mapM_ (\vk -> require (baseKind vk) + ("higher-order kind in:\n" ++ show a0 ++ "\n" ++ + "kind: " ++ show vk)) vks + let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0) + zipWithM_ + (\ct_arg vt -> + require (ct_arg == vt) + ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++ + "pattern variable type: " ++ show ct_arg ++ "\n" ++ + "constructor argument type: " ++ show vt)) ct_args vts + require (ct_res == t0) + ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ + "pattern constructor type: " ++ show ct_res ++ "\n" ++ + "scrutinee type: " ++ show t0) + l_venv' <- foldM extendVenv l_venv vbs + t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e + checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -} + return t + Alit l e -> + do t <- checkLit l + require (t == t0) + ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ + "pattern type: " ++ show t ++ "\n" ++ + "scrutinee type: " ++ show t0) + checkExp env e + Adefault e -> + checkExp env e + +checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind +checkTy es@(tcenv,tvenv) = ch + where + ch (Tvar tv) = lookupM tvenv tv + ch (Tcon qtc) = do + kOrC <- qlookupM tcenv_ tcenv eempty qtc + case kOrC of + Kind k -> return k + Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2 + Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc) + ch (t@(Tapp t1 t2)) = + case splitTyConApp_maybe t of + Just (tc, tys) -> do + tcK <- qlookupM tcenv_ tcenv eempty tc + case tcK of + Kind _ -> checkTapp t1 t2 + Coercion (DefinedCoercion tbs (from,to)) -> do + -- makes sure coercion is fully applied + require (length tys == length tbs) $ + ("Arity mismatch in coercion app: " ++ show t) + let (tvs, tks) = unzip tbs + argKs <- mapM (checkTy es) tys + let kPairs = zip argKs tks + -- Simon says it's okay for these to be + -- subkinds + let kindsOk = all (uncurry subKindOf) kPairs + require kindsOk + ("Kind mismatch in coercion app: " ++ show tks + ++ " and " ++ show argKs ++ " t = " ++ show t) + return $ Keq (substl tvs tys from) (substl tvs tys to) + Nothing -> checkTapp t1 t2 + where checkTapp t1 t2 = do + k1 <- ch t1 + k2 <- ch t2 + case k1 of + Karrow k11 k12 -> do + require (k2 `subKindOf` k11) kindError + return k12 + where kindError = + "kinds don't match in type application: " + ++ show t ++ "\n" ++ + "operator kind: " ++ show k11 ++ "\n" ++ + "operand kind: " ++ show k2 + _ -> fail ("applied type has non-arrow kind: " ++ show t) + + ch (Tforall tb t) = + do tvenv' <- extendTvenv tvenv tb + checkTy (tcenv,tvenv') t + ch (TransCoercion t1 t2) = do + (ty1,ty2) <- checkTyCo es t1 + (ty3,ty4) <- checkTyCo es t2 + require (ty2 == ty3) ("Types don't match in trans. coercion: " ++ + show ty2 ++ " and " ++ show ty3) + return $ Keq ty1 ty4 + ch (SymCoercion t1) = do + (ty1,ty2) <- checkTyCo es t1 + return $ Keq ty2 ty1 + ch (UnsafeCoercion t1 t2) = do + checkTy es t1 + checkTy es t2 + return $ Keq t1 t2 + ch (LeftCoercion t1) = do + k <- checkTyCo es t1 + case k of + ((Tapp u _), (Tapp w _)) -> return $ Keq u w + _ -> fail ("Bad coercion kind in operand of left: " ++ show k) + ch (RightCoercion t1) = do + k <- checkTyCo es t1 + case k of + ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x + _ -> fail ("Bad coercion kind in operand of left: " ++ show k) + ch (InstCoercion ty arg) = do + forallK <- checkTyCo es ty + case forallK of + ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do + require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: " + ++ show ty) + argK <- checkTy es arg + require (argK `eqKind` k1) ("Kind mismatch in type being " + ++ "instantiated: " ++ show arg) + let newLhs = substl [v1] [arg] b1 + let newRhs = substl [v2] [arg] b2 + return $ Keq newLhs newRhs + _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty) + +checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty) +checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = + (case splitTyConApp_maybe t of + Just (tc, tys) -> do + tcK <- qlookupM tcenv_ tcenv eempty tc + case tcK of + -- todo: avoid duplicating this code + -- blah, this almost calls for a different syntactic form + -- (for a defined-coercion app): (TCoercionApp Tcon [Ty]) + Coercion (DefinedCoercion tbs (from, to)) -> do + require (length tys == length tbs) $ + ("Arity mismatch in coercion app: " ++ show t) + let (tvs, tks) = unzip tbs + argKs <- mapM (checkTy es) tys + let kPairs = zip argKs tks + let kindsOk = all (uncurry subKindOf) kPairs + require kindsOk + ("Kind mismatch in coercion app: " ++ show tks + ++ " and " ++ show argKs ++ " t = " ++ show t) + return (substl tvs tys from, substl tvs tys to) + _ -> checkTapp t1 t2 + _ -> checkTapp t1 t2) + where checkTapp t1 t2 = do + (lhsRator, rhsRator) <- checkTyCo es t1 + (lhs, rhs) <- checkTyCo es t2 + -- Comp rule from paper + checkTy es (Tapp lhsRator lhs) + checkTy es (Tapp rhsRator rhs) + return (Tapp lhsRator lhs, Tapp rhsRator rhs) +checkTyCo (tcenv, tvenv) (Tforall tb t) = do + tvenv' <- extendTvenv tvenv tb + (t1,t2) <- checkTyCo (tcenv, tvenv') t + return (Tforall tb t1, Tforall tb t2) +checkTyCo es t = do + k <- checkTy es t + case k of + Keq t1 t2 -> return (t1, t2) + -- otherwise, expand by the "refl" rule + _ -> return (t, t) + +mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname + -> CheckResult (Env a b) +mlookupM _ _ local_env Nothing = return local_env +mlookupM selector external_env local_env (Just m) = do + mn <- getMname + if m == mn + then return external_env + else do + globalEnv <- getGlobalEnv + case elookup globalEnv m of + Just env' -> return (selector env') + Nothing -> fail ("Check: undefined module name: " + ++ show m ++ show (edomain local_env)) + +qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b + -> Qual a -> CheckResult b +qlookupM selector external_env local_env (m,k) = + do env <- mlookupM selector external_env local_env m + lookupM env k + +checkLit :: Lit -> CheckResult Ty +checkLit (Literal lit t) = + case lit of + Lint _ -> + do require (t `elem` intLitTypes) + ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) + return t + Lrational _ -> + do require (t `elem` ratLitTypes) + ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) + return t + Lchar _ -> + do require (t `elem` charLitTypes) + ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) + return t + Lstring _ -> + do require (t `elem` stringLitTypes) + ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) + return t + +{- Utilities -} + +{- Split off tbs, arguments and result of a (possibly abstracted) arrow type -} +splitTy :: Ty -> ([Tbind],[Ty],Ty) +splitTy (Tforall tb t) = (tb:tbs,ts,tr) + where (tbs,ts,tr) = splitTy t +splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr) + where (tbs,ts,tr) = splitTy t +splitTy t = ([],[],t) + + +{- Simultaneous substitution on types for type variables, + renaming as neceessary to avoid capture. + No checks for correct kindedness. -} +substl :: [Tvar] -> [Ty] -> Ty -> Ty +substl tvs ts t = f (zip tvs ts) t + where + f env t0 = + case t0 of + Tcon _ -> t0 + Tvar v -> case lookup v env of + Just t1 -> t1 + Nothing -> t0 + Tapp t1 t2 -> Tapp (f env t1) (f env t2) + Tforall (t,k) t1 -> + if t `elem` free then + Tforall (t',k) (f ((t,Tvar t'):env) t1) + else + Tforall (t,k) (f (filter ((/=t).fst) env) t1) + TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2) + SymCoercion t1 -> SymCoercion (f env t1) + UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2) + LeftCoercion t1 -> LeftCoercion (f env t1) + RightCoercion t1 -> RightCoercion (f env t1) + InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2) + where free = foldr union [] (map (freeTvars.snd) env) + t' = freshTvar free + +{- Return free tvars in a type -} +freeTvars :: Ty -> [Tvar] +freeTvars (Tcon _) = [] +freeTvars (Tvar v) = [v] +freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2 +freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1) +freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 +freeTvars (SymCoercion t) = freeTvars t +freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 +freeTvars (LeftCoercion t) = freeTvars t +freeTvars (RightCoercion t) = freeTvars t +freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2 + +{- Return any tvar *not* in the argument list. -} +freshTvar :: [Tvar] -> Tvar +freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way! + +primCoercionError :: Show a => a -> b +primCoercionError s = error $ "Bad coercion application: " ++ show s + +-- todo +reportError :: Show a => a -> String -> b +reportError e s = error $ ("Core type error: checkExpr failed with " + ++ s ++ " and " ++ show e)