1 {-# OPTIONS -Wall -fno-warn-name-shadowing #-}
3 checkModule, envsModule,
6 Menv, Venv, Tvenv, Envs(..),
7 CheckRes(..), splitTy, substl) where
10 import Control.Monad.Reader
18 {- Checking is done in a simple error monad. In addition to
19 allowing errors to be captured, this makes it easy to guarantee
20 that checking itself has been completed for an entire module. -}
22 {- We use the Reader monad transformer in order to thread the
23 top-level module name throughout the computation simply.
24 This is so that checkExp can also be an entry point (we call it
26 data CheckRes a = OkC a | FailC String
27 type CheckResult a = ReaderT (AnMname, Menv) CheckRes a
28 getMname :: CheckResult AnMname
29 getMname = ask >>= (return . fst)
30 getGlobalEnv :: CheckResult Menv
31 getGlobalEnv = ask >>= (return . snd)
33 instance Monad CheckRes where
35 FailC s >>= _ = fail s
39 require :: Bool -> String -> CheckResult ()
40 require False s = fail s
41 require True _ = return ()
43 requireM :: CheckResult Bool -> String -> CheckResult ()
49 type Tvenv = Env Tvar Kind -- type variables (local only)
50 type Tcenv = Env Tcon KindOrCoercion -- type constructors
51 type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms
52 type Cenv = Env Dcon Ty -- data constructors
53 type Venv = Env Var Ty -- values
54 type Menv = Env AnMname Envs -- modules
55 data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
58 {- Extend an environment, checking for illegal shadowing of identifiers (for term
59 variables -- shadowing type variables is allowed.) -}
60 data EnvType = Tv | NotTv
63 extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
64 extendM envType env (k,d) =
66 Just _ | envType == NotTv -> fail ("multiply-defined identifier: "
68 _ -> return (eextend env (k,d))
70 extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
71 extendVenv = extendM NotTv
73 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
74 extendTvenv = extendM Tv
76 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
80 Nothing -> fail ("undefined identifier: " ++ show k)
82 {- Main entry point. -}
83 checkModule :: Menv -> Module -> CheckRes Menv
84 checkModule globalEnv (Module mn tdefs vdefgs) =
86 (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
87 (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
90 return (eextend globalEnv
91 (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})))
94 -- Like checkModule, but doesn't typecheck the code, instead just
95 -- returning declared types for top-level defns.
96 -- This is necessary in order to handle circular dependencies, but it's sort
98 envsModule :: Menv -> Module -> Menv
99 envsModule globalEnv (Module mn tdefs vdefgs) =
100 let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs
101 e_venv = foldr vdefgTypes eempty vdefgs in
102 eextend globalEnv (mn,
103 (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
104 where vdefgTypes :: Vdefg -> Venv -> Venv
105 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
107 vdefgTypes (Rec vds) e =
108 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
109 add :: [(Qual Var,Ty)] -> Venv -> Venv
110 add pairs e = foldr addOne e pairs
111 addOne :: (Qual Var, Ty) -> Venv -> Venv
112 addOne ((Nothing,_),_) e = e
113 addOne ((Just _,v),t) e = eextend e (v,t)
115 checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
116 checkTdef0 (tcenv,tsenv) tdef = ch tdef
118 ch (Data (m,c) tbs _) =
120 requireModulesEq m mn "data type declaration" tdef False
121 tcenv' <- extendM NotTv tcenv (c, Kind k)
122 return (tcenv',tsenv)
123 where k = foldr Karrow Klifted (map snd tbs)
124 ch (Newtype (m,c) tbs ((_,coercion),cTbs,coercionKind) rhs) =
126 requireModulesEq m mn "newtype declaration" tdef False
127 tcenv' <- extendM NotTv tcenv (c, Kind k)
128 -- add newtype axiom to env
129 tcenv'' <- extendM NotTv tcenv'
130 (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
131 tsenv' <- case rhs of
132 Nothing -> return tsenv
133 Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
134 return (tcenv'', tsenv')
135 where k = foldr Karrow Klifted (map snd tbs)
137 processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
138 processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
140 ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
141 where k = foldr Karrow Klifted (map snd tbs)
142 ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) =
143 let tcenv' = eextend tcenv (c, Kind k)
144 -- add newtype axiom to env
145 tcenv'' = eextend tcenv'
146 (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
148 (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
150 where k = foldr Karrow Klifted (map snd tbs)
152 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
153 checkTdef tcenv cenv = ch
155 ch (Data (_,c) utbs cdefs) =
156 do cbinds <- mapM checkCdef cdefs
157 foldM (extendM NotTv) cenv cbinds
158 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
160 requireModulesEq m mn "constructor declaration" cdef
162 tvenv <- foldM (extendM Tv) eempty tbs
163 ks <- mapM (checkTy (tcenv,tvenv)) ts
164 mapM_ (\k -> require (baseKind k)
165 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
166 "kind: " ++ show k) ) ks
168 where tbs = utbs ++ etbs
171 (foldl Tapp (Tcon (Just mn,c))
172 (map (Tvar . fst) utbs)) ts) tbs
173 ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) =
174 do tvenv <- foldM (extendM Tv) eempty tbs
175 k <- checkTy (tcenv,tvenv) t
176 -- Makes sure GHC is eta-expanding things properly
177 require (length tbs == length coTbs) $
178 ("Arity mismatch between newtycon and newtype coercion: "
180 require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
181 axiomTvenv <- foldM (extendM Tv) eempty coTbs
182 kLhs <- checkTy (tcenv,axiomTvenv) coLhs
183 kRhs <- checkTy (tcenv,axiomTvenv) coRhs
184 require (kLhs `eqKind` kRhs)
185 ("Kind mismatch in newtype axiom types: " ++ show tdef
187 (show kLhs) ++ " and " ++ (show kRhs))
189 ch (Newtype _ _ _ Nothing) =
190 {- should only occur for recursive Newtypes -}
193 processCdef :: Cenv -> Tdef -> Cenv
194 processCdef cenv = ch
196 ch (Data (_,c) utbs cdefs) = do
197 let cbinds = map checkCdef cdefs
198 foldl eextend cenv cbinds
199 where checkCdef (Constr (mn,dcon) etbs ts) =
201 where tbs = utbs ++ etbs
204 (foldl Tapp (Tcon (mn,c))
205 (map (Tvar . fst) utbs)) ts) tbs
208 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv)
209 mkTypeEnvs tdefs = do
210 (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
211 cenv <- foldM (checkTdef tcenv) eempty tdefs
212 return (tcenv, tsenv, cenv)
214 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
215 mkTypeEnvsNoChecking tdefs =
216 let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
217 cenv = foldl processCdef eempty tdefs in
220 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
221 -> Bool -> CheckResult ()
222 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
223 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
225 mkErrMsg :: Show a => String -> a -> String
226 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
228 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv)
229 -> Vdefg -> CheckResult (Venv,Venv)
230 checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
233 do e_venv' <- foldM extendVenv e_venv e_vts
234 l_venv' <- foldM extendVenv l_venv l_vts
235 let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
236 mapM_ (\ (vdef@(Vdef ((m,_),t,e))) ->
238 requireModulesEq m mn "value definition" vdef True
239 k <- checkTy (tcenv,tvenv) t
240 require (k `eqKind` Klifted) ("unlifted kind in:\n" ++ show vdef)
241 t' <- checkExp env' e
242 requireM (equalTy tsenv t t')
243 ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
244 "declared type: " ++ show t ++ "\n" ++
245 "expression type: " ++ show t')) vdefs
246 return (e_venv',l_venv')
247 where e_vts = [ (v,t) | Vdef ((Just _,v),t,_) <- vdefs ]
248 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
249 Nonrec (vdef@(Vdef ((m,v),t,e))) ->
251 -- TODO: document this weirdness
252 let isZcMain = vdefIsMainWrapper mn m
254 requireModulesEq m mn "value definition" vdef True
255 k <- checkTy (tcenv,tvenv) t
256 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
257 require ((not top_level) || (not (k `eqKind` Kunlifted)))
258 ("top-level unlifted kind in:\n" ++ show vdef)
259 t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
260 requireM (equalTy tsenv t t')
261 ("declared type doesn't match expression type in:\n"
262 ++ show vdef ++ "\n" ++
263 "declared type: " ++ show t ++ "\n" ++
264 "expression type: " ++ show t')
266 do l_venv' <- extendVenv l_venv (v,t)
267 return (e_venv,l_venv')
269 -- awful, but avoids name shadowing --
270 -- otherwise we'd have two bindings for "main"
271 do e_venv' <- if isZcMain
273 else extendVenv e_venv (v,t)
274 return (e_venv',l_venv)
276 vdefIsMainWrapper :: AnMname -> Mname -> Bool
277 vdefIsMainWrapper enclosing defining =
278 enclosing == mainMname && defining == wrapperMainMname
280 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
282 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
283 (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
284 -- Since the preprocessor calls checkExpr after code has been
285 -- typechecked, we expect to find the external env in the Menv.
286 case (elookup menv mn) of
288 checkExp (tcenv, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e
289 Nothing -> reportError e ("checkExpr: Environment for " ++
290 show mn ++ " not found")) (mn,menv) of
292 FailC s -> reportError e s
294 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
295 checkType mn menv tdefs tvenv t = case runReaderT (do
296 (tcenv, _, _) <- mkTypeEnvs tdefs
297 checkTy (tcenv, tvenv) t) (mn, menv) of
299 FailC s -> reportError tvenv s
301 checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
302 checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
307 qlookupM venv_ e_venv l_venv qv
309 qlookupM cenv_ cenv eempty qc
314 k' <- checkTy (tcenv,tvenv) t
317 do require (k' `subKindOf` k)
318 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
319 "operator kind: " ++ show k ++ "\n" ++
320 "operand kind: " ++ show k')
321 return (substl [tv] [t] t0)
322 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
323 "operator type: " ++ show t')
328 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
329 do requireM (equalTy tsenv t2 t')
330 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
331 "operator type: " ++ show t' ++ "\n" ++
332 "operand type: " ++ show t2)
334 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
335 "operator type: " ++ show t1)
337 do tvenv' <- extendTvenv tvenv tb
338 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
339 return (Tforall tb t)
340 Lam (Vb (vb@(_,vt))) e ->
341 do k <- checkTy (tcenv,tvenv) vt
343 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
345 l_venv' <- extendVenv l_venv vb
346 t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
347 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
350 do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv)
351 (e_venv,l_venv) vdefg
352 checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
353 Case e (v,t) resultTy alts ->
355 checkTy (tcenv,tvenv) t
356 requireM (equalTy tsenv t t')
357 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
358 "declared type: " ++ show t ++ "\n" ++
359 "expression type: " ++ show t')
360 case (reverse alts) of
362 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
363 ("duplicate alternative in case:\n" ++ show e0)
365 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
366 ok [Adefault _] _ = return ()
367 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
371 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
372 ok ((Alit l _):as) ls = do require (notElem l ls)
373 ("duplicate alternative in case:\n" ++ show e0)
375 ok [Adefault _] _ = return ()
376 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
377 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
379 [Adefault _] -> return ()
380 _ -> fail ("no alternatives in case:\n" ++ show e0)
381 l_venv' <- extendVenv l_venv (v,t)
382 t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
383 bs <- mapM (equalTy tsenv t) ts
385 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
386 "types: " ++ show (t:ts))
387 checkTy (tcenv,tvenv) resultTy
388 require (t == resultTy) ("case alternative type doesn't " ++
389 " match case return type in:\n" ++ show e0 ++ "\n" ++
390 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
394 k <- checkTy (tcenv,tvenv) t
396 (Keq fromTy toTy) -> do
397 require (eTy == fromTy) ("Type mismatch in cast: c = "
398 ++ show c ++ " and " ++ show eTy
399 ++ " and " ++ show fromTy)
401 _ -> fail ("Cast with non-equality kind: " ++ show e
402 ++ " and " ++ show t ++ " has kind " ++ show k)
406 do checkTy (tcenv,eempty) t {- external types must be closed -}
409 checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
410 checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
414 Acon qc etbs vbs e ->
416 where f (Tapp t0 t) = f t0 ++ [t]
418 ct <- qlookupM cenv_ cenv eempty qc
419 let (tbs,ct_args0,ct_res0) = splitTy ct
421 let (utbs,etbs') = splitAt (length uts) tbs
422 let utvs = map fst utbs
423 {- check existentials -}
424 let (etvs,eks) = unzip etbs
425 let (etvs',eks') = unzip etbs'
426 require (all (uncurry eqKind)
428 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
429 "kinds declared in data constructor: " ++ show eks ++
430 "kinds declared in case alternative: " ++ show eks')
431 tvenv' <- foldM extendTvenv tvenv etbs
432 {- check term variables -}
433 let vts = map snd vbs
434 mapM_ (\vt -> require ((not . isUtupleTy) vt)
435 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
436 "pattern type: " ++ show vt)) vts
437 vks <- mapM (checkTy (tcenv,tvenv')) vts
438 mapM_ (\vk -> require (baseKind vk)
439 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
440 "kind: " ++ show vk)) vks
441 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
444 requireM (equalTy tsenv ct_arg vt)
445 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
446 "pattern variable type: " ++ show ct_arg ++ "\n" ++
447 "constructor argument type: " ++ show vt)) ct_args vts
448 requireM (equalTy tsenv ct_res t0)
449 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
450 "pattern constructor type: " ++ show ct_res ++ "\n" ++
451 "scrutinee type: " ++ show t0)
452 l_venv' <- foldM extendVenv l_venv vbs
453 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
454 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
458 requireM (equalTy tsenv t t0)
459 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
460 "pattern type: " ++ show t ++ "\n" ++
461 "scrutinee type: " ++ show t0)
466 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
467 checkTy es@(tcenv,tvenv) t = ch t
469 ch (Tvar tv) = lookupM tvenv tv
471 kOrC <- qlookupM tcenv_ tcenv eempty qtc
474 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
475 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
476 ch (t@(Tapp t1 t2)) =
477 case splitTyConApp_maybe t of
479 tcK <- qlookupM tcenv_ tcenv eempty tc
481 Kind _ -> checkTapp t1 t2
482 Coercion (DefinedCoercion tbs (from,to)) -> do
483 -- makes sure coercion is fully applied
484 require (length tys == length tbs) $
485 ("Arity mismatch in coercion app: " ++ show t)
486 let (tvs, tks) = unzip tbs
487 argKs <- mapM (checkTy es) tys
488 require (all (uncurry eqKind) (zip tks argKs))
489 ("Kind mismatch in coercion app: " ++ show tks
490 ++ " and " ++ show argKs ++ " t = " ++ show t)
491 return $ Keq (substl tvs tys from) (substl tvs tys to)
492 Nothing -> checkTapp t1 t2
493 where checkTapp t1 t2 = do
499 Keq eqTy1 eqTy2 -> do
500 -- Distribute the type operator over the
502 subK1 <- checkTy es eqTy1
503 subK2 <- checkTy es eqTy2
504 require (subK2 `subKindOf` k11 &&
505 subK1 `subKindOf` k11) $
507 return $ Keq (Tapp t1 eqTy1) (Tapp t1 eqTy2)
509 require (k2 `subKindOf` k11) kindError
512 "kinds don't match in type application: "
514 "operator kind: " ++ show k11 ++ "\n" ++
515 "operand kind: " ++ show k2
516 _ -> fail ("applied type has non-arrow kind: " ++ show t)
519 do tvenv' <- extendTvenv tvenv tb
520 k <- checkTy (tcenv,tvenv') t
522 -- distribute the forall
523 Keq t1 t2 -> Keq (Tforall tb t1) (Tforall tb t2)
525 ch (TransCoercion t1 t2) = do
529 (Keq ty1 ty2, Keq ty3 ty4) | ty2 == ty3 ->
531 _ -> fail ("Bad kinds in trans. coercion: " ++
532 show k1 ++ " " ++ show k2)
533 ch (SymCoercion t1) = do
536 Keq ty1 ty2 -> return $ Keq ty2 ty1
537 _ -> fail ("Bad kind in sym. coercion: "
539 ch (UnsafeCoercion t1 t2) = do
543 ch (LeftCoercion t1) = do
546 Keq (Tapp u _) (Tapp w _) -> return $ Keq u w
547 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
548 ch (RightCoercion t1) = do
551 Keq (Tapp _ v) (Tapp _ x) -> return $ Keq v x
552 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
554 {- Type equality modulo newtype synonyms. -}
555 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
556 equalTy tsenv t1 t2 =
560 where expand (Tvar v) = return (Tvar v)
561 expand (Tcon qtc) = return (Tcon qtc)
562 expand (Tapp t1 t2) =
565 expand (Tforall tb t) =
567 return (Tforall tb t')
568 expand (TransCoercion t1 t2) = do
571 return $ TransCoercion exp1 exp2
572 expand (SymCoercion t) = do
574 return $ SymCoercion exp
575 expand (UnsafeCoercion t1 t2) = do
578 return $ UnsafeCoercion exp1 exp2
579 expand (LeftCoercion t1) = do
581 return $ LeftCoercion exp1
582 expand (RightCoercion t1) = do
584 return $ RightCoercion exp1
585 expapp (t@(Tcon (m,tc))) ts =
586 do env <- mlookupM tsenv_ tsenv eempty m
587 case elookup env tc of
588 Just (formals,rhs) | (length formals) == (length ts) ->
589 return (substl formals ts rhs)
590 _ -> return (foldl Tapp t ts)
591 expapp (Tapp t1 t2) ts =
596 return (foldl Tapp t' ts)
598 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
599 -> CheckResult (Env a b)
600 mlookupM _ _ local_env Nothing = return local_env
601 mlookupM selector external_env local_env (Just m) = do
604 then return external_env
606 globalEnv <- getGlobalEnv
607 case elookup globalEnv m of
608 Just env' -> return (selector env')
609 Nothing -> fail ("Check: undefined module name: "
610 ++ show m ++ show (edomain local_env))
612 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
613 -> Qual a -> CheckResult b
614 qlookupM selector external_env local_env (m,k) =
615 do env <- mlookupM selector external_env local_env m
618 checkLit :: Lit -> CheckResult Ty
619 checkLit (Literal lit t) =
622 do require (t `elem` intLitTypes)
623 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
626 do require (t `elem` ratLitTypes)
627 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
630 do require (t `elem` charLitTypes)
631 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
634 do require (t `elem` stringLitTypes)
635 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
640 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
641 splitTy :: Ty -> ([Tbind],[Ty],Ty)
642 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
643 where (tbs,ts,tr) = splitTy t
644 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
645 where (tbs,ts,tr) = splitTy t
646 splitTy t = ([],[],t)
649 {- Simultaneous substitution on types for type variables,
650 renaming as neceessary to avoid capture.
651 No checks for correct kindedness. -}
652 substl :: [Tvar] -> [Ty] -> Ty -> Ty
653 substl tvs ts t = f (zip tvs ts) t
658 Tvar v -> case lookup v env of
661 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
663 if t `elem` free then
664 Tforall (t',k) (f ((t,Tvar t'):env) t1)
666 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
667 TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
668 SymCoercion t1 -> SymCoercion (f env t1)
669 UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
670 LeftCoercion t1 -> LeftCoercion (f env t1)
671 RightCoercion t1 -> RightCoercion (f env t1)
672 where free = foldr union [] (map (freeTvars.snd) env)
675 {- Return free tvars in a type -}
676 freeTvars :: Ty -> [Tvar]
677 freeTvars (Tcon _) = []
678 freeTvars (Tvar v) = [v]
679 freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
680 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
681 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
682 freeTvars (SymCoercion t) = freeTvars t
683 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
684 freeTvars (LeftCoercion t) = freeTvars t
685 freeTvars (RightCoercion t) = freeTvars t
687 {- Return any tvar *not* in the argument list. -}
688 freshTvar :: [Tvar] -> Tvar
689 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
691 primCoercionError :: Show a => a -> b
692 primCoercionError s = error $ "Bad coercion application: " ++ show s
695 reportError :: Show a => a -> String -> b
696 reportError e s = error $ ("Core type error: checkExpr failed with "
697 ++ s ++ " and " ++ show e)