X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FCheck.hs;h=cab3e62ebdca6831f9626d6e42e734b9db78c5cc;hp=a9a3eac8f49845362ccdb9404e6b5b3d4cafd594;hb=10704b34c1928dde3d0ef33fe37c3eb7b948975f;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1 diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index a9a3eac..cab3e62 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -1,20 +1,40 @@ -module Check where +{-# OPTIONS -Wall -fno-warn-name-shadowing #-} +module Check( + checkModule, envsModule, + checkExpr, checkType, + primCoercionError, + Menv, Venv, Tvenv, Envs(..), + CheckRes(..), splitTy, substl) where + +import Maybe +import Control.Monad.Reader +-- just for printing warnings +import System.IO.Unsafe -import Monad import Core -import Printer +import Printer() import List import Env +import PrimEnv {- 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. -} -data CheckResult a = OkC a | FailC String +{- 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 CheckResult where +instance Monad CheckRes where OkC a >>= k = k a - FailC s >>= k = fail s + FailC s >>= _ = fail s return = OkC fail = FailC @@ -29,19 +49,31 @@ requireM cond s = {- Environments. -} type Tvenv = Env Tvar Kind -- type variables (local only) -type Tcenv = Env Tcon Kind -- type constructors +type Tcenv = Env Tcon KindOrCoercion -- type constructors type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms type Cenv = Env Dcon Ty -- data constructors type Venv = Env Var Ty -- values -type Menv = Env Mname Envs -- modules +type Menv = Env AnMname Envs -- modules data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,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 -{- Extend an environment, checking for illegal shadowing of identifiers. -} -extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b) -extendM env (k,d) = +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 _ -> fail ("multiply-defined identifier: " ++ show k) - Nothing -> return (eextend env (k,d)) + 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 = @@ -50,100 +82,222 @@ lookupM env k = Nothing -> fail ("undefined identifier: " ++ show k) {- Main entry point. -} -checkModule :: Menv -> Module -> CheckResult Menv +checkModule :: Menv -> Module -> CheckRes Menv checkModule globalEnv (Module mn tdefs vdefgs) = - do (tcenv,tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs - cenv <- foldM (checkTdef tcenv) eempty tdefs - (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) (eempty,eempty) vdefgs - return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})) - where + runReaderT + (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs + (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) + (eempty,eempty) + vdefgs + return (eextend globalEnv + (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,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, tsenv, cenv) = mkTypeEnvsNoChecking tdefs + e_venv = foldr vdefgTypes eempty vdefgs in + eextend globalEnv (mn, + (Envs{tcenv_=tcenv,tsenv_=tsenv,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,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv) - checkTdef0 (tcenv,tsenv) tdef = ch tdef +checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv) +checkTdef0 (tcenv,tsenv) tdef = ch tdef where ch (Data (m,c) tbs _) = - do require (m == mn) ("wrong module name in data type declaration:\n" ++ show tdef) - tcenv' <- extendM tcenv (c,k) + do mn <- getMname + requireModulesEq m mn "data type declaration" tdef False + tcenv' <- extendM NotTv tcenv (c, Kind k) return (tcenv',tsenv) where k = foldr Karrow Klifted (map snd tbs) - ch (Newtype (m,c) tbs rhs) = - do require (m == mn) ("wrong module name in newtype declaration:\n" ++ show tdef) - tcenv' <- extendM tcenv (c,k) + ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = + do mn <- getMname + requireModulesEq m mn "newtype declaration" tdef False + tcenv' <- extendM NotTv tcenv (c, Kind k) + -- add newtype axiom to env + tcenv'' <- extendM NotTv tcenv' + (coercion, Coercion $ DefinedCoercion cTbs coercionKind) tsenv' <- case rhs of Nothing -> return tsenv - Just rep -> extendM tsenv (c,(map fst tbs,rep)) - return (tcenv', tsenv') + Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep)) + return (tcenv'', tsenv') + where k = foldr Karrow Klifted (map snd tbs) + +processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv) +processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef + where + ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv) + where k = foldr Karrow Klifted (map snd tbs) + ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = + let tcenv' = eextend tcenv (c, Kind k) + -- add newtype axiom to env + tcenv'' = eextend tcenv' + (coercion, Coercion $ DefinedCoercion cTbs coercionKind) + tsenv' = maybe tsenv + (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in + (tcenv'', tsenv') where k = foldr Karrow Klifted (map snd tbs) - checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv - checkTdef tcenv cenv = ch +checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv +checkTdef tcenv cenv = ch where ch (Data (_,c) utbs cdefs) = do cbinds <- mapM checkCdef cdefs - foldM extendM cenv cbinds + foldM (extendM NotTv) cenv cbinds where checkCdef (cdef@(Constr (m,dcon) etbs ts)) = - do require (m == mn) ("wrong module name in constructor declaration:\n" ++ show cdef) - tvenv <- foldM extendM eempty tbs + 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) + return (dcon,t mn) where tbs = utbs ++ etbs - t = foldr Tforall + t mn = foldr Tforall (foldr tArrow - (foldl Tapp (Tcon (mn,c)) + (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype c tbs (Just t))) = - do tvenv <- foldM extendM eempty tbs + ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) = + do tvenv <- foldM (extendM Tv) eempty tbs k <- checkTy (tcenv,tvenv) t - require (k==Klifted) ("bad kind:\n" ++ show tdef) + -- Makes sure GHC is eta-expanding things properly + require (length tbs == length coTbs) $ + ("Arity mismatch between newtycon and newtype coercion: " + ++ show tdef) + require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef) + axiomTvenv <- foldM (extendM Tv) eempty coTbs + kLhs <- checkTy (tcenv,axiomTvenv) coLhs + kRhs <- checkTy (tcenv,axiomTvenv) coRhs + require (kLhs `eqKind` kRhs) + ("Kind mismatch in newtype axiom types: " ++ show tdef + ++ " kinds: " ++ + (show kLhs) ++ " and " ++ (show kRhs)) return cenv - ch (tdef@(Newtype c tbs Nothing)) = + ch (Newtype _ _ _ Nothing) = {- should only occur for recursive Newtypes -} return cenv - - checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv) - checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = +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, Tsenv, Cenv) +mkTypeEnvs tdefs = do + (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs + cenv <- foldM (checkTdef tcenv) eempty tdefs + return (tcenv, tsenv, cenv) + +mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv) +mkTypeEnvsNoChecking tdefs = + let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs + cenv = foldl processCdef eempty tdefs in + (tcenv, tsenv, 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,Tsenv,Tvenv,Cenv) -> (Venv,Venv) + -> Vdefg -> CheckResult (Venv,Venv) +checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do + mn <- getMname case vdefg of Rec vdefs -> - do e_venv' <- foldM extendM e_venv e_vts - l_venv' <- foldM extendM l_venv l_vts + do (e_venv', l_venv') <- makeEnv mn vdefs let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') - mapM_ (\ (vdef@(Vdef ((m,v),t,e))) -> - do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef) - k <- checkTy (tcenv,tvenv) t - require (k==Klifted) ("unlifted kind in:\n" ++ show vdef) - t' <- checkExp env' e - requireM (equalTy tsenv t t') - ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t')) vdefs - return (e_venv',l_venv') - where e_vts = [ (v,t) | Vdef ((m,v),t,_) <- vdefs, m /= "" ] - l_vts = [ (v,t) | Vdef (("",v),t,_) <- vdefs] - Nonrec (vdef@(Vdef ((m,v),t,e))) -> - do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef) - k <- checkTy (tcenv,tvenv) t - require (k /= Kopen) ("open kind in:\n" ++ show vdef) - require ((not top_level) || (k /= Kunlifted)) ("top-level unlifted kind in:\n" ++ show vdef) - t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e - requireM (equalTy tsenv t t') - ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++ - "declared type: " ++ show t ++ "\n" ++ - "expression type: " ++ show t') - if m == "" then - do l_venv' <- extendM l_venv (v,t) - return (e_venv,l_venv') - else - do e_venv' <- extendM e_venv (v,t) - return (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, tsenv, 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 + requireM (equalTy tsenv t t') + ("declared type doesn't match expression type in:\n" + ++ show vdef ++ "\n" ++ + "declared type: " ++ show t ++ "\n" ++ + "expression type: " ++ show t') - checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty - checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch +vdefIsMainWrapper :: AnMname -> Mname -> Bool +vdefIsMainWrapper enclosing defining = + enclosing == mainMname && defining == wrapperMainMname + +checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv + -> Exp -> Ty +checkExpr mn menv tdefs venv tvenv e = case runReaderT (do + (tcenv, tsenv, 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, tsenv, 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,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty +checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch where - ch e0 = + ch e0 = case e0 of Var qv -> qlookupM venv_ e_venv l_venv qv @@ -156,7 +310,7 @@ checkModule globalEnv (Module mn tdefs vdefgs) = k' <- checkTy (tcenv,tvenv) t case t' of Tforall (tv,k) t0 -> - do require (k' <= k) + 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') @@ -176,7 +330,7 @@ checkModule globalEnv (Module mn tdefs vdefgs) = _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++ "operator type: " ++ show t1) Lam (Tb tb) e -> - do tvenv' <- extendM tvenv tb + do tvenv' <- extendTvenv tvenv tb t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e return (Tforall tb t) Lam (Vb (vb@(_,vt))) e -> @@ -184,14 +338,15 @@ checkModule globalEnv (Module mn tdefs vdefgs) = require (baseKind k) ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ "kind: " ++ show k) - l_venv' <- extendM l_venv vb + l_venv' <- extendVenv l_venv vb t <- checkExp (tcenv,tsenv,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,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg + do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv) + (e_venv,l_venv) vdefg checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e - Case e (v,t) alts -> + Case e (v,t) resultTy alts -> do t' <- ch e checkTy (tcenv,tvenv) t requireM (equalTy tsenv t t') @@ -218,26 +373,33 @@ checkModule globalEnv (Module mn tdefs vdefgs) = 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' <- extendM l_venv (v,t) + _ -> fail ("no alternatives in case:\n" ++ show e0) + l_venv' <- extendVenv l_venv (v,t) t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts bs <- mapM (equalTy tsenv t) ts require (and bs) ("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 - Coerce t e -> - do ch e - checkTy (tcenv,tvenv) t - return t - Note s e -> + 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,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty - checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch +checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty +checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch where ch a0 = case a0 of @@ -253,11 +415,12 @@ checkModule globalEnv (Module mn tdefs vdefgs) = {- check existentials -} let (etvs,eks) = unzip etbs let (etvs',eks') = unzip etbs' - require (eks == eks') + 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 extendM tvenv etbs + tvenv' <- foldM extendTvenv tvenv etbs {- check term variables -} let vts = map snd vbs mapM_ (\vt -> require ((not . isUtupleTy) vt) @@ -278,7 +441,7 @@ checkModule globalEnv (Module mn tdefs vdefgs) = ("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 extendM l_venv vbs + l_venv' <- foldM extendVenv l_venv vbs t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -} return t @@ -292,29 +455,150 @@ checkModule globalEnv (Module mn tdefs vdefgs) = Adefault e -> checkExp env e - checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind - checkTy (tcenv,tvenv) = ch +checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind +checkTy es@(tcenv,tvenv) = ch where ch (Tvar tv) = lookupM tvenv tv - ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc + 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)) = - do k1 <- ch t1 - k2 <- ch t2 - case k1 of - Karrow k11 k12 -> - do require (k2 <= k11) - ("kinds don't match in type application: " ++ show t ++ "\n" ++ - "operator kind: " ++ show k11 ++ "\n" ++ - "operand kind: " ++ show k2) - return k12 - _ -> fail ("applied type has non-arrow kind: " ++ show t) + 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 + let kindsOk = all (uncurry eqKind) kPairs + if not kindsOk && + all (uncurry subKindOf) kPairs + -- GHC occasionally generates code like: + -- :Co:TTypeable2 (->) + -- where in this case, :Co:TTypeable2 expects an + -- argument of kind (*->(*->*)) and (->) has kind + -- (?->(?->*)). I'm not sure whether or not it's + -- sound to apply an arbitrary coercion to an + -- argument that's a subkind of what it expects. + then warn $ "Applying coercion " ++ show tc ++ + " to arguments of kind " ++ show argKs + ++ " when it expects: " ++ show tks + else 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' <- extendM tvenv tb - checkTy (tcenv,tvenv') t - - {- Type equality modulo newtype synonyms. -} - equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool - equalTy tsenv t1 t2 = + 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 eqKind) kPairs + if not kindsOk && + all (uncurry subKindOf) kPairs + -- see comments in checkTy about this + then warn $ "Applying coercion " ++ show tc ++ + " to arguments of kind " ++ show argKs + ++ " when it expects: " ++ show tks + else 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) + +{- Type equality modulo newtype synonyms. -} +equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool +equalTy tsenv t1 t2 = do t1' <- expand t1 t2' <- expand t2 return (t1' == t2') @@ -326,10 +610,32 @@ checkModule globalEnv (Module mn tdefs vdefgs) = expand (Tforall tb t) = do t' <- expand t return (Tforall tb t') + expand (TransCoercion t1 t2) = do + exp1 <- expand t1 + exp2 <- expand t2 + return $ TransCoercion exp1 exp2 + expand (SymCoercion t) = do + exp <- expand t + return $ SymCoercion exp + expand (UnsafeCoercion t1 t2) = do + exp1 <- expand t1 + exp2 <- expand t2 + return $ UnsafeCoercion exp1 exp2 + expand (LeftCoercion t1) = do + exp1 <- expand t1 + return $ LeftCoercion exp1 + expand (RightCoercion t1) = do + exp1 <- expand t1 + return $ RightCoercion exp1 + expand (InstCoercion t1 t2) = do + exp1 <- expand t1 + exp2 <- expand t2 + return $ InstCoercion exp1 exp2 expapp (t@(Tcon (m,tc))) ts = do env <- mlookupM tsenv_ tsenv eempty m case elookup env tc of - Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs) + Just (formals,rhs) | (length formals) == (length ts) -> + return (substl formals ts rhs) _ -> return (foldl Tapp t ts) expapp (Tapp t1 t2) ts = do t2' <- expand t2 @@ -337,43 +643,45 @@ checkModule globalEnv (Module mn tdefs vdefgs) = expapp t ts = do t' <- expand t return (foldl Tapp t' ts) - - mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname -> CheckResult (Env a b) - mlookupM selector external_env local_env m = - if m == "" then - return local_env - else if m == mn then - return external_env - else - case elookup globalEnv m of - Just env' -> return (selector env') - Nothing -> fail ("undefined module name: " ++ show m) - - qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> (Mname,a) -> CheckResult b - qlookupM selector external_env local_env (m,k) = - do env <- mlookupM selector external_env local_env m - lookupM env k +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 lit = +checkLit (Literal lit t) = case lit of - Lint _ t -> - do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh]) - ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -} + Lint _ -> + do require (t `elem` intLitTypes) + ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) return t - Lrational _ t -> - do {- require (elem t [tFloatzh,tDoublezh]) - ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -} + Lrational _ -> + do require (t `elem` ratLitTypes) + ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) return t - Lchar _ t -> - do {- require (t == tCharzh) - ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -} + Lchar _ -> + do require (t `elem` charLitTypes) + ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) return t - Lstring _ t -> - do {- require (t == tAddrzh) - ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -} + Lstring _ -> + do require (t `elem` stringLitTypes) + ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) return t {- Utilities -} @@ -405,6 +713,12 @@ substl tvs ts t = f (zip tvs ts) t 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 @@ -412,10 +726,26 @@ substl tvs ts t = f (zip tvs ts) t freeTvars :: Ty -> [Tvar] freeTvars (Tcon _) = [] freeTvars (Tvar v) = [v] -freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2) +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) + +warn :: String -> CheckResult () +warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return () \ No newline at end of file