+{-# OPTIONS -Wall -fno-warn-name-shadowing #-}
+module Language.Core.Check(
+ checkModule, envsModule,
+ checkExpr, checkType,
+ primCoercionError,
+ Menv, Venv, Tvenv, Envs(..),
+ CheckRes(..), splitTy, substl) where
+
+import Language.Core.Core
+import Language.Core.Printer()
+import Language.Core.PrimEnv
+import Language.Core.Env
+
+import Control.Monad.Reader
+import Data.List
+import Data.Maybe
+
+{- 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. -}
+
+{- 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 CheckRes where
+ OkC a >>= k = k a
+ FailC s >>= _ = fail s
+ return = OkC
+ fail = FailC
+
+require :: Bool -> String -> CheckResult ()
+require False s = fail s
+require True _ = return ()
+
+{- Environments. -}
+type Tvenv = Env Tvar Kind -- type variables (local only)
+type Tcenv = Env Tcon KindOrCoercion -- type constructors
+type Cenv = Env Dcon Ty -- data constructors
+type Venv = Env Var Ty -- values
+type Menv = Env AnMname Envs -- modules
+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
+ variables -- shadowing type variables is allowed.) -}
+data EnvType = Tv | NotTv
+ deriving Eq
+
+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 _ | 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 =
+ case elookup env k of
+ Just v -> return v
+ Nothing -> fail ("undefined identifier: " ++ show k)
+
+{- Main entry point. -}
+checkModule :: Menv -> Module -> CheckRes Menv
+checkModule globalEnv (Module mn tdefs vdefgs) =
+ runReaderT
+ (do (tcenv, cenv) <- mkTypeEnvs tdefs
+ (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))
+ (eempty,eempty)
+ vdefgs
+ return (eextend 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.
+-- 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, cenv) = mkTypeEnvsNoChecking tdefs
+ e_venv = foldr vdefgTypes eempty vdefgs in
+ eextend globalEnv (mn,
+ (Envs{tcenv_=tcenv,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 -> 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
+ extendM NotTv tcenv (c, Kind k)
+ where k = foldr Karrow Klifted (map snd tbs)
+ 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'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
+ return tcenv''
+ where k = foldr Karrow Klifted (map snd tbs)
+
+processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
+processTdef0NoChecking tcenv tdef = ch tdef
+ where
+ 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) in
+ -- add newtype axiom to env
+ 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
+ where
+ ch (Data (_,c) utbs cdefs) =
+ do cbinds <- mapM checkCdef cdefs
+ foldM (extendM NotTv) cenv cbinds
+ where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
+ 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 mn)
+ where tbs = utbs ++ etbs
+ t mn = foldr Tforall
+ (foldr tArrow
+ (foldl Tapp (Tcon (Just mn,c))
+ (map (Tvar . fst) utbs)) ts) tbs
+ 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)
+ 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
+
+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, Cenv)
+mkTypeEnvs tdefs = do
+ tcenv <- foldM checkTdef0 eempty tdefs
+ cenv <- foldM (checkTdef tcenv) eempty tdefs
+ return (tcenv, cenv)
+
+mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
+mkTypeEnvsNoChecking tdefs =
+ let tcenv = foldl processTdef0NoChecking eempty tdefs
+ cenv = foldl processCdef eempty tdefs in
+ (tcenv, 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,Tvenv,Cenv) -> (Venv,Venv)
+ -> Vdefg -> CheckResult (Venv,Venv)
+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,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 == wrapperMainAnMname
+
+checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
+ -> Exp -> Ty
+checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
+ (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, 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,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
+checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
+ where
+ ch e0 =
+ case e0 of
+ Var qv ->
+ qlookupM venv_ e_venv l_venv qv
+ Dcon qc ->
+ qlookupM cenv_ cenv eempty qc
+ Lit l ->
+ checkLit l
+ Appt e t ->
+ do t' <- ch e
+ k' <- checkTy (tcenv,tvenv) t
+ case t' of
+ Tforall (tv,k) t0 ->
+ 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')
+ return (substl [tv] [t] t0)
+ _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t')
+ App e1 e2 ->
+ do t1 <- ch e1
+ t2 <- ch e2
+ case t1 of
+ Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
+ do require (t2 == t')
+ ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t' ++ "\n" ++
+ "operand type: " ++ show t2)
+ return t0
+ _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
+ "operator type: " ++ show t1)
+ Lam (Tb tb) e ->
+ do tvenv' <- extendTvenv tvenv tb
+ 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
+ require (baseKind k)
+ ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
+ "kind: " ++ show k)
+ l_venv' <- extendVenv l_venv vb
+ 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,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
+ 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')
+ case (reverse alts) of
+ (Acon c _ _ _):as ->
+ let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
+ ("duplicate alternative in case:\n" ++ show e0)
+ ok as (c:cs)
+ ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
+ ok [Adefault _] _ = return ()
+ ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
+ ok [] _ = return ()
+ in ok as [c]
+ (Alit l _):as ->
+ let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
+ ok ((Alit l _):as) ls = do require (notElem l ls)
+ ("duplicate alternative in case:\n" ++ show e0)
+ ok as (l:ls)
+ ok [Adefault _] _ = return ()
+ ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
+ 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' <- extendVenv l_venv (v,t)
+ 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
+ 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
+ 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,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
+ Acon qc etbs vbs e ->
+ do let uts = f t0
+ where f (Tapp t0 t) = f t0 ++ [t]
+ f _ = []
+ ct <- qlookupM cenv_ cenv eempty qc
+ let (tbs,ct_args0,ct_res0) = splitTy ct
+ {- get universals -}
+ let (utbs,etbs') = splitAt (length uts) tbs
+ let utvs = map fst utbs
+ {- check existentials -}
+ let (etvs,eks) = unzip etbs
+ let (etvs',eks') = unzip etbs'
+ 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 extendTvenv tvenv etbs
+ {- check term variables -}
+ let vts = map snd vbs
+ mapM_ (\vt -> require ((not . isUtupleTy) vt)
+ ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
+ "pattern type: " ++ show vt)) vts
+ vks <- mapM (checkTy (tcenv,tvenv')) vts
+ mapM_ (\vk -> require (baseKind vk)
+ ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
+ "kind: " ++ show vk)) vks
+ let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
+ zipWithM_
+ (\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
+ 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,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
+ require (t == t0)
+ ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
+ "pattern type: " ++ show t ++ "\n" ++
+ "scrutinee type: " ++ show t0)
+ checkExp env e
+ Adefault e ->
+ checkExp env e
+
+checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
+checkTy es@(tcenv,tvenv) = ch
+ where
+ ch (Tvar tv) = lookupM tvenv tv
+ 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)) =
+ 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
+ -- 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
+ 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' <- 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 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)
+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 (Literal lit t) =
+ case lit of
+ Lint _ ->
+ do require (t `elem` intLitTypes)
+ ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
+ return t
+ Lrational _ ->
+ do require (t `elem` ratLitTypes)
+ ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
+ return t
+ Lchar _ ->
+ do require (t `elem` charLitTypes)
+ ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
+ return t
+ Lstring _ ->
+ do require (t `elem` stringLitTypes)
+ ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
+ return t
+
+{- Utilities -}
+
+{- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
+splitTy :: Ty -> ([Tbind],[Ty],Ty)
+splitTy (Tforall tb t) = (tb:tbs,ts,tr)
+ where (tbs,ts,tr) = splitTy t
+splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
+ where (tbs,ts,tr) = splitTy t
+splitTy t = ([],[],t)
+
+
+{- Simultaneous substitution on types for type variables,
+ renaming as neceessary to avoid capture.
+ No checks for correct kindedness. -}
+substl :: [Tvar] -> [Ty] -> Ty -> Ty
+substl tvs ts t = f (zip tvs ts) t
+ where
+ f env t0 =
+ case t0 of
+ Tcon _ -> t0
+ Tvar v -> case lookup v env of
+ Just t1 -> t1
+ Nothing -> t0
+ Tapp t1 t2 -> Tapp (f env t1) (f env t2)
+ Tforall (t,k) t1 ->
+ if t `elem` free then
+ 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
+
+{- Return free tvars in a type -}
+freeTvars :: Ty -> [Tvar]
+freeTvars (Tcon _) = []
+freeTvars (Tvar v) = [v]
+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)
projects / ghc-hetmet.git / blobdiff