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) 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
23 {- Checking is done in a simple error monad. In addition to
24 allowing errors to be captured, this makes it easy to guarantee
25 that checking itself has been completed for an entire module. -}
27 {- We use the Reader monad transformer in order to thread the
28 top-level module name throughout the computation simply.
29 This is so that checkExp can also be an entry point (we call it
31 data CheckRes a = OkC a | FailC String
32 type CheckResult a = ReaderT (AnMname, Menv) CheckRes a
33 getMname :: CheckResult AnMname
34 getMname = ask >>= (return . fst)
35 getGlobalEnv :: CheckResult Menv
36 getGlobalEnv = ask >>= (return . snd)
38 instance Monad CheckRes where
40 FailC s >>= _ = fail s
44 require :: Bool -> String -> CheckResult ()
45 require False s = fail s
46 require True _ = return ()
49 extendM :: (Ord a, Show a) => Bool -> EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
50 extendM checkNameShadowing envType env (k,d) =
52 Just _ | envType == NotTv && checkNameShadowing -> fail ("multiply-defined identifier: "
54 _ -> return (eextend env (k,d))
56 extendVenv :: (Ord a, Show a) => Bool -> Env a b -> (a,b) -> CheckResult (Env a b)
57 extendVenv check = extendM check NotTv
59 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
60 extendTvenv = extendM True Tv
62 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult (Maybe b)
63 lookupM env k = return $ elookup env k
65 {- Main entry point. -}
66 checkModule :: Menv -> Module -> CheckRes Menv
67 checkModule globalEnv (Module mn tdefs vdefgs) =
69 (do (tcenv, cenv) <- mkTypeEnvs tdefs
70 (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))
73 return (eextend globalEnv
74 (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})))
77 -- Like checkModule, but doesn't typecheck the code, instead just
78 -- returning declared types for top-level defns.
79 -- This is necessary in order to handle circular dependencies, but it's sort
81 envsModule :: Menv -> Module -> Menv
82 envsModule globalEnv (Module mn tdefs vdefgs) =
83 let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
84 e_venv = foldr vdefgTypes eempty vdefgs in
85 eextend globalEnv (mn,
86 (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))
87 where vdefgTypes :: Vdefg -> Venv -> Venv
88 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
90 vdefgTypes (Rec vds) e =
91 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
92 add :: [(Qual Var,Ty)] -> Venv -> Venv
93 add pairs e = foldr addOne e pairs
94 addOne :: (Qual Var, Ty) -> Venv -> Venv
95 addOne ((_,v),t) e = eextend e (v,t)
97 checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
98 checkTdef0 tcenv tdef = ch tdef
100 ch (Data (m,c) tbs _) =
102 requireModulesEq m mn "data type declaration" tdef False
103 extendM True NotTv tcenv (c, Kind k)
104 where k = foldr Karrow Klifted (map snd tbs)
105 ch (Newtype (m,c) coVar tbs rhs) =
107 requireModulesEq m mn "newtype declaration" tdef False
108 tcenv' <- extendM True NotTv tcenv (c, Kind k)
109 -- add newtype axiom to env
110 tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
112 where k = foldr Karrow Klifted (map snd tbs)
114 processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
115 processTdef0NoChecking tcenv tdef = ch tdef
117 ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)
118 where k = foldr Karrow Klifted (map snd tbs)
119 ch (Newtype tc@(_,c) coercion tbs rhs) =
120 let tcenv' = eextend tcenv (c, Kind k) in
121 -- add newtype axiom to env
123 (snd coercion, Coercion $ DefinedCoercion tbs
124 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))
125 where k = foldr Karrow Klifted (map snd tbs)
127 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty
129 envPlusNewtype tcenv tyCon coVar tbs rep = extendM True NotTv tcenv
130 (snd coVar, Coercion $ DefinedCoercion tbs
131 (foldl Tapp (Tcon tyCon)
132 (map Tvar (fst (unzip tbs))),
135 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
136 checkTdef tcenv cenv = ch
138 ch (Data (_,c) utbs cdefs) =
139 do cbinds <- mapM checkCdef cdefs
140 foldM (extendM True NotTv) cenv cbinds
141 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
143 requireModulesEq m mn "constructor declaration" cdef
145 tvenv <- foldM (extendM True Tv) eempty tbs
146 ks <- mapM (checkTy (tcenv,tvenv)) ts
147 mapM_ (\k -> require (baseKind k)
148 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
149 "kind: " ++ show k) ) ks
151 where tbs = utbs ++ etbs
154 (foldl Tapp (Tcon (Just mn,c))
155 (map (Tvar . fst) utbs)) ts) tbs
156 ch (tdef@(Newtype tc _ tbs t)) =
157 do tvenv <- foldM (extendM True Tv) eempty tbs
158 kRhs <- checkTy (tcenv,tvenv) t
159 require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
160 kLhs <- checkTy (tcenv,tvenv)
161 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
162 require (kLhs `eqKind` kRhs)
163 ("Kind mismatch in newtype axiom types: " ++ show tdef
165 (show kLhs) ++ " and " ++ (show kRhs))
168 processCdef :: Cenv -> Tdef -> Cenv
169 processCdef cenv = ch
171 ch (Data (_,c) utbs cdefs) = do
172 let cbinds = map checkCdef cdefs
173 foldl eextend cenv cbinds
174 where checkCdef (Constr (mn,dcon) etbs ts) =
176 where tbs = utbs ++ etbs
179 (foldl Tapp (Tcon (mn,c))
180 (map (Tvar . fst) utbs)) ts) tbs
183 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)
184 mkTypeEnvs tdefs = do
185 tcenv <- foldM checkTdef0 eempty tdefs
186 cenv <- foldM (checkTdef tcenv) eempty tdefs
189 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
190 mkTypeEnvsNoChecking tdefs =
191 let tcenv = foldl processTdef0NoChecking eempty tdefs
192 cenv = foldl processCdef eempty tdefs in
195 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
196 -> Bool -> CheckResult ()
197 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
198 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
200 mkErrMsg :: Show a => String -> a -> String
201 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
203 checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)
204 -> Vdefg -> CheckResult (Venv,Venv)
205 checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
209 do (e_venv', l_venv') <- makeEnv mn vdefs
210 let env' = (tcenv,tvenv,cenv,e_venv',l_venv')
211 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
212 ("unlifted kind in:\n" ++ show vdef)) env')
214 return (e_venv', l_venv')
216 do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)
217 checkVdef (\ vdef k -> do
218 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
219 require ((not top_level) || (not (k `eqKind` Kunlifted)))
220 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
223 where makeEnv mn vdefs = do
224 ev <- foldM (extendVenv False) e_venv e_vts
225 lv <- foldM (extendVenv False) l_venv l_vts
227 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
228 not (vdefIsMainWrapper mn (Just m))]
229 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
230 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
232 let isZcMain = vdefIsMainWrapper mn m
234 requireModulesEq m mn "value definition" vdef True
235 k <- checkTy (tcenv,tvenv) t
239 ("declared type doesn't match expression type in:\n"
240 ++ show vdef ++ "\n" ++
241 "declared type: " ++ show t ++ "\n" ++
242 "expression type: " ++ show t')
244 vdefIsMainWrapper :: AnMname -> Mname -> Bool
245 vdefIsMainWrapper enclosing defining =
246 enclosing == mainMname && defining == wrapperMainAnMname
248 checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv
250 checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do
251 --(tcenv, cenv) <- mkTypeEnvs tdefs
252 -- Since the preprocessor calls checkExpr after code has been
253 -- typechecked, we expect to find the external env in the Menv.
254 case (elookup menv mn) of
256 checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e
257 Nothing -> reportError e ("checkExpr: Environment for " ++
258 show mn ++ " not found")) (mn,menv) of
260 FailC s -> reportError e s
262 checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind
263 checkType mn menv _tcenv tvenv t =
264 case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of
266 FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn)
268 checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
269 checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
274 qlookupM venv_ e_venv l_venv qv
276 qlookupM cenv_ cenv eempty qc
281 k' <- checkTy (tcenv,tvenv) t
284 do require (k' `subKindOf` k)
285 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
286 "operator kind: " ++ show k ++ "\n" ++
287 "operand kind: " ++ show k')
288 return (substl [tv] [t] t0)
289 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
290 "operator type: " ++ show t')
295 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
296 do require (t2 == t')
297 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
298 "operator type: " ++ show t' ++ "\n" ++
299 "operand type: " ++ show t2)
301 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
302 "operator type: " ++ show t1)
304 do tvenv' <- extendTvenv tvenv tb
305 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e
306 return (Tforall tb t)
307 Lam (Vb (vb@(_,vt))) e ->
308 do k <- checkTy (tcenv,tvenv) vt
310 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
312 l_venv' <- extendVenv True l_venv vb
313 t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e
314 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
317 do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
318 (e_venv,l_venv) vdefg
319 checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e
320 Case e (v,t) resultTy alts ->
322 checkTy (tcenv,tvenv) t
324 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
325 "declared type: " ++ show t ++ "\n" ++
326 "expression type: " ++ show t')
327 case (reverse alts) of
329 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
330 ("duplicate alternative in case:\n" ++ show e0)
332 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
333 ok [Adefault _] _ = return ()
334 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
338 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
339 ok ((Alit l _):as) ls = do require (notElem l ls)
340 ("duplicate alternative in case:\n" ++ show e0)
342 ok [Adefault _] _ = return ()
343 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
344 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
346 [Adefault _] -> return ()
347 _ -> fail ("no alternatives in case:\n" ++ show e0)
348 l_venv' <- extendVenv True l_venv (v,t)
349 t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
350 require (all (== t) ts)
351 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
352 "types: " ++ show (t:ts))
353 checkTy (tcenv,tvenv) resultTy
354 require (t == resultTy) ("case alternative type doesn't " ++
355 " match case return type in:\n" ++ show e0 ++ "\n" ++
356 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
360 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
361 require (eTy == fromTy) ("Type mismatch in cast: c = "
362 ++ show c ++ "\nand eTy = " ++ show eTy
363 ++ "\n and " ++ show fromTy)
368 do checkTy (tcenv,eempty) t {- external types must be closed -}
371 checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
372 checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
376 Acon qc etbs vbs e ->
378 where f (Tapp t0 t) = f t0 ++ [t]
380 ct <- qlookupM cenv_ cenv eempty qc
381 let (tbs,ct_args0,ct_res0) = splitTy ct
383 let (utbs,etbs') = splitAt (length uts) tbs
384 let utvs = map fst utbs
385 {- check existentials -}
386 let (etvs,eks) = unzip etbs
387 let (etvs',eks') = unzip etbs'
388 require (all (uncurry eqKind)
390 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
391 "kinds declared in data constructor: " ++ show eks ++
392 "kinds declared in case alternative: " ++ show eks')
393 tvenv' <- foldM extendTvenv tvenv etbs
394 {- check term variables -}
395 let vts = map snd vbs
396 mapM_ (\vt -> require ((not . isUtupleTy) vt)
397 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
398 "pattern type: " ++ show vt)) vts
399 vks <- mapM (checkTy (tcenv,tvenv')) vts
400 mapM_ (\vk -> require (baseKind vk)
401 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
402 "kind: " ++ show vk)) vks
403 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
406 require (ct_arg == vt)
407 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
408 "pattern variable type: " ++ show ct_arg ++ "\n" ++
409 "constructor argument type: " ++ show vt)) ct_args vts
410 require (ct_res == t0)
411 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
412 "pattern constructor type: " ++ show ct_res ++ "\n" ++
413 "scrutinee type: " ++ show t0)
414 l_venv' <- foldM (extendVenv True) l_venv vbs
415 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e
416 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
421 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
422 "pattern type: " ++ show t ++ "\n" ++
423 "scrutinee type: " ++ show t0)
428 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
429 checkTy es@(tcenv,tvenv) = ch
432 res <- lookupM tvenv tv
435 Nothing -> fail ("Undefined tvar: " ++ show tv)
437 kOrC <- qlookupM tcenv_ tcenv eempty qtc
440 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
441 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
442 ch (t@(Tapp t1 t2)) =
443 case splitTyConApp_maybe t of
445 tcK <- qlookupM tcenv_ tcenv eempty tc
447 Kind _ -> checkTapp t1 t2
448 Coercion co@(DefinedCoercion tbs _) -> do
449 -- makes sure coercion is fully applied
450 require (length tys == length tbs) $
451 ("Arity mismatch in coercion app: " ++ show t)
452 let (_, tks) = unzip tbs
453 argKs <- mapM (checkTy es) tys
454 let kPairs = zip argKs tks
455 -- Simon says it's okay for these to be
457 let kindsOk = all (uncurry subKindOf) kPairs
459 ("Kind mismatch in coercion app: " ++ show tks
460 ++ " and " ++ show argKs ++ " t = " ++ show t)
461 return $ (uncurry Keq) (applyNewtype co tys)
462 Nothing -> checkTapp t1 t2
463 where checkTapp t1 t2 = do
468 require (k2 `subKindOf` k11) kindError
471 "kinds don't match in type application: "
473 "operator kind: " ++ show k11 ++ "\n" ++
474 "operand kind: " ++ show k2
475 _ -> fail ("applied type has non-arrow kind: " ++ show t)
478 do tvenv' <- extendTvenv tvenv tb
479 checkTy (tcenv,tvenv') t
480 ch (TransCoercion t1 t2) = do
481 (ty1,ty2) <- checkTyCo es t1
482 (ty3,ty4) <- checkTyCo es t2
483 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
484 show ty2 ++ " and " ++ show ty3)
486 ch (SymCoercion t1) = do
487 (ty1,ty2) <- checkTyCo es t1
489 ch (UnsafeCoercion t1 t2) = do
493 ch (LeftCoercion t1) = do
496 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
497 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
498 ch (RightCoercion t1) = do
501 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
502 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
503 ch (InstCoercion ty arg) = do
504 forallK <- checkTyCo es ty
506 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
507 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
509 argK <- checkTy es arg
510 require (argK `eqKind` k1) ("Kind mismatch in type being "
511 ++ "instantiated: " ++ show arg)
512 let newLhs = substl [v1] [arg] b1
513 let newRhs = substl [v2] [arg] b2
514 return $ Keq newLhs newRhs
515 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
517 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
518 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
519 (case splitTyConApp_maybe t of
521 tcK <- qlookupM tcenv_ tcenv eempty tc
523 -- todo: avoid duplicating this code
524 -- blah, this almost calls for a different syntactic form
525 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
526 Coercion co@(DefinedCoercion tbs _) -> do
527 require (length tys == length tbs) $
528 ("Arity mismatch in coercion app: " ++ show t)
529 let (_, tks) = unzip tbs
530 argKs <- mapM (checkTy es) tys
531 let kPairs = zip argKs tks
532 let kindsOk = all (uncurry subKindOf) kPairs
534 ("Kind mismatch in coercion app: " ++ show tks
535 ++ " and " ++ show argKs ++ " t = " ++ show t)
536 return (applyNewtype co tys)
538 _ -> checkTapp t1 t2)
539 where checkTapp t1 t2 = do
540 (lhsRator, rhsRator) <- checkTyCo es t1
541 (lhs, rhs) <- checkTyCo es t2
542 -- Comp rule from paper
543 checkTy es (Tapp lhsRator lhs)
544 checkTy es (Tapp rhsRator rhs)
545 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
546 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
547 tvenv' <- extendTvenv tvenv tb
548 (t1,t2) <- checkTyCo (tcenv, tvenv') t
549 return (Tforall tb t1, Tforall tb t2)
553 Keq t1 t2 -> return (t1, t2)
554 -- otherwise, expand by the "refl" rule
557 mlookupM :: (Eq a, Show a, Show b) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
558 -> CheckResult (Env a b)
559 mlookupM _ _ local_env Nothing = -- (trace ("mlookupM_: returning " ++ show local_env)) $
561 mlookupM selector external_env local_env (Just m) = do
563 globalEnv <- getGlobalEnv
565 then -- trace ("global env would b e " ++ show (elookup globalEnv m)) $
568 case elookup globalEnv m of
569 Just env' -> return (selector env')
570 Nothing -> fail ("Check: undefined module name: "
571 ++ show m ++ show (edomain local_env))
573 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
574 -> Qual a -> CheckResult b
575 qlookupM selector external_env local_env v@(m,k) =
576 do env <- -- trace ("qlookupM: " ++ show v) $
577 mlookupM selector external_env local_env m
578 -- argh, hack for unqualified top-level names
579 maybeRes <- lookupM env k
582 Nothing -> do mn <- getMname
583 currentMenv <- -- trace ("qlookupM: trying module for " ++ show mn) $
584 mlookupM selector external_env local_env (Just mn)
585 maybeRes1 <- -- trace ("qlookupM: trying in " ++ show currentMenv) $
586 lookupM currentMenv k
590 globalEnv <- getGlobalEnv
591 case elookup globalEnv mn of
592 Just e1 -> case elookup (selector e1) k of
594 Nothing -> fail ("Undefined id " ++ show v)
595 Nothing -> fail ("Undefined id " ++ show v)
597 checkLit :: Lit -> CheckResult Ty
598 checkLit (Literal lit t) =
601 do require (t `elem` intLitTypes)
602 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
605 do require (t `elem` ratLitTypes)
606 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
609 do require (t `elem` charLitTypes)
610 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
613 do require (t `elem` stringLitTypes)
614 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
619 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
620 splitTy :: Ty -> ([Tbind],[Ty],Ty)
621 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
622 where (tbs,ts,tr) = splitTy t
623 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
624 where (tbs,ts,tr) = splitTy t
625 splitTy t = ([],[],t)
628 primCoercionError :: Show a => a -> b
629 primCoercionError s = error $ "Bad coercion application: " ++ show s
632 reportError :: Show a => a -> String -> b
633 reportError e s = error $ ("Core type error: checkExpr failed with "
634 ++ s ++ " and " ++ show e)