X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=utils%2Fext-core%2FCheck.hs;h=e379cd75826070994e907182ddb185290ced8ee6;hb=8e3f4465c2a85e6328df52939c9e2429dc63aaca;hp=95c72812a6c8acb2d48958151ef4d10e78e96db5;hpb=2ad4df602e5bb2cff0315b945fa3201749878c30;p=ghc-hetmet.git diff --git a/utils/ext-core/Check.hs b/utils/ext-core/Check.hs index 95c7281..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,13 +77,14 @@ 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, 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. @@ -99,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 @@ -114,42 +107,43 @@ 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) tbs ((_,coercion),cTbs,coercionKind) rhs) = + 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'' <- extendM NotTv tcenv' - (coercion, Coercion $ DefinedCoercion cTbs coercionKind) - tsenv' <- case rhs of - Nothing -> return tsenv - Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep)) - return (tcenv'', tsenv') + tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs + 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 (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) = - let tcenv' = eextend tcenv (c, Kind k) + ch (Newtype tc@(_,c) coercion tbs rhs) = + let tcenv' = eextend tcenv (c, Kind k) in -- 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') + 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 @@ -172,25 +166,17 @@ checkTdef tcenv cenv = ch (foldr tArrow (foldl Tapp (Tcon (Just mn,c)) (map (Tvar . fst) utbs)) ts) tbs - ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) = + ch (tdef@(Newtype tc _ tbs t)) = do tvenv <- foldM (extendM Tv) eempty tbs - k <- checkTy (tcenv,tvenv) t - -- 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 + 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 - ch (Newtype _ _ _ Nothing) = - {- should only occur for recursive Newtypes -} - return cenv processCdef :: Cenv -> Tdef -> Cenv processCdef cenv = ch @@ -207,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 () @@ -227,67 +213,60 @@ 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 = +checkVdefg top_level (tcenv,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 - 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) + 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 == wrapperMainMname + enclosing == mainMname && defining == wrapperMainAnMname 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 @@ -295,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 @@ -328,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) @@ -337,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 @@ -345,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') @@ -381,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 @@ -393,23 +371,19 @@ 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 -> 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 @@ -443,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) @@ -466,7 +440,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 @@ -488,42 +462,21 @@ checkTy es@(tcenv,tvenv) t = ch 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 - -- (?->(?->*)). In general, I don't think 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) 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" ++ @@ -533,83 +486,83 @@ 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) - -{- 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 - 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) + 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) @@ -685,6 +638,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 @@ -692,13 +646,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 @@ -711,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