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) tbs ((_,coercion),cTbs,coercionKind) 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'' <- extendM NotTv tcenv'
133 (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
134 tsenv' <- case rhs of
135 Nothing -> return tsenv
136 Just rep -> extendM NotTv tsenv (c,(map fst tbs,rep))
137 return (tcenv'', tsenv')
138 where k = foldr Karrow Klifted (map snd tbs)
140 processTdef0NoChecking :: (Tcenv,Tsenv) -> Tdef -> (Tcenv,Tsenv)
141 processTdef0NoChecking (tcenv,tsenv) tdef = ch tdef
143 ch (Data (_,c) tbs _) = (eextend tcenv (c, Kind k), tsenv)
144 where k = foldr Karrow Klifted (map snd tbs)
145 ch (Newtype (_,c) tbs ((_,coercion),cTbs,coercionKind) rhs) =
146 let tcenv' = eextend tcenv (c, Kind k)
147 -- add newtype axiom to env
148 tcenv'' = eextend tcenv'
149 (coercion, Coercion $ DefinedCoercion cTbs coercionKind)
151 (\ rep -> eextend tsenv (c, (map fst tbs, rep))) rhs in
153 where k = foldr Karrow Klifted (map snd tbs)
155 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
156 checkTdef tcenv cenv = ch
158 ch (Data (_,c) utbs cdefs) =
159 do cbinds <- mapM checkCdef cdefs
160 foldM (extendM NotTv) cenv cbinds
161 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
163 requireModulesEq m mn "constructor declaration" cdef
165 tvenv <- foldM (extendM Tv) eempty tbs
166 ks <- mapM (checkTy (tcenv,tvenv)) ts
167 mapM_ (\k -> require (baseKind k)
168 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
169 "kind: " ++ show k) ) ks
171 where tbs = utbs ++ etbs
174 (foldl Tapp (Tcon (Just mn,c))
175 (map (Tvar . fst) utbs)) ts) tbs
176 ch (tdef@(Newtype _ tbs (_, coTbs, (coLhs, coRhs)) (Just t))) =
177 do tvenv <- foldM (extendM Tv) eempty tbs
178 k <- checkTy (tcenv,tvenv) t
179 -- Makes sure GHC is eta-expanding things properly
180 require (length tbs == length coTbs) $
181 ("Arity mismatch between newtycon and newtype coercion: "
183 require (k `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
184 axiomTvenv <- foldM (extendM Tv) eempty coTbs
185 kLhs <- checkTy (tcenv,axiomTvenv) coLhs
186 kRhs <- checkTy (tcenv,axiomTvenv) coRhs
187 require (kLhs `eqKind` kRhs)
188 ("Kind mismatch in newtype axiom types: " ++ show tdef
190 (show kLhs) ++ " and " ++ (show kRhs))
192 ch (Newtype _ _ _ Nothing) =
193 {- should only occur for recursive Newtypes -}
196 processCdef :: Cenv -> Tdef -> Cenv
197 processCdef cenv = ch
199 ch (Data (_,c) utbs cdefs) = do
200 let cbinds = map checkCdef cdefs
201 foldl eextend cenv cbinds
202 where checkCdef (Constr (mn,dcon) etbs ts) =
204 where tbs = utbs ++ etbs
207 (foldl Tapp (Tcon (mn,c))
208 (map (Tvar . fst) utbs)) ts) tbs
211 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Tsenv, Cenv)
212 mkTypeEnvs tdefs = do
213 (tcenv, tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
214 cenv <- foldM (checkTdef tcenv) eempty tdefs
215 return (tcenv, tsenv, cenv)
217 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Tsenv, Cenv)
218 mkTypeEnvsNoChecking tdefs =
219 let (tcenv, tsenv) = foldl processTdef0NoChecking (eempty,eempty) tdefs
220 cenv = foldl processCdef eempty tdefs in
223 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
224 -> Bool -> CheckResult ()
225 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
226 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
228 mkErrMsg :: Show a => String -> a -> String
229 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
231 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv)
232 -> Vdefg -> CheckResult (Venv,Venv)
233 checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
237 do (e_venv', l_venv') <- makeEnv mn vdefs
238 let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
239 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
240 ("unlifted kind in:\n" ++ show vdef)) env')
242 return (e_venv', l_venv')
244 do let env' = (tcenv, tsenv, tvenv, cenv, e_venv, l_venv)
245 checkVdef (\ vdef k -> do
246 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
247 require ((not top_level) || (not (k `eqKind` Kunlifted)))
248 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
251 where makeEnv mn vdefs = do
252 ev <- foldM extendVenv e_venv e_vts
253 lv <- foldM extendVenv l_venv l_vts
255 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
256 not (vdefIsMainWrapper mn (Just m))]
257 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
258 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
260 let isZcMain = vdefIsMainWrapper mn m
262 requireModulesEq m mn "value definition" vdef True
263 k <- checkTy (tcenv,tvenv) t
266 requireM (equalTy tsenv t t')
267 ("declared type doesn't match expression type in:\n"
268 ++ show vdef ++ "\n" ++
269 "declared type: " ++ show t ++ "\n" ++
270 "expression type: " ++ show t')
272 vdefIsMainWrapper :: AnMname -> Mname -> Bool
273 vdefIsMainWrapper enclosing defining =
274 enclosing == mainMname && defining == wrapperMainMname
276 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
278 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
279 (tcenv, tsenv, cenv) <- mkTypeEnvs tdefs
280 -- Since the preprocessor calls checkExpr after code has been
281 -- typechecked, we expect to find the external env in the Menv.
282 case (elookup menv mn) of
284 checkExp (tcenv, tsenv, tvenv, cenv, (venv_ thisEnv), venv) e
285 Nothing -> reportError e ("checkExpr: Environment for " ++
286 show mn ++ " not found")) (mn,menv) of
288 FailC s -> reportError e s
290 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
291 checkType mn menv tdefs tvenv t = case runReaderT (do
292 (tcenv, _, _) <- mkTypeEnvs tdefs
293 checkTy (tcenv, tvenv) t) (mn, menv) of
295 FailC s -> reportError tvenv s
297 checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
298 checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
303 qlookupM venv_ e_venv l_venv qv
305 qlookupM cenv_ cenv eempty qc
310 k' <- checkTy (tcenv,tvenv) t
313 do require (k' `subKindOf` k)
314 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
315 "operator kind: " ++ show k ++ "\n" ++
316 "operand kind: " ++ show k')
317 return (substl [tv] [t] t0)
318 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
319 "operator type: " ++ show t')
324 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
325 do requireM (equalTy tsenv t2 t')
326 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
327 "operator type: " ++ show t' ++ "\n" ++
328 "operand type: " ++ show t2)
330 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
331 "operator type: " ++ show t1)
333 do tvenv' <- extendTvenv tvenv tb
334 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
335 return (Tforall tb t)
336 Lam (Vb (vb@(_,vt))) e ->
337 do k <- checkTy (tcenv,tvenv) vt
339 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
341 l_venv' <- extendVenv l_venv vb
342 t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
343 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
346 do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv)
347 (e_venv,l_venv) vdefg
348 checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
349 Case e (v,t) resultTy alts ->
351 checkTy (tcenv,tvenv) t
352 requireM (equalTy tsenv t t')
353 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
354 "declared type: " ++ show t ++ "\n" ++
355 "expression type: " ++ show t')
356 case (reverse alts) of
358 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
359 ("duplicate alternative in case:\n" ++ show e0)
361 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
362 ok [Adefault _] _ = return ()
363 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
367 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
368 ok ((Alit l _):as) ls = do require (notElem l ls)
369 ("duplicate alternative in case:\n" ++ show e0)
371 ok [Adefault _] _ = return ()
372 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
373 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
375 [Adefault _] -> return ()
376 _ -> fail ("no alternatives in case:\n" ++ show e0)
377 l_venv' <- extendVenv l_venv (v,t)
378 t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
379 bs <- mapM (equalTy tsenv t) ts
381 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
382 "types: " ++ show (t:ts))
383 checkTy (tcenv,tvenv) resultTy
384 require (t == resultTy) ("case alternative type doesn't " ++
385 " match case return type in:\n" ++ show e0 ++ "\n" ++
386 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
390 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
391 require (eTy == fromTy) ("Type mismatch in cast: c = "
392 ++ show c ++ "\nand eTy = " ++ show eTy
393 ++ "\n and " ++ show fromTy)
398 do checkTy (tcenv,eempty) t {- external types must be closed -}
401 checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
402 checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
406 Acon qc etbs vbs e ->
408 where f (Tapp t0 t) = f t0 ++ [t]
410 ct <- qlookupM cenv_ cenv eempty qc
411 let (tbs,ct_args0,ct_res0) = splitTy ct
413 let (utbs,etbs') = splitAt (length uts) tbs
414 let utvs = map fst utbs
415 {- check existentials -}
416 let (etvs,eks) = unzip etbs
417 let (etvs',eks') = unzip etbs'
418 require (all (uncurry eqKind)
420 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
421 "kinds declared in data constructor: " ++ show eks ++
422 "kinds declared in case alternative: " ++ show eks')
423 tvenv' <- foldM extendTvenv tvenv etbs
424 {- check term variables -}
425 let vts = map snd vbs
426 mapM_ (\vt -> require ((not . isUtupleTy) vt)
427 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
428 "pattern type: " ++ show vt)) vts
429 vks <- mapM (checkTy (tcenv,tvenv')) vts
430 mapM_ (\vk -> require (baseKind vk)
431 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
432 "kind: " ++ show vk)) vks
433 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
436 requireM (equalTy tsenv ct_arg vt)
437 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
438 "pattern variable type: " ++ show ct_arg ++ "\n" ++
439 "constructor argument type: " ++ show vt)) ct_args vts
440 requireM (equalTy tsenv ct_res t0)
441 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
442 "pattern constructor type: " ++ show ct_res ++ "\n" ++
443 "scrutinee type: " ++ show t0)
444 l_venv' <- foldM extendVenv l_venv vbs
445 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
446 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
450 requireM (equalTy tsenv t t0)
451 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
452 "pattern type: " ++ show t ++ "\n" ++
453 "scrutinee type: " ++ show t0)
458 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
459 checkTy es@(tcenv,tvenv) = ch
461 ch (Tvar tv) = lookupM tvenv tv
463 kOrC <- qlookupM tcenv_ tcenv eempty qtc
466 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
467 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
468 ch (t@(Tapp t1 t2)) =
469 case splitTyConApp_maybe t of
471 tcK <- qlookupM tcenv_ tcenv eempty tc
473 Kind _ -> checkTapp t1 t2
474 Coercion (DefinedCoercion tbs (from,to)) -> do
475 -- makes sure coercion is fully applied
476 require (length tys == length tbs) $
477 ("Arity mismatch in coercion app: " ++ show t)
478 let (tvs, tks) = unzip tbs
479 argKs <- mapM (checkTy es) tys
480 let kPairs = zip argKs tks
481 let kindsOk = all (uncurry eqKind) kPairs
483 all (uncurry subKindOf) kPairs
484 -- GHC occasionally generates code like:
485 -- :Co:TTypeable2 (->)
486 -- where in this case, :Co:TTypeable2 expects an
487 -- argument of kind (*->(*->*)) and (->) has kind
488 -- (?->(?->*)). I'm not sure whether or not it's
489 -- sound to apply an arbitrary coercion to an
490 -- argument that's a subkind of what it expects.
491 then warn $ "Applying coercion " ++ show tc ++
492 " to arguments of kind " ++ show argKs
493 ++ " when it expects: " ++ show tks
495 ("Kind mismatch in coercion app: " ++ show tks
496 ++ " and " ++ show argKs ++ " t = " ++ show t)
497 return $ Keq (substl tvs tys from) (substl tvs tys to)
498 Nothing -> checkTapp t1 t2
499 where checkTapp t1 t2 = do
504 require (k2 `subKindOf` k11) kindError
507 "kinds don't match in type application: "
509 "operator kind: " ++ show k11 ++ "\n" ++
510 "operand kind: " ++ show k2
511 _ -> fail ("applied type has non-arrow kind: " ++ show t)
514 do tvenv' <- extendTvenv tvenv tb
515 checkTy (tcenv,tvenv') t
516 ch (TransCoercion t1 t2) = do
517 (ty1,ty2) <- checkTyCo es t1
518 (ty3,ty4) <- checkTyCo es t2
519 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
520 show ty2 ++ " and " ++ show ty3)
522 ch (SymCoercion t1) = do
523 (ty1,ty2) <- checkTyCo es t1
525 ch (UnsafeCoercion t1 t2) = do
529 ch (LeftCoercion t1) = do
532 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
533 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
534 ch (RightCoercion t1) = do
537 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
538 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
539 ch (InstCoercion ty arg) = do
540 forallK <- checkTyCo es ty
542 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
543 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
545 argK <- checkTy es arg
546 require (argK `eqKind` k1) ("Kind mismatch in type being "
547 ++ "instantiated: " ++ show arg)
548 let newLhs = substl [v1] [arg] b1
549 let newRhs = substl [v2] [arg] b2
550 return $ Keq newLhs newRhs
551 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
553 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
554 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
555 (case splitTyConApp_maybe t of
557 tcK <- qlookupM tcenv_ tcenv eempty tc
559 -- todo: avoid duplicating this code
560 -- blah, this almost calls for a different syntactic form
561 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
562 Coercion (DefinedCoercion tbs (from, to)) -> do
563 require (length tys == length tbs) $
564 ("Arity mismatch in coercion app: " ++ show t)
565 let (tvs, tks) = unzip tbs
566 argKs <- mapM (checkTy es) tys
567 let kPairs = zip argKs tks
568 let kindsOk = all (uncurry eqKind) kPairs
570 all (uncurry subKindOf) kPairs
571 -- see comments in checkTy about this
572 then warn $ "Applying coercion " ++ show tc ++
573 " to arguments of kind " ++ show argKs
574 ++ " when it expects: " ++ show tks
576 ("Kind mismatch in coercion app: " ++ show tks
577 ++ " and " ++ show argKs ++ " t = " ++ show t)
578 return (substl tvs tys from, substl tvs tys to)
580 _ -> checkTapp t1 t2)
581 where checkTapp t1 t2 = do
582 (lhsRator, rhsRator) <- checkTyCo es t1
583 (lhs, rhs) <- checkTyCo es t2
584 -- Comp rule from paper
585 checkTy es (Tapp lhsRator lhs)
586 checkTy es (Tapp rhsRator rhs)
587 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
588 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
589 tvenv' <- extendTvenv tvenv tb
590 (t1,t2) <- checkTyCo (tcenv, tvenv') t
591 return (Tforall tb t1, Tforall tb t2)
595 Keq t1 t2 -> return (t1, t2)
596 -- otherwise, expand by the "refl" rule
599 {- Type equality modulo newtype synonyms. -}
600 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
601 equalTy tsenv t1 t2 =
605 where expand (Tvar v) = return (Tvar v)
606 expand (Tcon qtc) = return (Tcon qtc)
607 expand (Tapp t1 t2) =
610 expand (Tforall tb t) =
612 return (Tforall tb t')
613 expand (TransCoercion t1 t2) = do
616 return $ TransCoercion exp1 exp2
617 expand (SymCoercion t) = do
619 return $ SymCoercion exp
620 expand (UnsafeCoercion t1 t2) = do
623 return $ UnsafeCoercion exp1 exp2
624 expand (LeftCoercion t1) = do
626 return $ LeftCoercion exp1
627 expand (RightCoercion t1) = do
629 return $ RightCoercion exp1
630 expand (InstCoercion t1 t2) = do
633 return $ InstCoercion exp1 exp2
634 expapp (t@(Tcon (m,tc))) ts =
635 do env <- mlookupM tsenv_ tsenv eempty m
636 case elookup env tc of
637 Just (formals,rhs) | (length formals) == (length ts) ->
638 return (substl formals ts rhs)
639 _ -> return (foldl Tapp t ts)
640 expapp (Tapp t1 t2) ts =
645 return (foldl Tapp t' ts)
647 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
648 -> CheckResult (Env a b)
649 mlookupM _ _ local_env Nothing = return local_env
650 mlookupM selector external_env local_env (Just m) = do
653 then return external_env
655 globalEnv <- getGlobalEnv
656 case elookup globalEnv m of
657 Just env' -> return (selector env')
658 Nothing -> fail ("Check: undefined module name: "
659 ++ show m ++ show (edomain local_env))
661 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
662 -> Qual a -> CheckResult b
663 qlookupM selector external_env local_env (m,k) =
664 do env <- mlookupM selector external_env local_env m
667 checkLit :: Lit -> CheckResult Ty
668 checkLit (Literal lit t) =
671 do require (t `elem` intLitTypes)
672 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
675 do require (t `elem` ratLitTypes)
676 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
679 do require (t `elem` charLitTypes)
680 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
683 do require (t `elem` stringLitTypes)
684 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
689 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
690 splitTy :: Ty -> ([Tbind],[Ty],Ty)
691 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
692 where (tbs,ts,tr) = splitTy t
693 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
694 where (tbs,ts,tr) = splitTy t
695 splitTy t = ([],[],t)
698 {- Simultaneous substitution on types for type variables,
699 renaming as neceessary to avoid capture.
700 No checks for correct kindedness. -}
701 substl :: [Tvar] -> [Ty] -> Ty -> Ty
702 substl tvs ts t = f (zip tvs ts) t
707 Tvar v -> case lookup v env of
710 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
712 if t `elem` free then
713 Tforall (t',k) (f ((t,Tvar t'):env) t1)
715 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
716 TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
717 SymCoercion t1 -> SymCoercion (f env t1)
718 UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
719 LeftCoercion t1 -> LeftCoercion (f env t1)
720 RightCoercion t1 -> RightCoercion (f env t1)
721 InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
722 where free = foldr union [] (map (freeTvars.snd) env)
725 {- Return free tvars in a type -}
726 freeTvars :: Ty -> [Tvar]
727 freeTvars (Tcon _) = []
728 freeTvars (Tvar v) = [v]
729 freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
730 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
731 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
732 freeTvars (SymCoercion t) = freeTvars t
733 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
734 freeTvars (LeftCoercion t) = freeTvars t
735 freeTvars (RightCoercion t) = freeTvars t
736 freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
738 {- Return any tvar *not* in the argument list. -}
739 freshTvar :: [Tvar] -> Tvar
740 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
742 primCoercionError :: Show a => a -> b
743 primCoercionError s = error $ "Bad coercion application: " ++ show s
746 reportError :: Show a => a -> String -> b
747 reportError e s = error $ ("Core type error: checkExpr failed with "
748 ++ s ++ " and " ++ show e)
750 warn :: String -> CheckResult ()
751 warn s = (unsafePerformIO $ putStrLn ("WARNING: " ++ s)) `seq` return ()