1 {-# OPTIONS -Wall -fno-warn-name-shadowing #-}
2 module Language.Core.Check(
3 checkModule, envsModule,
6 Menv, Venv, Tvenv, Envs(..),
7 CheckRes(..), splitTy, substl) where
9 import Language.Core.Core
10 import Language.Core.Printer()
11 import Language.Core.PrimEnv
12 import Language.Core.Env
14 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 ()
44 type Tvenv = Env Tvar Kind -- type variables (local only)
45 type Tcenv = Env Tcon KindOrCoercion -- type constructors
46 type Cenv = Env Dcon Ty -- data constructors
47 type Venv = Env Var Ty -- values
48 type Menv = Env AnMname Envs -- modules
49 data Envs = Envs {tcenv_::Tcenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
52 {- Extend an environment, checking for illegal shadowing of identifiers (for term
53 variables -- shadowing type variables is allowed.) -}
54 data EnvType = Tv | NotTv
57 extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
58 extendM envType env (k,d) =
60 Just _ | envType == NotTv -> fail ("multiply-defined identifier: "
62 _ -> return (eextend env (k,d))
64 extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
65 extendVenv = extendM NotTv
67 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
68 extendTvenv = extendM Tv
70 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
74 Nothing -> fail ("undefined identifier: " ++ show k)
76 {- Main entry point. -}
77 checkModule :: Menv -> Module -> CheckRes Menv
78 checkModule globalEnv (Module mn tdefs vdefgs) =
80 (do (tcenv, cenv) <- mkTypeEnvs tdefs
81 (e_venv,_) <- foldM (checkVdefg True (tcenv,eempty,cenv))
84 return (eextend globalEnv
85 (mn,Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv})))
86 -- avoid name shadowing
87 (mn, eremove globalEnv mn)
89 -- Like checkModule, but doesn't typecheck the code, instead just
90 -- returning declared types for top-level defns.
91 -- This is necessary in order to handle circular dependencies, but it's sort
93 envsModule :: Menv -> Module -> Menv
94 envsModule globalEnv (Module mn tdefs vdefgs) =
95 let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
96 e_venv = foldr vdefgTypes eempty vdefgs in
97 eextend globalEnv (mn,
98 (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))
99 where vdefgTypes :: Vdefg -> Venv -> Venv
100 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
102 vdefgTypes (Rec vds) e =
103 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
104 add :: [(Qual Var,Ty)] -> Venv -> Venv
105 add pairs e = foldr addOne e pairs
106 addOne :: (Qual Var, Ty) -> Venv -> Venv
107 addOne ((Nothing,_),_) e = e
108 addOne ((Just _,v),t) e = eextend e (v,t)
110 checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
111 checkTdef0 tcenv tdef = ch tdef
113 ch (Data (m,c) tbs _) =
115 requireModulesEq m mn "data type declaration" tdef False
116 extendM NotTv tcenv (c, Kind k)
117 where k = foldr Karrow Klifted (map snd tbs)
118 ch (Newtype (m,c) coVar tbs rhs) =
120 requireModulesEq m mn "newtype declaration" tdef False
121 tcenv' <- extendM NotTv tcenv (c, Kind k)
122 -- add newtype axiom to env
123 tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
125 where k = foldr Karrow Klifted (map snd tbs)
127 processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
128 processTdef0NoChecking tcenv tdef = ch tdef
130 ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)
131 where k = foldr Karrow Klifted (map snd tbs)
132 ch (Newtype tc@(_,c) coercion tbs rhs) =
133 let tcenv' = eextend tcenv (c, Kind k) in
134 -- add newtype axiom to env
136 (snd coercion, Coercion $ DefinedCoercion tbs
137 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))
138 where k = foldr Karrow Klifted (map snd tbs)
140 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty
142 envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv
143 (snd coVar, Coercion $ DefinedCoercion tbs
144 (foldl Tapp (Tcon tyCon)
145 (map Tvar (fst (unzip tbs))),
148 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
149 checkTdef tcenv cenv = ch
151 ch (Data (_,c) utbs cdefs) =
152 do cbinds <- mapM checkCdef cdefs
153 foldM (extendM NotTv) cenv cbinds
154 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
156 requireModulesEq m mn "constructor declaration" cdef
158 tvenv <- foldM (extendM Tv) eempty tbs
159 ks <- mapM (checkTy (tcenv,tvenv)) ts
160 mapM_ (\k -> require (baseKind k)
161 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
162 "kind: " ++ show k) ) ks
164 where tbs = utbs ++ etbs
167 (foldl Tapp (Tcon (Just mn,c))
168 (map (Tvar . fst) utbs)) ts) tbs
169 ch (tdef@(Newtype tc _ tbs t)) =
170 do tvenv <- foldM (extendM Tv) eempty tbs
171 kRhs <- checkTy (tcenv,tvenv) t
172 require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
173 kLhs <- checkTy (tcenv,tvenv)
174 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
175 require (kLhs `eqKind` kRhs)
176 ("Kind mismatch in newtype axiom types: " ++ show tdef
178 (show kLhs) ++ " and " ++ (show kRhs))
181 processCdef :: Cenv -> Tdef -> Cenv
182 processCdef cenv = ch
184 ch (Data (_,c) utbs cdefs) = do
185 let cbinds = map checkCdef cdefs
186 foldl eextend cenv cbinds
187 where checkCdef (Constr (mn,dcon) etbs ts) =
189 where tbs = utbs ++ etbs
192 (foldl Tapp (Tcon (mn,c))
193 (map (Tvar . fst) utbs)) ts) tbs
196 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)
197 mkTypeEnvs tdefs = do
198 tcenv <- foldM checkTdef0 eempty tdefs
199 cenv <- foldM (checkTdef tcenv) eempty tdefs
202 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
203 mkTypeEnvsNoChecking tdefs =
204 let tcenv = foldl processTdef0NoChecking eempty tdefs
205 cenv = foldl processCdef eempty tdefs in
208 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
209 -> Bool -> CheckResult ()
210 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
211 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
213 mkErrMsg :: Show a => String -> a -> String
214 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
216 checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)
217 -> Vdefg -> CheckResult (Venv,Venv)
218 checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
222 do (e_venv', l_venv') <- makeEnv mn vdefs
223 let env' = (tcenv,tvenv,cenv,e_venv',l_venv')
224 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
225 ("unlifted kind in:\n" ++ show vdef)) env')
227 return (e_venv', l_venv')
229 do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)
230 checkVdef (\ vdef k -> do
231 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
232 require ((not top_level) || (not (k `eqKind` Kunlifted)))
233 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
236 where makeEnv mn vdefs = do
237 ev <- foldM extendVenv e_venv e_vts
238 lv <- foldM extendVenv l_venv l_vts
240 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
241 not (vdefIsMainWrapper mn (Just m))]
242 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
243 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
245 let isZcMain = vdefIsMainWrapper mn m
247 requireModulesEq m mn "value definition" vdef True
248 k <- checkTy (tcenv,tvenv) t
252 ("declared type doesn't match expression type in:\n"
253 ++ show vdef ++ "\n" ++
254 "declared type: " ++ show t ++ "\n" ++
255 "expression type: " ++ show t')
257 vdefIsMainWrapper :: AnMname -> Mname -> Bool
258 vdefIsMainWrapper enclosing defining =
259 enclosing == mainMname && defining == wrapperMainAnMname
261 checkExpr :: AnMname -> Menv -> [Tdef] -> Venv -> Tvenv
263 checkExpr mn menv tdefs venv tvenv e = case runReaderT (do
264 (tcenv, cenv) <- mkTypeEnvs tdefs
265 -- Since the preprocessor calls checkExpr after code has been
266 -- typechecked, we expect to find the external env in the Menv.
267 case (elookup menv mn) of
269 checkExp (tcenv, tvenv, cenv, (venv_ thisEnv), venv) e
270 Nothing -> reportError e ("checkExpr: Environment for " ++
271 show mn ++ " not found")) (mn,menv) of
273 FailC s -> reportError e s
275 checkType :: AnMname -> Menv -> [Tdef] -> Tvenv -> Ty -> Kind
276 checkType mn menv tdefs tvenv t = case runReaderT (do
277 (tcenv, _) <- mkTypeEnvs tdefs
278 checkTy (tcenv, tvenv) t) (mn, menv) of
280 FailC s -> reportError tvenv s
282 checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
283 checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
288 qlookupM venv_ e_venv l_venv qv
290 qlookupM cenv_ cenv eempty qc
295 k' <- checkTy (tcenv,tvenv) t
298 do require (k' `subKindOf` k)
299 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
300 "operator kind: " ++ show k ++ "\n" ++
301 "operand kind: " ++ show k')
302 return (substl [tv] [t] t0)
303 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
304 "operator type: " ++ show t')
309 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
310 do require (t2 == t')
311 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
312 "operator type: " ++ show t' ++ "\n" ++
313 "operand type: " ++ show t2)
315 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
316 "operator type: " ++ show t1)
318 do tvenv' <- extendTvenv tvenv tb
319 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e
320 return (Tforall tb t)
321 Lam (Vb (vb@(_,vt))) e ->
322 do k <- checkTy (tcenv,tvenv) vt
324 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
326 l_venv' <- extendVenv l_venv vb
327 t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e
328 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
331 do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
332 (e_venv,l_venv) vdefg
333 checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e
334 Case e (v,t) resultTy alts ->
336 checkTy (tcenv,tvenv) t
338 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
339 "declared type: " ++ show t ++ "\n" ++
340 "expression type: " ++ show t')
341 case (reverse alts) of
343 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
344 ("duplicate alternative in case:\n" ++ show e0)
346 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
347 ok [Adefault _] _ = return ()
348 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
352 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
353 ok ((Alit l _):as) ls = do require (notElem l ls)
354 ("duplicate alternative in case:\n" ++ show e0)
356 ok [Adefault _] _ = return ()
357 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
358 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
360 [Adefault _] -> return ()
361 _ -> fail ("no alternatives in case:\n" ++ show e0)
362 l_venv' <- extendVenv l_venv (v,t)
363 t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
364 require (all (== t) ts)
365 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
366 "types: " ++ show (t:ts))
367 checkTy (tcenv,tvenv) resultTy
368 require (t == resultTy) ("case alternative type doesn't " ++
369 " match case return type in:\n" ++ show e0 ++ "\n" ++
370 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
374 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
375 require (eTy == fromTy) ("Type mismatch in cast: c = "
376 ++ show c ++ "\nand eTy = " ++ show eTy
377 ++ "\n and " ++ show fromTy)
382 do checkTy (tcenv,eempty) t {- external types must be closed -}
385 checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
386 checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
390 Acon qc etbs vbs e ->
392 where f (Tapp t0 t) = f t0 ++ [t]
394 ct <- qlookupM cenv_ cenv eempty qc
395 let (tbs,ct_args0,ct_res0) = splitTy ct
397 let (utbs,etbs') = splitAt (length uts) tbs
398 let utvs = map fst utbs
399 {- check existentials -}
400 let (etvs,eks) = unzip etbs
401 let (etvs',eks') = unzip etbs'
402 require (all (uncurry eqKind)
404 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
405 "kinds declared in data constructor: " ++ show eks ++
406 "kinds declared in case alternative: " ++ show eks')
407 tvenv' <- foldM extendTvenv tvenv etbs
408 {- check term variables -}
409 let vts = map snd vbs
410 mapM_ (\vt -> require ((not . isUtupleTy) vt)
411 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
412 "pattern type: " ++ show vt)) vts
413 vks <- mapM (checkTy (tcenv,tvenv')) vts
414 mapM_ (\vk -> require (baseKind vk)
415 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
416 "kind: " ++ show vk)) vks
417 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
420 require (ct_arg == vt)
421 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
422 "pattern variable type: " ++ show ct_arg ++ "\n" ++
423 "constructor argument type: " ++ show vt)) ct_args vts
424 require (ct_res == t0)
425 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
426 "pattern constructor type: " ++ show ct_res ++ "\n" ++
427 "scrutinee type: " ++ show t0)
428 l_venv' <- foldM extendVenv l_venv vbs
429 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e
430 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
435 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
436 "pattern type: " ++ show t ++ "\n" ++
437 "scrutinee type: " ++ show t0)
442 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
443 checkTy es@(tcenv,tvenv) = ch
445 ch (Tvar tv) = lookupM tvenv tv
447 kOrC <- qlookupM tcenv_ tcenv eempty qtc
450 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
451 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
452 ch (t@(Tapp t1 t2)) =
453 case splitTyConApp_maybe t of
455 tcK <- qlookupM tcenv_ tcenv eempty tc
457 Kind _ -> checkTapp t1 t2
458 Coercion (DefinedCoercion tbs (from,to)) -> do
459 -- makes sure coercion is fully applied
460 require (length tys == length tbs) $
461 ("Arity mismatch in coercion app: " ++ show t)
462 let (tvs, tks) = unzip tbs
463 argKs <- mapM (checkTy es) tys
464 let kPairs = zip argKs tks
465 -- Simon says it's okay for these to be
467 let kindsOk = all (uncurry subKindOf) kPairs
469 ("Kind mismatch in coercion app: " ++ show tks
470 ++ " and " ++ show argKs ++ " t = " ++ show t)
471 return $ Keq (substl tvs tys from) (substl tvs tys to)
472 Nothing -> checkTapp t1 t2
473 where checkTapp t1 t2 = do
478 require (k2 `subKindOf` k11) kindError
481 "kinds don't match in type application: "
483 "operator kind: " ++ show k11 ++ "\n" ++
484 "operand kind: " ++ show k2
485 _ -> fail ("applied type has non-arrow kind: " ++ show t)
488 do tvenv' <- extendTvenv tvenv tb
489 checkTy (tcenv,tvenv') t
490 ch (TransCoercion t1 t2) = do
491 (ty1,ty2) <- checkTyCo es t1
492 (ty3,ty4) <- checkTyCo es t2
493 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
494 show ty2 ++ " and " ++ show ty3)
496 ch (SymCoercion t1) = do
497 (ty1,ty2) <- checkTyCo es t1
499 ch (UnsafeCoercion t1 t2) = do
503 ch (LeftCoercion t1) = do
506 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
507 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
508 ch (RightCoercion t1) = do
511 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
512 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
513 ch (InstCoercion ty arg) = do
514 forallK <- checkTyCo es ty
516 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
517 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
519 argK <- checkTy es arg
520 require (argK `eqKind` k1) ("Kind mismatch in type being "
521 ++ "instantiated: " ++ show arg)
522 let newLhs = substl [v1] [arg] b1
523 let newRhs = substl [v2] [arg] b2
524 return $ Keq newLhs newRhs
525 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
527 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
528 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
529 (case splitTyConApp_maybe t of
531 tcK <- qlookupM tcenv_ tcenv eempty tc
533 -- todo: avoid duplicating this code
534 -- blah, this almost calls for a different syntactic form
535 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
536 Coercion (DefinedCoercion tbs (from, to)) -> do
537 require (length tys == length tbs) $
538 ("Arity mismatch in coercion app: " ++ show t)
539 let (tvs, tks) = unzip tbs
540 argKs <- mapM (checkTy es) tys
541 let kPairs = zip argKs tks
542 let kindsOk = all (uncurry subKindOf) kPairs
544 ("Kind mismatch in coercion app: " ++ show tks
545 ++ " and " ++ show argKs ++ " t = " ++ show t)
546 return (substl tvs tys from, substl tvs tys to)
548 _ -> checkTapp t1 t2)
549 where checkTapp t1 t2 = do
550 (lhsRator, rhsRator) <- checkTyCo es t1
551 (lhs, rhs) <- checkTyCo es t2
552 -- Comp rule from paper
553 checkTy es (Tapp lhsRator lhs)
554 checkTy es (Tapp rhsRator rhs)
555 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
556 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
557 tvenv' <- extendTvenv tvenv tb
558 (t1,t2) <- checkTyCo (tcenv, tvenv') t
559 return (Tforall tb t1, Tforall tb t2)
563 Keq t1 t2 -> return (t1, t2)
564 -- otherwise, expand by the "refl" rule
567 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
568 -> CheckResult (Env a b)
569 mlookupM _ _ local_env Nothing = return local_env
570 mlookupM selector external_env local_env (Just m) = do
573 then return external_env
575 globalEnv <- getGlobalEnv
576 case elookup globalEnv m of
577 Just env' -> return (selector env')
578 Nothing -> fail ("Check: undefined module name: "
579 ++ show m ++ show (edomain local_env))
581 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
582 -> Qual a -> CheckResult b
583 qlookupM selector external_env local_env (m,k) =
584 do env <- mlookupM selector external_env local_env m
587 checkLit :: Lit -> CheckResult Ty
588 checkLit (Literal lit t) =
591 do require (t `elem` intLitTypes)
592 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
595 do require (t `elem` ratLitTypes)
596 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
599 do require (t `elem` charLitTypes)
600 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
603 do require (t `elem` stringLitTypes)
604 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
609 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
610 splitTy :: Ty -> ([Tbind],[Ty],Ty)
611 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
612 where (tbs,ts,tr) = splitTy t
613 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
614 where (tbs,ts,tr) = splitTy t
615 splitTy t = ([],[],t)
618 {- Simultaneous substitution on types for type variables,
619 renaming as neceessary to avoid capture.
620 No checks for correct kindedness. -}
621 substl :: [Tvar] -> [Ty] -> Ty -> Ty
622 substl tvs ts t = f (zip tvs ts) t
627 Tvar v -> case lookup v env of
630 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
632 if t `elem` free then
633 Tforall (t',k) (f ((t,Tvar t'):env) t1)
635 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
636 TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
637 SymCoercion t1 -> SymCoercion (f env t1)
638 UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
639 LeftCoercion t1 -> LeftCoercion (f env t1)
640 RightCoercion t1 -> RightCoercion (f env t1)
641 InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
642 where free = foldr union [] (map (freeTvars.snd) env)
645 {- Return free tvars in a type -}
646 freeTvars :: Ty -> [Tvar]
647 freeTvars (Tcon _) = []
648 freeTvars (Tvar v) = [v]
649 freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
650 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
651 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
652 freeTvars (SymCoercion t) = freeTvars t
653 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
654 freeTvars (LeftCoercion t) = freeTvars t
655 freeTvars (RightCoercion t) = freeTvars t
656 freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
658 {- Return any tvar *not* in the argument list. -}
659 freshTvar :: [Tvar] -> Tvar
660 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
662 primCoercionError :: Show a => a -> b
663 primCoercionError s = error $ "Bad coercion application: " ++ show s
666 reportError :: Show a => a -> String -> b
667 reportError e s = error $ ("Core type error: checkExpr failed with "
668 ++ s ++ " and " ++ show e)