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
10 import Language.Core.Core
11 import Language.Core.Printer()
12 import Language.Core.PrimEnv
13 import Language.Core.Env
14 import Language.Core.Environments
16 import Control.Monad.Reader
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 ()
46 extendM :: (Ord a, Show a) => EnvType -> Env a b -> (a,b) -> CheckResult (Env a b)
47 extendM envType env (k,d) =
49 Just _ | envType == NotTv -> fail ("multiply-defined identifier: "
51 _ -> return (eextend env (k,d))
53 extendVenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
54 extendVenv = extendM NotTv
56 extendTvenv :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
57 extendTvenv = extendM Tv
59 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
63 Nothing -> fail ("undefined identifier: " ++ show k ++ " e = " ++ show (edomain env))
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})))
75 -- avoid name shadowing
76 (mn, eremove globalEnv mn)
78 -- Like checkModule, but doesn't typecheck the code, instead just
79 -- returning declared types for top-level defns.
80 -- This is necessary in order to handle circular dependencies, but it's sort
82 envsModule :: Menv -> Module -> Menv
83 envsModule globalEnv (Module mn tdefs vdefgs) =
84 let (tcenv, cenv) = mkTypeEnvsNoChecking tdefs
85 e_venv = foldr vdefgTypes eempty vdefgs in
86 eextend globalEnv (mn,
87 (Envs{tcenv_=tcenv,cenv_=cenv,venv_=e_venv}))
88 where vdefgTypes :: Vdefg -> Venv -> Venv
89 vdefgTypes (Nonrec (Vdef (v,t,_))) e =
91 vdefgTypes (Rec vds) e =
92 add (map (\ (Vdef (v,t,_)) -> (v,t)) vds) e
93 add :: [(Qual Var,Ty)] -> Venv -> Venv
94 add pairs e = foldr addOne e pairs
95 addOne :: (Qual Var, Ty) -> Venv -> Venv
96 addOne ((Nothing,_),_) e = e
97 addOne ((Just _,v),t) e = eextend e (v,t)
99 checkTdef0 :: Tcenv -> Tdef -> CheckResult Tcenv
100 checkTdef0 tcenv tdef = ch tdef
102 ch (Data (m,c) tbs _) =
104 requireModulesEq m mn "data type declaration" tdef False
105 extendM NotTv tcenv (c, Kind k)
106 where k = foldr Karrow Klifted (map snd tbs)
107 ch (Newtype (m,c) coVar tbs rhs) =
109 requireModulesEq m mn "newtype declaration" tdef False
110 tcenv' <- extendM NotTv tcenv (c, Kind k)
111 -- add newtype axiom to env
112 tcenv'' <- envPlusNewtype tcenv' (m,c) coVar tbs rhs
114 where k = foldr Karrow Klifted (map snd tbs)
116 processTdef0NoChecking :: Tcenv -> Tdef -> Tcenv
117 processTdef0NoChecking tcenv tdef = ch tdef
119 ch (Data (_,c) tbs _) = eextend tcenv (c, Kind k)
120 where k = foldr Karrow Klifted (map snd tbs)
121 ch (Newtype tc@(_,c) coercion tbs rhs) =
122 let tcenv' = eextend tcenv (c, Kind k) in
123 -- add newtype axiom to env
125 (snd coercion, Coercion $ DefinedCoercion tbs
126 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))), rhs))
127 where k = foldr Karrow Klifted (map snd tbs)
129 envPlusNewtype :: Tcenv -> Qual Tcon -> Qual Tcon -> [Tbind] -> Ty
131 envPlusNewtype tcenv tyCon coVar tbs rep = extendM NotTv tcenv
132 (snd coVar, Coercion $ DefinedCoercion tbs
133 (foldl Tapp (Tcon tyCon)
134 (map Tvar (fst (unzip tbs))),
137 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
138 checkTdef tcenv cenv = ch
140 ch (Data (_,c) utbs cdefs) =
141 do cbinds <- mapM checkCdef cdefs
142 foldM (extendM NotTv) cenv cbinds
143 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
145 requireModulesEq m mn "constructor declaration" cdef
147 tvenv <- foldM (extendM Tv) eempty tbs
148 ks <- mapM (checkTy (tcenv,tvenv)) ts
149 mapM_ (\k -> require (baseKind k)
150 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
151 "kind: " ++ show k) ) ks
153 where tbs = utbs ++ etbs
156 (foldl Tapp (Tcon (Just mn,c))
157 (map (Tvar . fst) utbs)) ts) tbs
158 ch (tdef@(Newtype tc _ tbs t)) =
159 do tvenv <- foldM (extendM Tv) eempty tbs
160 kRhs <- checkTy (tcenv,tvenv) t
161 require (kRhs `eqKind` Klifted) ("bad kind:\n" ++ show tdef)
162 kLhs <- checkTy (tcenv,tvenv)
163 (foldl Tapp (Tcon tc) (map Tvar (fst (unzip tbs))))
164 require (kLhs `eqKind` kRhs)
165 ("Kind mismatch in newtype axiom types: " ++ show tdef
167 (show kLhs) ++ " and " ++ (show kRhs))
170 processCdef :: Cenv -> Tdef -> Cenv
171 processCdef cenv = ch
173 ch (Data (_,c) utbs cdefs) = do
174 let cbinds = map checkCdef cdefs
175 foldl eextend cenv cbinds
176 where checkCdef (Constr (mn,dcon) etbs ts) =
178 where tbs = utbs ++ etbs
181 (foldl Tapp (Tcon (mn,c))
182 (map (Tvar . fst) utbs)) ts) tbs
185 mkTypeEnvs :: [Tdef] -> CheckResult (Tcenv, Cenv)
186 mkTypeEnvs tdefs = do
187 tcenv <- foldM checkTdef0 eempty tdefs
188 cenv <- foldM (checkTdef tcenv) eempty tdefs
191 mkTypeEnvsNoChecking :: [Tdef] -> (Tcenv, Cenv)
192 mkTypeEnvsNoChecking tdefs =
193 let tcenv = foldl processTdef0NoChecking eempty tdefs
194 cenv = foldl processCdef eempty tdefs in
197 requireModulesEq :: Show a => Mname -> AnMname -> String -> a
198 -> Bool -> CheckResult ()
199 requireModulesEq (Just mn) m msg t _ = require (mn == m) (mkErrMsg msg t)
200 requireModulesEq Nothing _ msg t emptyOk = require emptyOk (mkErrMsg msg t)
202 mkErrMsg :: Show a => String -> a -> String
203 mkErrMsg msg t = "wrong module name in " ++ msg ++ ":\n" ++ show t
205 checkVdefg :: Bool -> (Tcenv,Tvenv,Cenv) -> (Venv,Venv)
206 -> Vdefg -> CheckResult (Venv,Venv)
207 checkVdefg top_level (tcenv,tvenv,cenv) (e_venv,l_venv) vdefg = do
211 do (e_venv', l_venv') <- makeEnv mn vdefs
212 let env' = (tcenv,tvenv,cenv,e_venv',l_venv')
213 mapM_ (checkVdef (\ vdef k -> require (k `eqKind` Klifted)
214 ("unlifted kind in:\n" ++ show vdef)) env')
216 return (e_venv', l_venv')
218 do let env' = (tcenv, tvenv, cenv, e_venv, l_venv)
219 checkVdef (\ vdef k -> do
220 require (not (k `eqKind` Kopen)) ("open kind in:\n" ++ show vdef)
221 require ((not top_level) || (not (k `eqKind` Kunlifted)))
222 ("top-level unlifted kind in:\n" ++ show vdef)) env' vdef
225 where makeEnv mn vdefs = do
226 ev <- foldM extendVenv e_venv e_vts
227 lv <- foldM extendVenv l_venv l_vts
229 where e_vts = [ (v,t) | Vdef ((Just m,v),t,_) <- vdefs,
230 not (vdefIsMainWrapper mn (Just m))]
231 l_vts = [ (v,t) | Vdef ((Nothing,v),t,_) <- vdefs]
232 checkVdef checkKind env (vdef@(Vdef ((m,_),t,e))) = do
234 let isZcMain = vdefIsMainWrapper mn m
236 requireModulesEq m mn "value definition" vdef True
237 k <- checkTy (tcenv,tvenv) t
241 ("declared type doesn't match expression type in:\n"
242 ++ show vdef ++ "\n" ++
243 "declared type: " ++ show t ++ "\n" ++
244 "expression type: " ++ show t')
246 vdefIsMainWrapper :: AnMname -> Mname -> Bool
247 vdefIsMainWrapper enclosing defining =
248 enclosing == mainMname && defining == wrapperMainAnMname
250 checkExpr :: AnMname -> Menv -> Tcenv -> Cenv -> Venv -> Tvenv
252 checkExpr mn menv _tcenv _cenv venv tvenv e = case runReaderT (do
253 --(tcenv, cenv) <- mkTypeEnvs tdefs
254 -- Since the preprocessor calls checkExpr after code has been
255 -- typechecked, we expect to find the external env in the Menv.
256 case (elookup menv mn) of
258 checkExp ({-tcenv-}tcenv_ thisEnv, tvenv, {-cenv-}cenv_ thisEnv, (venv_ thisEnv), venv) e
259 Nothing -> reportError e ("checkExpr: Environment for " ++
260 show mn ++ " not found")) (mn,menv) of
262 FailC s -> reportError e s
264 checkType :: AnMname -> Menv -> Tcenv -> Tvenv -> Ty -> Kind
265 checkType mn menv _tcenv tvenv t =
266 case runReaderT (checkTy (tcenv_ (fromMaybe (error "checkType") (elookup menv mn)), tvenv) t) (mn, menv) of
268 FailC s -> reportError tvenv (s ++ "\n " ++ show menv ++ "\n mname =" ++ show mn)
270 checkExp :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
271 checkExp (tcenv,tvenv,cenv,e_venv,l_venv) = ch
276 qlookupM venv_ e_venv l_venv qv
278 qlookupM cenv_ cenv eempty qc
283 k' <- checkTy (tcenv,tvenv) t
286 do require (k' `subKindOf` k)
287 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
288 "operator kind: " ++ show k ++ "\n" ++
289 "operand kind: " ++ show k')
290 return (substl [tv] [t] t0)
291 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
292 "operator type: " ++ show t')
297 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
298 do require (t2 == t')
299 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
300 "operator type: " ++ show t' ++ "\n" ++
301 "operand type: " ++ show t2)
303 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
304 "operator type: " ++ show t1)
306 do tvenv' <- extendTvenv tvenv tb
307 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv) e
308 return (Tforall tb t)
309 Lam (Vb (vb@(_,vt))) e ->
310 do k <- checkTy (tcenv,tvenv) vt
312 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
314 l_venv' <- extendVenv l_venv vb
315 t <- checkExp (tcenv,tvenv,cenv,e_venv,l_venv') e
316 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
319 do (e_venv',l_venv') <- checkVdefg False (tcenv,tvenv,cenv)
320 (e_venv,l_venv) vdefg
321 checkExp (tcenv,tvenv,cenv,e_venv',l_venv') e
322 Case e (v,t) resultTy alts ->
324 checkTy (tcenv,tvenv) t
326 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
327 "declared type: " ++ show t ++ "\n" ++
328 "expression type: " ++ show t')
329 case (reverse alts) of
331 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
332 ("duplicate alternative in case:\n" ++ show e0)
334 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
335 ok [Adefault _] _ = return ()
336 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
340 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
341 ok ((Alit l _):as) ls = do require (notElem l ls)
342 ("duplicate alternative in case:\n" ++ show e0)
344 ok [Adefault _] _ = return ()
345 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
346 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
348 [Adefault _] -> return ()
349 _ -> fail ("no alternatives in case:\n" ++ show e0)
350 l_venv' <- extendVenv l_venv (v,t)
351 t:ts <- mapM (checkAlt (tcenv,tvenv,cenv,e_venv,l_venv') t) alts
352 require (all (== t) ts)
353 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
354 "types: " ++ show (t:ts))
355 checkTy (tcenv,tvenv) resultTy
356 require (t == resultTy) ("case alternative type doesn't " ++
357 " match case return type in:\n" ++ show e0 ++ "\n" ++
358 "alt type: " ++ show t ++ " return type: " ++ show resultTy)
362 (fromTy, toTy) <- checkTyCo (tcenv,tvenv) t
363 require (eTy == fromTy) ("Type mismatch in cast: c = "
364 ++ show c ++ "\nand eTy = " ++ show eTy
365 ++ "\n and " ++ show fromTy)
370 do checkTy (tcenv,eempty) t {- external types must be closed -}
373 checkAlt :: (Tcenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
374 checkAlt (env@(tcenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
378 Acon qc etbs vbs e ->
380 where f (Tapp t0 t) = f t0 ++ [t]
382 ct <- qlookupM cenv_ cenv eempty qc
383 let (tbs,ct_args0,ct_res0) = splitTy ct
385 let (utbs,etbs') = splitAt (length uts) tbs
386 let utvs = map fst utbs
387 {- check existentials -}
388 let (etvs,eks) = unzip etbs
389 let (etvs',eks') = unzip etbs'
390 require (all (uncurry eqKind)
392 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
393 "kinds declared in data constructor: " ++ show eks ++
394 "kinds declared in case alternative: " ++ show eks')
395 tvenv' <- foldM extendTvenv tvenv etbs
396 {- check term variables -}
397 let vts = map snd vbs
398 mapM_ (\vt -> require ((not . isUtupleTy) vt)
399 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
400 "pattern type: " ++ show vt)) vts
401 vks <- mapM (checkTy (tcenv,tvenv')) vts
402 mapM_ (\vk -> require (baseKind vk)
403 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
404 "kind: " ++ show vk)) vks
405 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
408 require (ct_arg == vt)
409 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
410 "pattern variable type: " ++ show ct_arg ++ "\n" ++
411 "constructor argument type: " ++ show vt)) ct_args vts
412 require (ct_res == t0)
413 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
414 "pattern constructor type: " ++ show ct_res ++ "\n" ++
415 "scrutinee type: " ++ show t0)
416 l_venv' <- foldM extendVenv l_venv vbs
417 t <- checkExp (tcenv,tvenv',cenv,e_venv,l_venv') e
418 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
423 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
424 "pattern type: " ++ show t ++ "\n" ++
425 "scrutinee type: " ++ show t0)
430 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
431 checkTy es@(tcenv,tvenv) = ch
433 ch (Tvar tv) = lookupM tvenv tv
435 kOrC <- qlookupM tcenv_ tcenv eempty qtc
438 Coercion (DefinedCoercion [] (t1,t2)) -> return $ Keq t1 t2
439 Coercion _ -> fail ("Unsaturated coercion app: " ++ show qtc)
440 ch (t@(Tapp t1 t2)) =
441 case splitTyConApp_maybe t of
443 tcK <- qlookupM tcenv_ tcenv eempty tc
445 Kind _ -> checkTapp t1 t2
446 Coercion (DefinedCoercion tbs (from,to)) -> do
447 -- makes sure coercion is fully applied
448 require (length tys == length tbs) $
449 ("Arity mismatch in coercion app: " ++ show t)
450 let (tvs, tks) = unzip tbs
451 argKs <- mapM (checkTy es) tys
452 let kPairs = zip argKs tks
453 -- Simon says it's okay for these to be
455 let kindsOk = all (uncurry subKindOf) kPairs
457 ("Kind mismatch in coercion app: " ++ show tks
458 ++ " and " ++ show argKs ++ " t = " ++ show t)
459 return $ Keq (substl tvs tys from) (substl tvs tys to)
460 Nothing -> checkTapp t1 t2
461 where checkTapp t1 t2 = do
466 require (k2 `subKindOf` k11) kindError
469 "kinds don't match in type application: "
471 "operator kind: " ++ show k11 ++ "\n" ++
472 "operand kind: " ++ show k2
473 _ -> fail ("applied type has non-arrow kind: " ++ show t)
476 do tvenv' <- extendTvenv tvenv tb
477 checkTy (tcenv,tvenv') t
478 ch (TransCoercion t1 t2) = do
479 (ty1,ty2) <- checkTyCo es t1
480 (ty3,ty4) <- checkTyCo es t2
481 require (ty2 == ty3) ("Types don't match in trans. coercion: " ++
482 show ty2 ++ " and " ++ show ty3)
484 ch (SymCoercion t1) = do
485 (ty1,ty2) <- checkTyCo es t1
487 ch (UnsafeCoercion t1 t2) = do
491 ch (LeftCoercion t1) = do
494 ((Tapp u _), (Tapp w _)) -> return $ Keq u w
495 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
496 ch (RightCoercion t1) = do
499 ((Tapp _ v), (Tapp _ x)) -> return $ Keq v x
500 _ -> fail ("Bad coercion kind in operand of left: " ++ show k)
501 ch (InstCoercion ty arg) = do
502 forallK <- checkTyCo es ty
504 ((Tforall (v1,k1) b1), (Tforall (v2,k2) b2)) -> do
505 require (k1 `eqKind` k2) ("Kind mismatch in argument of inst: "
507 argK <- checkTy es arg
508 require (argK `eqKind` k1) ("Kind mismatch in type being "
509 ++ "instantiated: " ++ show arg)
510 let newLhs = substl [v1] [arg] b1
511 let newRhs = substl [v2] [arg] b2
512 return $ Keq newLhs newRhs
513 _ -> fail ("Non-forall-ty in argument to inst: " ++ show ty)
515 checkTyCo :: (Tcenv, Tvenv) -> Ty -> CheckResult (Ty, Ty)
516 checkTyCo es@(tcenv,_) t@(Tapp t1 t2) =
517 (case splitTyConApp_maybe t of
519 tcK <- qlookupM tcenv_ tcenv eempty tc
521 -- todo: avoid duplicating this code
522 -- blah, this almost calls for a different syntactic form
523 -- (for a defined-coercion app): (TCoercionApp Tcon [Ty])
524 Coercion (DefinedCoercion tbs (from, to)) -> do
525 require (length tys == length tbs) $
526 ("Arity mismatch in coercion app: " ++ show t)
527 let (tvs, tks) = unzip tbs
528 argKs <- mapM (checkTy es) tys
529 let kPairs = zip argKs tks
530 let kindsOk = all (uncurry subKindOf) kPairs
532 ("Kind mismatch in coercion app: " ++ show tks
533 ++ " and " ++ show argKs ++ " t = " ++ show t)
534 return (substl tvs tys from, substl tvs tys to)
536 _ -> checkTapp t1 t2)
537 where checkTapp t1 t2 = do
538 (lhsRator, rhsRator) <- checkTyCo es t1
539 (lhs, rhs) <- checkTyCo es t2
540 -- Comp rule from paper
541 checkTy es (Tapp lhsRator lhs)
542 checkTy es (Tapp rhsRator rhs)
543 return (Tapp lhsRator lhs, Tapp rhsRator rhs)
544 checkTyCo (tcenv, tvenv) (Tforall tb t) = do
545 tvenv' <- extendTvenv tvenv tb
546 (t1,t2) <- checkTyCo (tcenv, tvenv') t
547 return (Tforall tb t1, Tforall tb t2)
551 Keq t1 t2 -> return (t1, t2)
552 -- otherwise, expand by the "refl" rule
555 mlookupM :: (Eq a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> Mname
556 -> CheckResult (Env a b)
557 mlookupM _ _ local_env Nothing = return local_env
558 mlookupM selector external_env local_env (Just m) = do
561 then return external_env
563 globalEnv <- getGlobalEnv
564 case elookup globalEnv m of
565 Just env' -> return (selector env')
566 Nothing -> fail ("Check: undefined module name: "
567 ++ show m ++ show (edomain local_env))
569 qlookupM :: (Ord a, Show a,Show b) => (Envs -> Env a b) -> Env a b -> Env a b
570 -> Qual a -> CheckResult b
571 qlookupM selector external_env local_env (m,k) =
572 do env <- mlookupM selector external_env local_env m
575 checkLit :: Lit -> CheckResult Ty
576 checkLit (Literal lit t) =
579 do require (t `elem` intLitTypes)
580 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
583 do require (t `elem` ratLitTypes)
584 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
587 do require (t `elem` charLitTypes)
588 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
591 do require (t `elem` stringLitTypes)
592 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t)
597 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
598 splitTy :: Ty -> ([Tbind],[Ty],Ty)
599 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
600 where (tbs,ts,tr) = splitTy t
601 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
602 where (tbs,ts,tr) = splitTy t
603 splitTy t = ([],[],t)
606 {- Simultaneous substitution on types for type variables,
607 renaming as neceessary to avoid capture.
608 No checks for correct kindedness. -}
609 substl :: [Tvar] -> [Ty] -> Ty -> Ty
610 substl tvs ts t = f (zip tvs ts) t
615 Tvar v -> case lookup v env of
618 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
620 if t `elem` free then
621 Tforall (t',k) (f ((t,Tvar t'):env) t1)
623 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
624 TransCoercion t1 t2 -> TransCoercion (f env t1) (f env t2)
625 SymCoercion t1 -> SymCoercion (f env t1)
626 UnsafeCoercion t1 t2 -> UnsafeCoercion (f env t1) (f env t2)
627 LeftCoercion t1 -> LeftCoercion (f env t1)
628 RightCoercion t1 -> RightCoercion (f env t1)
629 InstCoercion t1 t2 -> InstCoercion (f env t1) (f env t2)
630 where free = foldr union [] (map (freeTvars.snd) env)
633 {- Return free tvars in a type -}
634 freeTvars :: Ty -> [Tvar]
635 freeTvars (Tcon _) = []
636 freeTvars (Tvar v) = [v]
637 freeTvars (Tapp t1 t2) = freeTvars t1 `union` freeTvars t2
638 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
639 freeTvars (TransCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
640 freeTvars (SymCoercion t) = freeTvars t
641 freeTvars (UnsafeCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
642 freeTvars (LeftCoercion t) = freeTvars t
643 freeTvars (RightCoercion t) = freeTvars t
644 freeTvars (InstCoercion t1 t2) = freeTvars t1 `union` freeTvars t2
646 {- Return any tvar *not* in the argument list. -}
647 freshTvar :: [Tvar] -> Tvar
648 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!
650 primCoercionError :: Show a => a -> b
651 primCoercionError s = error $ "Bad coercion application: " ++ show s
654 reportError :: Show a => a -> String -> b
655 reportError e s = error $ ("Core type error: checkExpr failed with "
656 ++ s ++ " and " ++ show e)