X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=utils%2Fext-core%2FCheck.hs;h=cab3e62ebdca6831f9626d6e42e734b9db78c5cc;hb=10704b34c1928dde3d0ef33fe37c3eb7b948975f;hp=29fb71fcde04393569b6f90ec580c7010a3730bb;hpb=420a27dc9fb7de5fc6c96fe078ddd4dc87222d44;p=ghc-hetmet.git diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index 29fb71f..cab3e62 100644 --- a/utils/ext-core/Check.hs +++ b/utils/ext-core/Check.hs @@ -8,6 +8,8 @@ module Check( import Maybe import Control.Monad.Reader +-- just for printing warnings +import System.IO.Unsafe import Core import Printer() @@ -89,7 +91,8 @@ checkModule globalEnv (Module mn tdefs vdefgs) = vdefgs return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))) - (mn, globalEnv) + -- avoid name shadowing + (mn, eremove globalEnv mn) -- Like checkModule, but doesn't typecheck the code, instead just -- returning declared types for top-level defns. @@ -227,51 +230,44 @@ 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 = +checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do + mn <- getMname case vdefg of Rec vdefs -> - do e_venv' <- foldM extendVenv e_venv e_vts - l_venv' <- foldM extendVenv 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,_),t,e))) -> - do mn <- getMname - requireModulesEq m mn "value definition" vdef True - k <- checkTy (tcenv,tvenv) t - require (k `eqKind` 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 ((Just _,v),t,_) <- vdefs ] - l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs] - Nonrec (vdef@(Vdef ((m,v),t,e))) -> - do mn <- getMname - -- TODO: document this weirdness - let isZcMain = vdefIsMainWrapper mn m - unless isZcMain $ - requireModulesEq m mn "value definition" vdef True - k <- checkTy (tcenv,tvenv) t - 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) - 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 isNothing m then - do l_venv' <- extendVenv l_venv (v,t) - return (e_venv,l_venv') - else - -- awful, but avoids name shadowing -- - -- otherwise we'd have two bindings for "main" - do e_venv' <- if isZcMain - then return e_venv - else extendVenv 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') vdefIsMainWrapper :: AnMname -> Mname -> Bool vdefIsMainWrapper enclosing defining = @@ -301,7 +297,7 @@ checkType mn menv tdefs tvenv t = case runReaderT (do 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 @@ -391,15 +387,11 @@ checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch return t c@(Cast e t) -> do eTy <- ch e - k <- checkTy (tcenv,tvenv) t - case k of - (Keq fromTy toTy) -> do - require (eTy == fromTy) ("Type mismatch in cast: c = " - ++ show c ++ " and " ++ show eTy - ++ " and " ++ show fromTy) - return toTy - _ -> fail ("Cast with non-equality kind: " ++ show e - ++ " and " ++ show t ++ " has kind " ++ show k) + (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 -> @@ -464,7 +456,7 @@ checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch checkExp env e checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind -checkTy es@(tcenv,tvenv) t = ch t +checkTy es@(tcenv,tvenv) = ch where ch (Tvar tv) = lookupM tvenv tv ch (Tcon qtc) = do @@ -485,29 +477,32 @@ checkTy es@(tcenv,tvenv) t = ch t ("Arity mismatch in coercion app: " ++ show t) let (tvs, tks) = unzip tbs argKs <- mapM (checkTy es) tys - require (all (uncurry eqKind) (zip tks argKs)) + 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 + k1 <- ch t1 k2 <- ch t2 case k1 of - Karrow k11 k12 -> - case k2 of - Keq eqTy1 eqTy2 -> do - -- Distribute the type operator over the - -- coercion - subK1 <- checkTy es eqTy1 - subK2 <- checkTy es eqTy2 - require (subK2 `subKindOf` k11 && - subK1 `subKindOf` k11) $ - kindError - return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2) - _ -> do - require (k2 `subKindOf` k11) kindError - return k12 + Karrow k11 k12 -> do + require (k2 `subKindOf` k11) kindError + return k12 where kindError = "kinds don't match in type application: " ++ show t ++ "\n" ++ @@ -517,39 +512,89 @@ checkTy es@(tcenv,tvenv) t = ch t ch (Tforall tb t) = do tvenv' <- extendTvenv tvenv tb - k <- checkTy (tcenv,tvenv') t - return $ case k of - -- distribute the forall - Keq t1 t2 -> Keq (Tforall tb t1) (Tforall tb t2) - _ -> k + checkTy (tcenv,tvenv') t ch (TransCoercion t1 t2) = do - k1 <- checkTy es t1 - k2 <- checkTy es t2 - case (k1, k2) of - (Keq ty1 ty2, Keq ty3 ty4) | ty2 == ty3 -> - return $ Keq ty1 ty4 - _ -> fail ("Bad kinds in trans. coercion: " ++ - show k1 ++ " " ++ show k2) + (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 - k <- checkTy es t1 - case k of - Keq ty1 ty2 -> return $ Keq ty2 ty1 - _ -> fail ("Bad kind in sym. coercion: " - ++ show k) + (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 <- checkTy es t1 + k <- checkTyCo es t1 case k of - Keq (Tapp u _) (Tapp w _) -> return $ Keq u w + ((Tapp u _), (Tapp w _)) -> return $ Keq u w _ -> fail ("Bad coercion kind in operand of left: " ++ show k) ch (RightCoercion t1) = do - k <- checkTy es t1 + k <- checkTyCo es t1 case k of - Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x + ((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 @@ -582,6 +627,10 @@ equalTy tsenv t1 t2 = 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 @@ -669,6 +718,7 @@ substl tvs ts t = f (zip tvs ts) t 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 @@ -676,13 +726,14 @@ 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 @@ -696,3 +747,5 @@ 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