1 {-# OPTIONS -Wall -fno-warn-name-shadowing #-}
2 module Language.Core.Check(
3 checkModule, envsModule,
6 Menv, Venv, Tvenv, Envs(..),
7 CheckRes(..), splitTy, substl,
8 mkTypeEnvsNoChecking, NtEnv, mkNtEnv) where
12 import Language.Core.Core
13 import Language.Core.CoreUtils
14 import Language.Core.Printer()
15 import Language.Core.PrimEnv
16 import Language.Core.Env
17 import Language.Core.Environments
19 import Control.Monad.Reader
21 import qualified Data.Map as M
24 {- Checking is done in a simple error monad. In addition to
25 allowing errors to be captured, this makes it easy to guarantee
26 that checking itself has been completed for an entire module. -}
28 {- We use the Reader monad transformer in order to thread the
29 top-level module name throughout the computation simply.
30 This is so that checkExp can also be an entry point (we call it
32 data CheckRes a = OkC a | FailC String
33 type CheckResult a = ReaderT (AnMname, Menv) CheckRes a
34 getMname :: CheckResult AnMname
35 getMname = ask >>= (return . fst)
36 getGlobalEnv :: CheckResult Menv
37 getGlobalEnv = ask >>= (return . snd)
39 instance Monad CheckRes where
41 FailC s >>= _ = fail s
45 require :: Bool -> String -> CheckResult ()
46 require False s = fail s
47 require True _ = return ()
50 extendM :: (Ord a, Show a) => Bool -> EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
51 extendM checkNameShadowing envType env (k,d) =
53 Just _ | envType == NotTv && checkNameShadowing -> fail ("multiply-defined identifier: "
55 _ -> return (eextend env (k,d))
57 extendVenv :: (Ord a, Show a) => Bool -> Env a b -> (a,b) -> CheckResult (Env a b)
58 extendVenv check = extendM check NotTv
60 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
61 extendTvenv = extendM True Tv
63 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult (Maybe b)
64 lookupM env k = return $ elookup env k
66 {- Main entry point. -}
67 checkModule :: Menv -> Module -> CheckRes Menv
68 checkModule globalEnv (Module mn tdefs vdefgs) =
70 (do (tcenv, cenv) <- mkTypeEnvs tdefs
71 (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))
74 return (eextend globalEnv
75 (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})))
78 -- Like checkModule, but doesn't typecheck the code, instead just
79 -- returning declared types for top-level defns.
80 -- This is necessary in order to handle circular dependencies, but it's sort
82 envsModule :: Menv -> Module -> Menv
83 envsModule globalEnv (Module mn tdefs vdefgs) =
84 let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
85 e_venv = foldr vdefgTypes eempty vdefgs in
86 eextend globalEnv (mn,
87 (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))
88 where vdefgTypes :: Vdefg -> Venv -> Venv
89 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
91 vdefgTypes (Rec vds) e =
92 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
93 add :: [(Qual Var,Ty)] -> Venv -> Venv
94 add pairs e = foldr addOne e pairs
95 addOne :: (Qual Var, Ty) -> Venv -> Venv
96 addOne ((_,v),t) e = eextend e (v,t)
98 checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
99 checkTdef0 tcenv tdef = ch tdef
101 ch (Data (m,c) tbs _) =
103 requireModulesEq m mn "data type declaration" tdef False
104 extendM True NotTv tcenv (c, Kind k)
105 where k = foldr Karrow Klifted (map snd tbs)
106 ch (Newtype (m,c) coVar tbs rhs) =
108 requireModulesEq m mn "newtype declaration" tdef False
109 tcenv' <- extendM True NotTv tcenv (c, Kind k)
110 -- add newtype axiom to env
111 tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
113 where k = foldr Karrow Klifted (map snd tbs)
115 processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
116 processTdef0NoChecking tcenv tdef = ch tdef
118 ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)
119 where k = foldr Karrow Klifted (map snd tbs)
120 ch (Newtype tc@(_,c) coercion tbs rhs) =
121 let tcenv' = eextend tcenv (c, Kind k) in
122 -- add newtype axiom to env
124 (snd coercion, Coercion $ DefinedCoercion tbs
125 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))
126 where k = foldr Karrow Klifted (map snd tbs)
128 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty
130 envPlusNewtype tcenv tyCon coVar tbs rep = extendM True NotTv tcenv
131 (snd coVar, Coercion $ DefinedCoercion tbs
132 (foldl Tapp (Tcon tyCon)
133 (map Tvar (fst (unzip tbs))),
136 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
137 checkTdef tcenv cenv = ch
139 ch (Data (_,c) utbs cdefs) =
140 do cbinds <- mapM checkCdef cdefs
141 foldM (extendM True NotTv) cenv cbinds
142 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
144 requireModulesEq m mn "constructor declaration" cdef
146 tvenv <- foldM (extendM True Tv) eempty tbs
147 ks <- mapM (checkTy (tcenv,tvenv)) ts
148 mapM_ (\k -> require (baseKind k)
149 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
150 "kind: " ++ show k) ) ks
152 where tbs = utbs ++ etbs
155 (foldl Tapp (Tcon (Just mn,c))
156 (map (Tvar . fst) utbs)) ts) tbs
157 ch (tdef@(Newtype tc _ tbs t)) =
158 do tvenv <- foldM (extendM True Tv) eempty tbs
159 kRhs <- checkTy (tcenv,tvenv) t
160 require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
161 kLhs <- checkTy (tcenv,tvenv)
162 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
163 require (kLhs `eqKind` kRhs)
164 ("Kind mismatch in newtype axiom types: " ++ show tdef
166 (show kLhs) ++ " and " ++ (show kRhs))
169 processCdef :: Cenv -> Tdef -> Cenv
170 processCdef cenv = ch
172 ch (Data (_,c) utbs cdefs) = do
173 let cbinds = map checkCdef cdefs
174 foldl eextend cenv cbinds
175 where checkCdef (Constr (mn,dcon) etbs ts) =
177 where tbs = utbs ++ etbs
180 (foldl Tapp (Tcon (mn,c))
181 (map (Tvar . fst) utbs)) ts) tbs
184 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)
185 mkTypeEnvs tdefs = do
186 tcenv <- foldM checkTdef0 eempty tdefs
187 cenv <- foldM (checkTdef tcenv) eempty tdefs
190 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
191 mkTypeEnvsNoChecking tdefs =
192 let tcenv = foldl processTdef0NoChecking eempty tdefs
193 cenv = foldl processCdef eempty tdefs in
196 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
197 -> Bool -> CheckResult ()
198 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
199 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
201 mkErrMsg :: Show a => String -> a -> String
202 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
204 checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)
205 -> Vdefg -> CheckResult (Venv,Venv)
206 checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
210 do (e_venv', l_venv') <- makeEnv mn vdefs
211 let env' = (tcenv,tvenv,cenv,e_venv',l_venv')
212 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
213 ("unlifted kind in:\n" ++ show vdef)) env')
215 return (e_venv', l_venv')
217 do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)
218 checkVdef (\ vdef k -> do
219 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
220 require ((not top_level) || (not (k `eqKind` Kunlifted)))
221 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
224 where makeEnv mn vdefs = do
225 ev <- foldM (extendVenv False) e_venv e_vts
226 lv <- foldM (extendVenv False) l_venv l_vts
228 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
229 not (vdefIsMainWrapper mn (Just m))]
230 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
231 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
233 let isZcMain = vdefIsMainWrapper mn m
235 requireModulesEq m mn "value definition" vdef True
236 k <- checkTy (tcenv,tvenv) t
240 ("declared type doesn't match expression type in:\n"
241 ++ show vdef ++ "\n" ++
242 "declared type: " ++ show t ++ "\n" ++
243 "expression type: " ++ show t')
245 vdefIsMainWrapper :: AnMname -> Mname -> Bool
246 vdefIsMainWrapper enclosing defining =
247 enclosing == mainMname && defining == wrapperMainAnMname
249 checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv
251 checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do
252 --(tcenv, cenv) <- mkTypeEnvs tdefs
253 -- Since the preprocessor calls checkExpr after code has been
254 -- typechecked, we expect to find the external env in the Menv.
255 case (elookup menv mn) of
257 checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e
258 Nothing -> reportError e ("checkExpr: Environment for " ++
259 show mn ++ " not found")) (mn,menv) of
261 FailC s -> reportError e s
263 checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind
264 checkType mn menv _tcenv tvenv t =
265 case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of
267 FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn)
269 checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
270 checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
275 qlookupM venv_ e_venv l_venv qv
277 qlookupM cenv_ cenv eempty qc
282 k' <- checkTy (tcenv,tvenv) t
285 do require (k' `subKindOf` k)
286 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
287 "operator kind: " ++ show k ++ "\n" ++
288 "operand kind: " ++ show k')
289 return (substl [tv] [t] t0)
290 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
291 "operator type: " ++ show t')
296 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
297 do require (t2 == t')
298 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
299 "operator type: " ++ show t' ++ "\n" ++
300 "operand type: " ++ show t2)
302 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
303 "operator type: " ++ show t1)
305 do tvenv' <- extendTvenv tvenv tb
306 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e
307 return (Tforall tb t)
308 Lam (Vb (vb@(_,vt))) e ->
309 do k <- checkTy (tcenv,tvenv) vt
311 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
313 l_venv' <- extendVenv True l_venv vb
314 t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e
315 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
318 do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
319 (e_venv,l_venv) vdefg
320 checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e
321 Case e (v,t) resultTy alts ->
323 checkTy (tcenv,tvenv) t
325 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
326 "declared type: " ++ show t ++ "\n" ++
327 "expression type: " ++ show t')
328 case (reverse alts) of
330 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
331 ("duplicate alternative in case:\n" ++ show e0)
333 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
334 ok [Adefault _] _ = return ()
335 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
339 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
340 ok ((Alit l _):as) ls = do require (notElem l ls)
341 ("duplicate alternative in case:\n" ++ show e0)
343 ok [Adefault _] _ = return ()
344 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
345 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
347 [Adefault _] -> return ()
348 _ -> fail ("no alternatives in case:\n" ++ show e0)
349 l_venv' <- extendVenv True l_venv (v,t)
350 t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
351 require (all (== t) ts)
352 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
353 "types: " ++ show (t:ts))
354 checkTy (tcenv,tvenv) resultTy
355 require (t == resultTy) ("case alternative type doesn't " ++
356 " match case return type in:\n" ++ show e0 ++ "\n" ++
357 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
361 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
362 require (eTy == fromTy) ("Type mismatch in cast: c = "
363 ++ show c ++ "\nand eTy = " ++ show eTy
364 ++ "\n and " ++ show fromTy)
369 do checkTy (tcenv,eempty) t {- external types must be closed -}
372 checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
373 checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
377 Acon qc etbs vbs e ->
379 where f (Tapp t0 t) = f t0 ++ [t]
381 ct <- qlookupM cenv_ cenv eempty qc
382 let (tbs,ct_args0,ct_res0) = splitTy ct
384 let (utbs,etbs') = splitAt (length uts) tbs
385 let utvs = map fst utbs
386 {- check existentials -}
387 let (etvs,eks) = unzip etbs
388 let (etvs',eks') = unzip etbs'
389 require (all (uncurry eqKind)
391 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
392 "kinds declared in data constructor: " ++ show eks ++
393 "kinds declared in case alternative: " ++ show eks')
394 tvenv' <- foldM extendTvenv tvenv etbs
395 {- check term variables -}
396 let vts = map snd vbs
397 mapM_ (\vt -> require ((not . isUtupleTy) vt)
398 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
399 "pattern type: " ++ show vt)) vts
400 vks <- mapM (checkTy (tcenv,tvenv')) vts
401 mapM_ (\vk -> require (baseKind vk)
402 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
403 "kind: " ++ show vk)) vks
404 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
407 require (ct_arg == vt)
408 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
409 "pattern variable type: " ++ show ct_arg ++ "\n" ++
410 "constructor argument type: " ++ show vt)) ct_args vts
411 require (ct_res == t0)
412 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
413 "pattern constructor type: " ++ show ct_res ++ "\n" ++
414 "scrutinee type: " ++ show t0)
415 l_venv' <- foldM (extendVenv True) l_venv vbs
416 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e
417 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
422 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
423 "pattern type: " ++ show t ++ "\n" ++
424 "scrutinee type: " ++ show t0)
429 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
430 checkTy es@(tcenv,tvenv) = ch
433 res <- lookupM tvenv tv
436 Nothing -> fail ("Undefined tvar: " ++ show tv)
438 kOrC <- qlookupM tcenv_ tcenv eempty qtc
441 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
442 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
443 ch (t@(Tapp t1 t2)) =
444 case splitTyConApp_maybe t of
446 tcK <- qlookupM tcenv_ tcenv eempty tc
448 Kind _ -> checkTapp t1 t2
449 Coercion co@(DefinedCoercion tbs _) -> do
450 -- makes sure coercion is fully applied
451 require (length tys == length tbs) $
452 ("Arity mismatch in coercion app: " ++ show t)
453 let (_, tks) = unzip tbs
454 argKs <- mapM (checkTy es) tys
455 let kPairs = zip argKs tks
456 -- Simon says it's okay for these to be
458 let kindsOk = all (uncurry subKindOf) kPairs
460 ("Kind mismatch in coercion app: " ++ show tks
461 ++ " and " ++ show argKs ++ " t = " ++ show t)
462 return $ (uncurry Keq) (applyNewtype co tys)
463 Nothing -> checkTapp t1 t2
464 where checkTapp t1 t2 = do
469 require (k2 `subKindOf` k11) kindError
472 "kinds don't match in type application: "
474 "operator kind: " ++ show k11 ++ "\n" ++
475 "operand kind: " ++ show k2
476 _ -> fail ("applied type has non-arrow kind: " ++ show t)
479 do tvenv' <- extendTvenv tvenv tb
480 checkTy (tcenv,tvenv') t
481 ch (TransCoercion t1 t2) = do
482 (ty1,ty2) <- checkTyCo es t1
483 (ty3,ty4) <- checkTyCo es t2
484 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
485 show ty2 ++ " and " ++ show ty3)
487 ch (SymCoercion t1) = do
488 (ty1,ty2) <- checkTyCo es t1
490 ch (UnsafeCoercion t1 t2) = do
494 ch (LeftCoercion t1) = do
497 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
498 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
499 ch (RightCoercion t1) = do
502 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
503 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
504 ch (InstCoercion ty arg) = do
505 forallK <- checkTyCo es ty
507 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
508 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
510 argK <- checkTy es arg
511 require (argK `eqKind` k1) ("Kind mismatch in type being "
512 ++ "instantiated: " ++ show arg)
513 let newLhs = substl [v1] [arg] b1
514 let newRhs = substl [v2] [arg] b2
515 return $ Keq newLhs newRhs
516 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
518 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
519 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
520 (case splitTyConApp_maybe t of
522 tcK <- qlookupM tcenv_ tcenv eempty tc
524 -- todo: avoid duplicating this code
525 -- blah, this almost calls for a different syntactic form
526 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
527 Coercion co@(DefinedCoercion tbs _) -> do
528 require (length tys == length tbs) $
529 ("Arity mismatch in coercion app: " ++ show t)
530 let (_, tks) = unzip tbs
531 argKs <- mapM (checkTy es) tys
532 let kPairs = zip argKs tks
533 let kindsOk = all (uncurry subKindOf) kPairs
535 ("Kind mismatch in coercion app: " ++ show tks
536 ++ " and " ++ show argKs ++ " t = " ++ show t)
537 return (applyNewtype co tys)
539 _ -> checkTapp t1 t2)
540 where checkTapp t1 t2 = do
541 (lhsRator, rhsRator) <- checkTyCo es t1
542 (lhs, rhs) <- checkTyCo es t2
543 -- Comp rule from paper
544 checkTy es (Tapp lhsRator lhs)
545 checkTy es (Tapp rhsRator rhs)
546 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
547 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
548 tvenv' <- extendTvenv tvenv tb
549 (t1,t2) <- checkTyCo (tcenv, tvenv') t
550 return (Tforall tb t1, Tforall tb t2)
554 Keq t1 t2 -> return (t1, t2)
555 -- otherwise, expand by the "refl" rule
558 mlookupM :: (Eq a, Show a, Show b) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
559 -> CheckResult (Env a b)
560 mlookupM _ _ local_env Nothing = -- (trace ("mlookupM_: returning " ++ show local_env)) $
562 mlookupM selector external_env local_env (Just m) = do
564 globalEnv <- getGlobalEnv
566 then -- trace ("global env would b e " ++ show (elookup globalEnv m)) $
569 case elookup globalEnv m of
570 Just env' -> return (selector env')
571 Nothing -> fail ("Check: undefined module name: "
572 ++ show m ++ show (edomain local_env))
574 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
575 -> Qual a -> CheckResult b
576 qlookupM selector external_env local_env v@(m,k) =
577 do env <- -- trace ("qlookupM: " ++ show v) $
578 mlookupM selector external_env local_env m
579 -- argh, hack for unqualified top-level names
580 maybeRes <- lookupM env k
583 Nothing -> do mn <- getMname
584 currentMenv <- -- trace ("qlookupM: trying module for " ++ show mn) $
585 mlookupM selector external_env local_env (Just mn)
586 maybeRes1 <- -- trace ("qlookupM: trying in " ++ show currentMenv) $
587 lookupM currentMenv k
591 globalEnv <- getGlobalEnv
592 case elookup globalEnv mn of
593 Just e1 -> case elookup (selector e1) k of
595 Nothing -> fail ("Undefined id " ++ show v)
596 Nothing -> fail ("Undefined id " ++ show v)
598 checkLit :: Lit -> CheckResult Ty
599 checkLit (Literal lit t) =
602 do require (t `elem` intLitTypes)
603 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
606 do require (t `elem` ratLitTypes)
607 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
610 do require (t `elem` charLitTypes)
611 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
614 do require (t `elem` stringLitTypes)
615 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
620 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
621 splitTy :: Ty -> ([Tbind],[Ty],Ty)
622 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
623 where (tbs,ts,tr) = splitTy t
624 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
625 where (tbs,ts,tr) = splitTy t
626 splitTy t = ([],[],t)
629 primCoercionError :: Show a => a -> b
630 primCoercionError s = error $ "Bad coercion application: " ++ show s
633 reportError :: Show a => a -> String -> b
634 reportError e s = error $ ("Core type error: checkExpr failed with "
635 ++ s ++ " and " ++ show e)
637 type NtEnv = M.Map Tcon CoercionKind
639 mkNtEnv :: Menv -> NtEnv
641 foldl M.union M.empty $
643 foldr (\ (_,thing) rest ->
646 Coercion d@(DefinedCoercion _ (lhs,_)) ->
647 case splitTyConApp_maybe lhs of
648 Just ((_,tc1),_) -> M.insert tc1 d rest
649 _ -> rest) M.empty (etolist (tcenv_ e))) (etolist menv)