import Maybe
import Control.Monad.Reader
--- just for printing warnings
-import System.IO.Unsafe
import Core
import Printer()
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
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)
-- 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
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
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))),
(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)
++ " 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
(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 ()
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)))
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" ++
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
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
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)
"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
("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')
[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
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
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)
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)
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)
-- 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
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