X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=utils%2Fext-core%2FCheck.hs;h=e379cd75826070994e907182ddb185290ced8ee6;hp=4d35676b97a1020846c5ab4c9a54956244b41a29;hb=8bfeb25ae78e99c7014113468b0057342db4208f;hpb=044805225a08d5e370b72d2efed66880912b0806;ds=sidebyside diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index 4d35676..e379cd7 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -8,8 +8,6 @@ module Check( import Maybe import Control.Monad.Reader --- just for printing warnings -import System.IO.Unsafe import Core import Printer() @@ -42,19 +40,13 @@ require :: Bool -> String -> CheckResult () require False s = fail s require True _ = return () -requireM :: CheckResult Bool -> String -> CheckResult () -requireM cond s = - do b <- cond - require b s - {- Environments. -} type Tvenv = Env Tvar Kind -- type variables (local only) 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 AnMname Envs -- modules -data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs +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 @@ -85,12 +77,12 @@ lookupM env k = checkModule :: Menv -> Module -> CheckRes Menv checkModule globalEnv (Module mn tdefs vdefgs) = runReaderT - (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs - (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) + (do (tcenv, cenv) <- mkTypeEnvs tdefs + (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv)) (eempty,eempty) vdefgs return (eextend globalEnv - (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))) + (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))) -- avoid name shadowing (mn, eremove globalEnv mn) @@ -100,10 +92,10 @@ checkModule globalEnv (Module mn tdefs vdefgs) = -- of unpleasant. envsModule :: Menv -> Module -> Menv envsModule globalEnv (Module mn tdefs vdefgs) = - let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs + let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs e_venv = foldr vdefgTypes eempty vdefgs in eextend globalEnv (mn, - (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})) + (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})) where vdefgTypes :: Vdefg -> Venv -> Venv vdefgTypes (Nonrec (Vdef (v,t,_))) e = add [(v,t)] e @@ -115,14 +107,13 @@ envsModule globalEnv (Module mn tdefs vdefgs) = 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 -> 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 - tcenv' <- extendM NotTv tcenv (c, Kind k) - return (tcenv',tsenv) + extendM NotTv tcenv (c, Kind k) where k = foldr Karrow Klifted (map snd tbs) ch (Newtype (m,c) coVar tbs rhs) = do mn <- getMname @@ -130,37 +121,25 @@ checkTdef0 (tcenv,tsenv) tdef = ch tdef tcenv' <- extendM NotTv tcenv (c, Kind k) -- add newtype axiom to env tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs - tsenv' <- case rhs of - Nothing -> return tsenv - Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep)) - return (tcenv'', tsenv') + return tcenv'' where k = foldr Karrow Klifted (map snd tbs) -processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv) -processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef +processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv +processTdef0NoChecking tcenv tdef = ch tdef where - ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv) + 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) + let tcenv' = eextend tcenv (c, Kind k) in -- add newtype axiom to env - tcenv'' = case rhs of - Just rep -> - eextend tcenv' - (snd coercion, Coercion $ DefinedCoercion tbs - (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep)) - Nothing -> tcenv' - tsenv' = maybe tsenv - (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in - (tcenv'', tsenv') + 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] -> Maybe Ty +envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty -> CheckResult Tcenv -envPlusNewtype tcenv tyCon coVar tbs rhs = - case rhs of - Nothing -> return tcenv - Just rep -> extendM NotTv tcenv +envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv (snd coVar, Coercion $ DefinedCoercion tbs (foldl Tapp (Tcon tyCon) (map Tvar (fst (unzip tbs))), @@ -187,7 +166,7 @@ checkTdef tcenv cenv = ch (foldr tArrow (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype tc _ tbs (Just t))) = + 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) @@ -198,9 +177,6 @@ checkTdef tcenv cenv = ch ++ " kinds: " ++ (show kLhs) ++ " and " ++ (show kRhs)) return cenv - ch (Newtype _ _ _ Nothing) = - {- should only occur for recursive Newtypes -} - return cenv processCdef :: Cenv -> Tdef -> Cenv processCdef cenv = ch @@ -217,17 +193,17 @@ processCdef cenv = ch (map (Tvar . fst) utbs)) ts) tbs ch _ = cenv -mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv) +mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv) mkTypeEnvs tdefs = do - (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs + tcenv <- foldM checkTdef0 eempty tdefs cenv <- foldM (checkTdef tcenv) eempty tdefs - return (tcenv, tsenv, cenv) + return (tcenv, cenv) -mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv) +mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv) mkTypeEnvsNoChecking tdefs = - let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs - cenv = foldl processCdef eempty tdefs in - (tcenv, tsenv, cenv) + let tcenv = foldl processTdef0NoChecking eempty tdefs + cenv = foldl processCdef eempty tdefs in + (tcenv, cenv) requireModulesEq :: Show a => Mname -> AnMname -> String -> a -> Bool -> CheckResult () @@ -237,20 +213,20 @@ 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) +checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv) -checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do +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,tsenv,tvenv,cenv,e_venv',l_venv') + 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, tsenv, tvenv, cenv, e_venv, l_venv) + 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))) @@ -272,7 +248,7 @@ checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do k <- checkTy (tcenv,tvenv) t checkKind vdef k t' <- checkExp env e - requireM (equalTy tsenv t t') + require (t == t') ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++ "declared type: " ++ show t ++ "\n" ++ @@ -285,12 +261,12 @@ vdefIsMainWrapper enclosing defining = checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv -> Exp -> Ty checkExpr mn menv tdefs venv tvenv e = case runReaderT (do - (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs + (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, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e + checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e Nothing -> reportError e ("checkExpr: Environment for " ++ show mn ++ " not found")) (mn,menv) of OkC t -> t @@ -298,13 +274,13 @@ checkExpr mn menv tdefs venv tvenv e = case runReaderT (do checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind checkType mn menv tdefs tvenv t = case runReaderT (do - (tcenv, _, _) <- mkTypeEnvs tdefs + (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 +checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty +checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch where ch e0 = case e0 of @@ -331,7 +307,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch t2 <- ch e2 case t1 of Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow -> - do requireM (equalTy tsenv t2 t') + do require (t2 == t') ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++ "operator type: " ++ show t' ++ "\n" ++ "operand type: " ++ show t2) @@ -340,7 +316,7 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch "operator type: " ++ show t1) Lam (Tb tb) e -> do tvenv' <- extendTvenv tvenv tb - t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e + 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 @@ -348,17 +324,17 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch ("higher-order kind in:\n" ++ show e0 ++ "\n" ++ "kind: " ++ show k) l_venv' <- extendVenv l_venv vb - t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e + 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,tsenv,tvenv,cenv) - (e_venv,l_venv) vdefg - checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') 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 - requireM (equalTy tsenv t 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') @@ -384,9 +360,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch [Adefault _] -> return () _ -> 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) + 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 @@ -407,8 +382,8 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch 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,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 @@ -442,21 +417,21 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0) zipWithM_ (\ct_arg vt -> - requireM (equalTy tsenv 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 - requireM (equalTy tsenv ct_res t0) + 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,tsenv,tvenv',cenv,e_venv,l_venv') e + 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 - requireM (equalTy tsenv t t0) + require (t == t0) ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++ "pattern type: " ++ show t ++ "\n" ++ "scrutinee type: " ++ show t0) @@ -487,20 +462,10 @@ checkTy es@(tcenv,tvenv) = ch 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 + -- 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) @@ -574,16 +539,10 @@ checkTyCo es@(tcenv,_) t@(Tapp t1 t2) = 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) + 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) @@ -605,54 +564,6 @@ checkTyCo es t = do -- 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') - where expand (Tvar v) = return (Tvar v) - expand (Tcon qtc) = return (Tcon qtc) - expand (Tapp t1 t2) = - do t2' <- expand t2 - expapp t1 [t2'] - 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) - _ -> return (foldl Tapp t ts) - expapp (Tapp t1 t2) ts = - do t2' <- expand t2 - expapp t1 (t2':ts) - expapp t ts = - do t' <- expand t - return (foldl Tapp t' ts) - 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 @@ -755,6 +666,3 @@ primCoercionError s = error $ "Bad coercion application: " ++ show s 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