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
11 -- just for printing warnings
12 import System.IO.Unsafe
20 {- Checking is done in a simple error monad. In addition to
21 allowing errors to be captured, this makes it easy to guarantee
22 that checking itself has been completed for an entire module. -}
24 {- We use the Reader monad transformer in order to thread the
25 top-level module name throughout the computation simply.
26 This is so that checkExp can also be an entry point (we call it
28 data CheckRes a = OkC a | FailC String
29 type CheckResult a = ReaderT (AnMname, Menv) CheckRes a
30 getMname :: CheckResult AnMname
31 getMname = ask >>= (return . fst)
32 getGlobalEnv :: CheckResult Menv
33 getGlobalEnv = ask >>= (return . snd)
35 instance Monad CheckRes where
37 FailC s >>= _ = fail s
41 require :: Bool -> String -> CheckResult ()
42 require False s = fail s
43 require True _ = return ()
45 requireM :: CheckResult Bool -> String -> CheckResult ()
51 type Tvenv = Env Tvar Kind -- type variables (local only)
52 type Tcenv = Env Tcon KindOrCoercion -- type constructors
53 type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms
54 type Cenv = Env Dcon Ty -- data constructors
55 type Venv = Env Var Ty -- values
56 type Menv = Env AnMname Envs -- modules
57 data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
60 {- Extend an environment, checking for illegal shadowing of identifiers (for term
61 variables -- shadowing type variables is allowed.) -}
62 data EnvType = Tv | NotTv
65 extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
66 extendM envType env (k,d) =
68 Just _ | envType == NotTv -> fail ("multiply-defined identifier: "
70 _ -> return (eextend env (k,d))
72 extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
73 extendVenv = extendM NotTv
75 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
76 extendTvenv = extendM Tv
78 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
82 Nothing -> fail ("undefined identifier: " ++ show k)
84 {- Main entry point. -}
85 checkModule :: Menv -> Module -> CheckRes Menv
86 checkModule globalEnv (Module mn tdefs vdefgs) =
88 (do (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
89 (e_venv,_) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv))
92 return (eextend globalEnv
93 (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv})))
94 -- avoid name shadowing
95 (mn, eremove globalEnv mn)
97 -- Like checkModule, but doesn't typecheck the code, instead just
98 -- returning declared types for top-level defns.
99 -- This is necessary in order to handle circular dependencies, but it's sort
101 envsModule :: Menv -> Module -> Menv
102 envsModule globalEnv (Module mn tdefs vdefgs) =
103 let (tcenv, tsenv, cenv) = mkTypeEnvsNoChecking tdefs
104 e_venv = foldr vdefgTypes eempty vdefgs in
105 eextend globalEnv (mn,
106 (Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
107 where vdefgTypes :: Vdefg -> Venv -> Venv
108 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
110 vdefgTypes (Rec vds) e =
111 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
112 add :: [(Qual Var,Ty)] -> Venv -> Venv
113 add pairs e = foldr addOne e pairs
114 addOne :: (Qual Var, Ty) -> Venv -> Venv
115 addOne ((Nothing,_),_) e = e
116 addOne ((Just _,v),t) e = eextend e (v,t)
118 checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
119 checkTdef0 (tcenv,tsenv) tdef = ch tdef
121 ch (Data (m,c) tbs _) =
123 requireModulesEq m mn "data type declaration" tdef False
124 tcenv' <- extendM NotTv tcenv (c, Kind k)
125 return (tcenv',tsenv)
126 where k = foldr Karrow Klifted (map snd tbs)
127 ch (Newtype (m,c) coVar tbs rhs) =
129 requireModulesEq m mn "newtype declaration" tdef False
130 tcenv' <- extendM NotTv tcenv (c, Kind k)
131 -- add newtype axiom to env
132 tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
133 tsenv' <- case rhs of
134 Nothing -> return tsenv
135 Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
136 return (tcenv'', tsenv')
137 where k = foldr Karrow Klifted (map snd tbs)
139 processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
140 processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
142 ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
143 where k = foldr Karrow Klifted (map snd tbs)
144 ch (Newtype tc@(_,c) coercion tbs rhs) =
145 let tcenv' = eextend tcenv (c, Kind k)
146 -- add newtype axiom to env
147 tcenv'' = case rhs of
150 (snd coercion, Coercion $ DefinedCoercion tbs
151 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rep))
154 (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
156 where k = foldr Karrow Klifted (map snd tbs)
158 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Maybe Ty
160 envPlusNewtype tcenv tyCon coVar tbs rhs =
162 Nothing -> return tcenv
163 Just rep -> extendM NotTv tcenv
164 (snd coVar, Coercion $ DefinedCoercion tbs
165 (foldl Tapp (Tcon tyCon)
166 (map Tvar (fst (unzip tbs))),
169 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
170 checkTdef tcenv cenv = ch
172 ch (Data (_,c) utbs cdefs) =
173 do cbinds <- mapM checkCdef cdefs
174 foldM (extendM NotTv) cenv cbinds
175 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
177 requireModulesEq m mn "constructor declaration" cdef
179 tvenv <- foldM (extendM Tv) eempty tbs
180 ks <- mapM (checkTy (tcenv,tvenv)) ts
181 mapM_ (\k -> require (baseKind k)
182 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
183 "kind: " ++ show k) ) ks
185 where tbs = utbs ++ etbs
188 (foldl Tapp (Tcon (Just mn,c))
189 (map (Tvar . fst) utbs)) ts) tbs
190 ch (tdef@(Newtype tc _ tbs (Just t))) =
191 do tvenv <- foldM (extendM Tv) eempty tbs
192 kRhs <- checkTy (tcenv,tvenv) t
193 require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
194 kLhs <- checkTy (tcenv,tvenv)
195 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
196 require (kLhs `eqKind` kRhs)
197 ("Kind mismatch in newtype axiom types: " ++ show tdef
199 (show kLhs) ++ " and " ++ (show kRhs))
201 ch (Newtype _ _ _ Nothing) =
202 {- should only occur for recursive Newtypes -}
205 processCdef :: Cenv -> Tdef -> Cenv
206 processCdef cenv = ch
208 ch (Data (_,c) utbs cdefs) = do
209 let cbinds = map checkCdef cdefs
210 foldl eextend cenv cbinds
211 where checkCdef (Constr (mn,dcon) etbs ts) =
213 where tbs = utbs ++ etbs
216 (foldl Tapp (Tcon (mn,c))
217 (map (Tvar . fst) utbs)) ts) tbs
220 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv)
221 mkTypeEnvs tdefs = do
222 (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
223 cenv <- foldM (checkTdef tcenv) eempty tdefs
224 return (tcenv, tsenv, cenv)
226 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
227 mkTypeEnvsNoChecking tdefs =
228 let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
229 cenv = foldl processCdef eempty tdefs in
232 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
233 -> Bool -> CheckResult ()
234 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
235 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
237 mkErrMsg :: Show a => String -> a -> String
238 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
240 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv)
241 -> Vdefg -> CheckResult (Venv,Venv)
242 checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
246 do (e_venv', l_venv') <- makeEnv mn vdefs
247 let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
248 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
249 ("unlifted kind in:\n" ++ show vdef)) env')
251 return (e_venv', l_venv')
253 do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv)
254 checkVdef (\ vdef k -> do
255 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
256 require ((not top_level) || (not (k `eqKind` Kunlifted)))
257 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
260 where makeEnv mn vdefs = do
261 ev <- foldM extendVenv e_venv e_vts
262 lv <- foldM extendVenv l_venv l_vts
264 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
265 not (vdefIsMainWrapper mn (Just m))]
266 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
267 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
269 let isZcMain = vdefIsMainWrapper mn m
271 requireModulesEq m mn "value definition" vdef True
272 k <- checkTy (tcenv,tvenv) t
275 requireM (equalTy tsenv t t')
276 ("declared type doesn't match expression type in:\n"
277 ++ show vdef ++ "\n" ++
278 "declared type: " ++ show t ++ "\n" ++
279 "expression type: " ++ show t')
281 vdefIsMainWrapper :: AnMname -> Mname -> Bool
282 vdefIsMainWrapper enclosing defining =
283 enclosing == mainMname && defining == wrapperMainAnMname
285 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
287 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
288 (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
289 -- Since the preprocessor calls checkExpr after code has been
290 -- typechecked, we expect to find the external env in the Menv.
291 case (elookup menv mn) of
293 checkExp (tcenv, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e
294 Nothing -> reportError e ("checkExpr: Environment for " ++
295 show mn ++ " not found")) (mn,menv) of
297 FailC s -> reportError e s
299 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
300 checkType mn menv tdefs tvenv t = case runReaderT (do
301 (tcenv, _, _) <- mkTypeEnvs tdefs
302 checkTy (tcenv, tvenv) t) (mn, menv) of
304 FailC s -> reportError tvenv s
306 checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
307 checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
312 qlookupM venv_ e_venv l_venv qv
314 qlookupM cenv_ cenv eempty qc
319 k' <- checkTy (tcenv,tvenv) t
322 do require (k' `subKindOf` k)
323 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
324 "operator kind: " ++ show k ++ "\n" ++
325 "operand kind: " ++ show k')
326 return (substl [tv] [t] t0)
327 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
328 "operator type: " ++ show t')
333 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
334 do requireM (equalTy tsenv t2 t')
335 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
336 "operator type: " ++ show t' ++ "\n" ++
337 "operand type: " ++ show t2)
339 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
340 "operator type: " ++ show t1)
342 do tvenv' <- extendTvenv tvenv tb
343 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
344 return (Tforall tb t)
345 Lam (Vb (vb@(_,vt))) e ->
346 do k <- checkTy (tcenv,tvenv) vt
348 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
350 l_venv' <- extendVenv l_venv vb
351 t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
352 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
355 do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv)
356 (e_venv,l_venv) vdefg
357 checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
358 Case e (v,t) resultTy alts ->
360 checkTy (tcenv,tvenv) t
361 requireM (equalTy tsenv t t')
362 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
363 "declared type: " ++ show t ++ "\n" ++
364 "expression type: " ++ show t')
365 case (reverse alts) of
367 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
368 ("duplicate alternative in case:\n" ++ show e0)
370 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
371 ok [Adefault _] _ = return ()
372 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
376 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
377 ok ((Alit l _):as) ls = do require (notElem l ls)
378 ("duplicate alternative in case:\n" ++ show e0)
380 ok [Adefault _] _ = return ()
381 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
382 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
384 [Adefault _] -> return ()
385 _ -> fail ("no alternatives in case:\n" ++ show e0)
386 l_venv' <- extendVenv l_venv (v,t)
387 t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
388 bs <- mapM (equalTy tsenv t) ts
390 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
391 "types: " ++ show (t:ts))
392 checkTy (tcenv,tvenv) resultTy
393 require (t == resultTy) ("case alternative type doesn't " ++
394 " match case return type in:\n" ++ show e0 ++ "\n" ++
395 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
399 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
400 require (eTy == fromTy) ("Type mismatch in cast: c = "
401 ++ show c ++ "\nand eTy = " ++ show eTy
402 ++ "\n and " ++ show fromTy)
407 do checkTy (tcenv,eempty) t {- external types must be closed -}
410 checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
411 checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
415 Acon qc etbs vbs e ->
417 where f (Tapp t0 t) = f t0 ++ [t]
419 ct <- qlookupM cenv_ cenv eempty qc
420 let (tbs,ct_args0,ct_res0) = splitTy ct
422 let (utbs,etbs') = splitAt (length uts) tbs
423 let utvs = map fst utbs
424 {- check existentials -}
425 let (etvs,eks) = unzip etbs
426 let (etvs',eks') = unzip etbs'
427 require (all (uncurry eqKind)
429 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
430 "kinds declared in data constructor: " ++ show eks ++
431 "kinds declared in case alternative: " ++ show eks')
432 tvenv' <- foldM extendTvenv tvenv etbs
433 {- check term variables -}
434 let vts = map snd vbs
435 mapM_ (\vt -> require ((not . isUtupleTy) vt)
436 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
437 "pattern type: " ++ show vt)) vts
438 vks <- mapM (checkTy (tcenv,tvenv')) vts
439 mapM_ (\vk -> require (baseKind vk)
440 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
441 "kind: " ++ show vk)) vks
442 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
445 requireM (equalTy tsenv ct_arg vt)
446 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
447 "pattern variable type: " ++ show ct_arg ++ "\n" ++
448 "constructor argument type: " ++ show vt)) ct_args vts
449 requireM (equalTy tsenv ct_res t0)
450 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
451 "pattern constructor type: " ++ show ct_res ++ "\n" ++
452 "scrutinee type: " ++ show t0)
453 l_venv' <- foldM extendVenv l_venv vbs
454 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
455 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
459 requireM (equalTy tsenv t t0)
460 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
461 "pattern type: " ++ show t ++ "\n" ++
462 "scrutinee type: " ++ show t0)
467 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
468 checkTy es@(tcenv,tvenv) = ch
470 ch (Tvar tv) = lookupM tvenv tv
472 kOrC <- qlookupM tcenv_ tcenv eempty qtc
475 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
476 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
477 ch (t@(Tapp t1 t2)) =
478 case splitTyConApp_maybe t of
480 tcK <- qlookupM tcenv_ tcenv eempty tc
482 Kind _ -> checkTapp t1 t2
483 Coercion (DefinedCoercion tbs (from,to)) -> do
484 -- makes sure coercion is fully applied
485 require (length tys == length tbs) $
486 ("Arity mismatch in coercion app: " ++ show t)
487 let (tvs, tks) = unzip tbs
488 argKs <- mapM (checkTy es) tys
489 let kPairs = zip argKs tks
490 let kindsOk = all (uncurry eqKind) kPairs
492 all (uncurry subKindOf) kPairs
493 -- GHC occasionally generates code like:
494 -- :Co:TTypeable2 (->)
495 -- where in this case, :Co:TTypeable2 expects an
496 -- argument of kind (*->(*->*)) and (->) has kind
497 -- (?->(?->*)). I'm not sure whether or not it's
498 -- sound to apply an arbitrary coercion to an
499 -- argument that's a subkind of what it expects.
500 then warn $ "Applying coercion " ++ show tc ++
501 " to arguments of kind " ++ show argKs
502 ++ " when it expects: " ++ show tks
504 ("Kind mismatch in coercion app: " ++ show tks
505 ++ " and " ++ show argKs ++ " t = " ++ show t)
506 return $ Keq (substl tvs tys from) (substl tvs tys to)
507 Nothing -> checkTapp t1 t2
508 where checkTapp t1 t2 = do
513 require (k2 `subKindOf` k11) kindError
516 "kinds don't match in type application: "
518 "operator kind: " ++ show k11 ++ "\n" ++
519 "operand kind: " ++ show k2
520 _ -> fail ("applied type has non-arrow kind: " ++ show t)
523 do tvenv' <- extendTvenv tvenv tb
524 checkTy (tcenv,tvenv') t
525 ch (TransCoercion t1 t2) = do
526 (ty1,ty2) <- checkTyCo es t1
527 (ty3,ty4) <- checkTyCo es t2
528 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
529 show ty2 ++ " and " ++ show ty3)
531 ch (SymCoercion t1) = do
532 (ty1,ty2) <- checkTyCo es t1
534 ch (UnsafeCoercion t1 t2) = do
538 ch (LeftCoercion t1) = do
541 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
542 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
543 ch (RightCoercion t1) = do
546 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
547 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
548 ch (InstCoercion ty arg) = do
549 forallK <- checkTyCo es ty
551 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
552 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
554 argK <- checkTy es arg
555 require (argK `eqKind` k1) ("Kind mismatch in type being "
556 ++ "instantiated: " ++ show arg)
557 let newLhs = substl [v1] [arg] b1
558 let newRhs = substl [v2] [arg] b2
559 return $ Keq newLhs newRhs
560 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
562 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
563 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
564 (case splitTyConApp_maybe t of
566 tcK <- qlookupM tcenv_ tcenv eempty tc
568 -- todo: avoid duplicating this code
569 -- blah, this almost calls for a different syntactic form
570 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
571 Coercion (DefinedCoercion tbs (from, to)) -> do
572 require (length tys == length tbs) $
573 ("Arity mismatch in coercion app: " ++ show t)
574 let (tvs, tks) = unzip tbs
575 argKs <- mapM (checkTy es) tys
576 let kPairs = zip argKs tks
577 let kindsOk = all (uncurry eqKind) kPairs
579 all (uncurry subKindOf) kPairs
580 -- see comments in checkTy about this
581 then warn $ "Applying coercion " ++ show tc ++
582 " to arguments of kind " ++ show argKs
583 ++ " when it expects: " ++ show tks
585 ("Kind mismatch in coercion app: " ++ show tks
586 ++ " and " ++ show argKs ++ " t = " ++ show t)
587 return (substl tvs tys from, substl tvs tys to)
589 _ -> checkTapp t1 t2)
590 where checkTapp t1 t2 = do
591 (lhsRator, rhsRator) <- checkTyCo es t1
592 (lhs, rhs) <- checkTyCo es t2
593 -- Comp rule from paper
594 checkTy es (Tapp lhsRator lhs)
595 checkTy es (Tapp rhsRator rhs)
596 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
597 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
598 tvenv' <- extendTvenv tvenv tb
599 (t1,t2) <- checkTyCo (tcenv, tvenv') t
600 return (Tforall tb t1, Tforall tb t2)
604 Keq t1 t2 -> return (t1, t2)
605 -- otherwise, expand by the "refl" rule
608 {- Type equality modulo newtype synonyms. -}
609 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
610 equalTy tsenv t1 t2 =
614 where expand (Tvar v) = return (Tvar v)
615 expand (Tcon qtc) = return (Tcon qtc)
616 expand (Tapp t1 t2) =
619 expand (Tforall tb t) =
621 return (Tforall tb t')
622 expand (TransCoercion t1 t2) = do
625 return $ TransCoercion exp1 exp2
626 expand (SymCoercion t) = do
628 return $ SymCoercion exp
629 expand (UnsafeCoercion t1 t2) = do
632 return $ UnsafeCoercion exp1 exp2
633 expand (LeftCoercion t1) = do
635 return $ LeftCoercion exp1
636 expand (RightCoercion t1) = do
638 return $ RightCoercion exp1
639 expand (InstCoercion t1 t2) = do
642 return $ InstCoercion exp1 exp2
643 expapp (t@(Tcon (m,tc))) ts =
644 do env <- mlookupM tsenv_ tsenv eempty m
645 case elookup env tc of
646 Just (formals,rhs) | (length formals) == (length ts) ->
647 return (substl formals ts rhs)
648 _ -> return (foldl Tapp t ts)
649 expapp (Tapp t1 t2) ts =
654 return (foldl Tapp t' ts)
656 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
657 -> CheckResult (Env a b)
658 mlookupM _ _ local_env Nothing = return local_env
659 mlookupM selector external_env local_env (Just m) = do
662 then return external_env
664 globalEnv <- getGlobalEnv
665 case elookup globalEnv m of
666 Just env' -> return (selector env')
667 Nothing -> fail ("Check: undefined module name: "
668 ++ show m ++ show (edomain local_env))
670 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
671 -> Qual a -> CheckResult b
672 qlookupM selector external_env local_env (m,k) =
673 do env <- mlookupM selector external_env local_env m
676 checkLit :: Lit -> CheckResult Ty
677 checkLit (Literal lit t) =
680 do require (t `elem` intLitTypes)
681 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
684 do require (t `elem` ratLitTypes)
685 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
688 do require (t `elem` charLitTypes)
689 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
692 do require (t `elem` stringLitTypes)
693 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
698 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
699 splitTy :: Ty -> ([Tbind],[Ty],Ty)
700 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
701 where (tbs,ts,tr) = splitTy t
702 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
703 where (tbs,ts,tr) = splitTy t
704 splitTy t = ([],[],t)
707 {- Simultaneous substitution on types for type variables,
708 renaming as neceessary to avoid capture.
709 No checks for correct kindedness. -}
710 substl :: [Tvar] -> [Ty] -> Ty -> Ty
711 substl tvs ts t = f (zip tvs ts) t
716 Tvar v -> case lookup v env of
719 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
721 if t `elem` free then
722 Tforall (t',k) (f ((t,Tvar t'):env) t1)
724 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
725 TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
726 SymCoercion t1 -> SymCoercion (f env t1)
727 UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
728 LeftCoercion t1 -> LeftCoercion (f env t1)
729 RightCoercion t1 -> RightCoercion (f env t1)
730 InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
731 where free = foldr union [] (map (freeTvars.snd) env)
734 {- Return free tvars in a type -}
735 freeTvars :: Ty -> [Tvar]
736 freeTvars (Tcon _) = []
737 freeTvars (Tvar v) = [v]
738 freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
739 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
740 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
741 freeTvars (SymCoercion t) = freeTvars t
742 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
743 freeTvars (LeftCoercion t) = freeTvars t
744 freeTvars (RightCoercion t) = freeTvars t
745 freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
747 {- Return any tvar *not* in the argument list. -}
748 freshTvar :: [Tvar] -> Tvar
749 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
751 primCoercionError :: Show a => a -> b
752 primCoercionError s = error $ "Bad coercion application: " ++ show s
755 reportError :: Show a => a -> String -> b
756 reportError e s = error $ ("Core type error: checkExpr failed with "
757 ++ s ++ " and " ++ show e)
759 warn :: String -> CheckResult ()
760 warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return ()