9 {- Checking is done in a simple error monad. In addition to
10 allowing errors to be captured, this makes it easy to guarantee
11 that checking itself has been completed for an entire module. -}
13 data CheckResult a = OkC a | FailC String
15 instance Monad CheckResult where
17 FailC s >>= k = fail s
21 require :: Bool -> String -> CheckResult ()
22 require False s = fail s
23 require True _ = return ()
25 requireM :: CheckResult Bool -> String -> CheckResult ()
31 type Tvenv = Env Tvar Kind -- type variables (local only)
32 type Tcenv = Env Tcon Kind -- type constructors
33 type Tsenv = Env Tcon ([Tvar],Ty) -- type synonyms
34 type Cenv = Env Dcon Ty -- data constructors
35 type Venv = Env Var Ty -- values
36 type Menv = Env Mname Envs -- modules
37 data Envs = Envs {tcenv_::Tcenv,tsenv_::Tsenv,cenv_::Cenv,venv_::Venv} -- all the exportable envs
39 {- Extend an environment, checking for illegal shadowing of identifiers. -}
40 extendM :: (Ord a, Show a) => Env a b -> (a,b) -> CheckResult (Env a b)
43 Just _ -> fail ("multiply-defined identifier: " ++ show k)
44 Nothing -> return (eextend env (k,d))
46 lookupM :: (Ord a, Show a) => Env a b -> a -> CheckResult b
50 Nothing -> fail ("undefined identifier: " ++ show k)
52 {- Main entry point. -}
53 checkModule :: Menv -> Module -> CheckResult Menv
54 checkModule globalEnv (Module mn tdefs vdefgs) =
55 do (tcenv,tsenv) <- foldM checkTdef0 (eempty,eempty) tdefs
56 cenv <- foldM (checkTdef tcenv) eempty tdefs
57 (e_venv,l_venv) <- foldM (checkVdefg True (tcenv,tsenv,eempty,cenv)) (eempty,eempty) vdefgs
58 return (eextend globalEnv (mn,Envs{tcenv_=tcenv,tsenv_=tsenv,cenv_=cenv,venv_=e_venv}))
61 checkTdef0 :: (Tcenv,Tsenv) -> Tdef -> CheckResult (Tcenv,Tsenv)
62 checkTdef0 (tcenv,tsenv) tdef = ch tdef
64 ch (Data (m,c) tbs _) =
65 do require (m == mn) ("wrong module name in data type declaration:\n" ++ show tdef)
66 tcenv' <- extendM tcenv (c,k)
68 where k = foldr Karrow Klifted (map snd tbs)
69 ch (Newtype (m,c) tbs rhs) =
70 do require (m == mn) ("wrong module name in newtype declaration:\n" ++ show tdef)
71 tcenv' <- extendM tcenv (c,k)
73 Nothing -> return tsenv
74 Just rep -> extendM tsenv (c,(map fst tbs,rep))
75 return (tcenv', tsenv')
76 where k = foldr Karrow Klifted (map snd tbs)
78 checkTdef :: Tcenv -> Cenv -> Tdef -> CheckResult Cenv
79 checkTdef tcenv cenv = ch
81 ch (Data (_,c) utbs cdefs) =
82 do cbinds <- mapM checkCdef cdefs
83 foldM extendM cenv cbinds
84 where checkCdef (cdef@(Constr (m,dcon) etbs ts)) =
85 do require (m == mn) ("wrong module name in constructor declaration:\n" ++ show cdef)
86 tvenv <- foldM extendM eempty tbs
87 ks <- mapM (checkTy (tcenv,tvenv)) ts
88 mapM_ (\k -> require (baseKind k)
89 ("higher-order kind in:\n" ++ show cdef ++ "\n" ++
90 "kind: " ++ show k) ) ks
92 where tbs = utbs ++ etbs
95 (foldl Tapp (Tcon (mn,c))
96 (map (Tvar . fst) utbs)) ts) tbs
97 ch (tdef@(Newtype c tbs (Just t))) =
98 do tvenv <- foldM extendM eempty tbs
99 k <- checkTy (tcenv,tvenv) t
100 require (k==Klifted) ("bad kind:\n" ++ show tdef)
102 ch (tdef@(Newtype c tbs Nothing)) =
103 {- should only occur for recursive Newtypes -}
107 checkVdefg :: Bool -> (Tcenv,Tsenv,Tvenv,Cenv) -> (Venv,Venv) -> Vdefg -> CheckResult (Venv,Venv)
108 checkVdefg top_level (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg =
111 do e_venv' <- foldM extendM e_venv e_vts
112 l_venv' <- foldM extendM l_venv l_vts
113 let env' = (tcenv,tsenv,tvenv,cenv,e_venv',l_venv')
114 mapM_ (\ (vdef@(Vdef ((m,v),t,e))) ->
115 do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
116 k <- checkTy (tcenv,tvenv) t
117 require (k==Klifted) ("unlifted kind in:\n" ++ show vdef)
118 t' <- checkExp env' e
119 requireM (equalTy tsenv t t')
120 ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
121 "declared type: " ++ show t ++ "\n" ++
122 "expression type: " ++ show t')) vdefs
123 return (e_venv',l_venv')
124 where e_vts = [ (v,t) | Vdef ((m,v),t,_) <- vdefs, m /= "" ]
125 l_vts = [ (v,t) | Vdef (("",v),t,_) <- vdefs]
126 Nonrec (vdef@(Vdef ((m,v),t,e))) ->
127 do require (m == "" || m == mn) ("wrong module name in value definition:\n" ++ show vdef)
128 k <- checkTy (tcenv,tvenv) t
129 require (k /= Kopen) ("open kind in:\n" ++ show vdef)
130 require ((not top_level) || (k /= Kunlifted)) ("top-level unlifted kind in:\n" ++ show vdef)
131 t' <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) e
132 requireM (equalTy tsenv t t')
133 ("declared type doesn't match expression type in:\n" ++ show vdef ++ "\n" ++
134 "declared type: " ++ show t ++ "\n" ++
135 "expression type: " ++ show t')
137 do l_venv' <- extendM l_venv (v,t)
138 return (e_venv,l_venv')
140 do e_venv' <- extendM e_venv (v,t)
141 return (e_venv',l_venv)
143 checkExp :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Exp -> CheckResult Ty
144 checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv) = ch
149 qlookupM venv_ e_venv l_venv qv
151 qlookupM cenv_ cenv eempty qc
156 k' <- checkTy (tcenv,tvenv) t
160 ("kind doesn't match at type application in:\n" ++ show e0 ++ "\n" ++
161 "operator kind: " ++ show k ++ "\n" ++
162 "operand kind: " ++ show k')
163 return (substl [tv] [t] t0)
164 _ -> fail ("bad operator type in type application:\n" ++ show e0 ++ "\n" ++
165 "operator type: " ++ show t')
170 Tapp(Tapp(Tcon tc) t') t0 | tc == tcArrow ->
171 do requireM (equalTy tsenv t2 t')
172 ("type doesn't match at application in:\n" ++ show e0 ++ "\n" ++
173 "operator type: " ++ show t' ++ "\n" ++
174 "operand type: " ++ show t2)
176 _ -> fail ("bad operator type at application in:\n" ++ show e0 ++ "\n" ++
177 "operator type: " ++ show t1)
179 do tvenv' <- extendM tvenv tb
180 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv) e
181 return (Tforall tb t)
182 Lam (Vb (vb@(_,vt))) e ->
183 do k <- checkTy (tcenv,tvenv) vt
185 ("higher-order kind in:\n" ++ show e0 ++ "\n" ++
187 l_venv' <- extendM l_venv vb
188 t <- checkExp (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') e
189 require (not (isUtupleTy vt)) ("lambda-bound unboxed tuple in:\n" ++ show e0)
192 do (e_venv',l_venv') <- checkVdefg False (tcenv,tsenv,tvenv,cenv) (e_venv,l_venv) vdefg
193 checkExp (tcenv,tsenv,tvenv,cenv,e_venv',l_venv') e
196 checkTy (tcenv,tvenv) t
197 requireM (equalTy tsenv t t')
198 ("scrutinee declared type doesn't match expression type in:\n" ++ show e0 ++ "\n" ++
199 "declared type: " ++ show t ++ "\n" ++
200 "expression type: " ++ show t')
201 case (reverse alts) of
203 let ok ((Acon c _ _ _):as) cs = do require (notElem c cs)
204 ("duplicate alternative in case:\n" ++ show e0)
206 ok ((Alit _ _):_) _ = fail ("invalid alternative in constructor case:\n" ++ show e0)
207 ok [Adefault _] _ = return ()
208 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
212 let ok ((Acon _ _ _ _):_) _ = fail ("invalid alternative in literal case:\n" ++ show e0)
213 ok ((Alit l _):as) ls = do require (notElem l ls)
214 ("duplicate alternative in case:\n" ++ show e0)
216 ok [Adefault _] _ = return ()
217 ok (Adefault _:_) _ = fail ("misplaced default alternative in case:\n" ++ show e0)
218 ok [] _ = fail ("missing default alternative in literal case:\n" ++ show e0)
220 [Adefault _] -> return ()
221 [] -> fail ("no alternatives in case:\n" ++ show e0)
222 l_venv' <- extendM l_venv (v,t)
223 t:ts <- mapM (checkAlt (tcenv,tsenv,tvenv,cenv,e_venv,l_venv') t) alts
224 bs <- mapM (equalTy tsenv t) ts
226 ("alternative types don't match in:\n" ++ show e0 ++ "\n" ++
227 "types: " ++ show (t:ts))
231 checkTy (tcenv,tvenv) t
236 do checkTy (tcenv,eempty) t {- external types must be closed -}
239 checkAlt :: (Tcenv,Tsenv,Tvenv,Cenv,Venv,Venv) -> Ty -> Alt -> CheckResult Ty
240 checkAlt (env@(tcenv,tsenv,tvenv,cenv,e_venv,l_venv)) t0 = ch
244 Acon qc etbs vbs e ->
246 where f (Tapp t0 t) = f t0 ++ [t]
248 ct <- qlookupM cenv_ cenv eempty qc
249 let (tbs,ct_args0,ct_res0) = splitTy ct
251 let (utbs,etbs') = splitAt (length uts) tbs
252 let utvs = map fst utbs
253 {- check existentials -}
254 let (etvs,eks) = unzip etbs
255 let (etvs',eks') = unzip etbs'
256 require (eks == eks')
257 ("existential kinds don't match in:\n" ++ show a0 ++ "\n" ++
258 "kinds declared in data constructor: " ++ show eks ++
259 "kinds declared in case alternative: " ++ show eks')
260 tvenv' <- foldM extendM tvenv etbs
261 {- check term variables -}
262 let vts = map snd vbs
263 mapM_ (\vt -> require ((not . isUtupleTy) vt)
264 ("pattern-bound unboxed tuple in:\n" ++ show a0 ++ "\n" ++
265 "pattern type: " ++ show vt)) vts
266 vks <- mapM (checkTy (tcenv,tvenv')) vts
267 mapM_ (\vk -> require (baseKind vk)
268 ("higher-order kind in:\n" ++ show a0 ++ "\n" ++
269 "kind: " ++ show vk)) vks
270 let (ct_res:ct_args) = map (substl (utvs++etvs') (uts++(map Tvar etvs))) (ct_res0:ct_args0)
273 requireM (equalTy tsenv ct_arg vt)
274 ("pattern variable type doesn't match constructor argument type in:\n" ++ show a0 ++ "\n" ++
275 "pattern variable type: " ++ show ct_arg ++ "\n" ++
276 "constructor argument type: " ++ show vt)) ct_args vts
277 requireM (equalTy tsenv ct_res t0)
278 ("pattern constructor type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
279 "pattern constructor type: " ++ show ct_res ++ "\n" ++
280 "scrutinee type: " ++ show t0)
281 l_venv' <- foldM extendM l_venv vbs
282 t <- checkExp (tcenv,tsenv,tvenv',cenv,e_venv,l_venv') e
283 checkTy (tcenv,tvenv) t {- check that existentials don't escape in result type -}
287 requireM (equalTy tsenv t t0)
288 ("pattern type doesn't match scrutinee type in:\n" ++ show a0 ++ "\n" ++
289 "pattern type: " ++ show t ++ "\n" ++
290 "scrutinee type: " ++ show t0)
295 checkTy :: (Tcenv,Tvenv) -> Ty -> CheckResult Kind
296 checkTy (tcenv,tvenv) = ch
298 ch (Tvar tv) = lookupM tvenv tv
299 ch (Tcon qtc) = qlookupM tcenv_ tcenv eempty qtc
300 ch (t@(Tapp t1 t2)) =
305 do require (k2 <= k11)
306 ("kinds don't match in type application: " ++ show t ++ "\n" ++
307 "operator kind: " ++ show k11 ++ "\n" ++
308 "operand kind: " ++ show k2)
310 _ -> fail ("applied type has non-arrow kind: " ++ show t)
312 do tvenv' <- extendM tvenv tb
313 checkTy (tcenv,tvenv') t
315 {- Type equality modulo newtype synonyms. -}
316 equalTy :: Tsenv -> Ty -> Ty -> CheckResult Bool
317 equalTy tsenv t1 t2 =
321 where expand (Tvar v) = return (Tvar v)
322 expand (Tcon qtc) = return (Tcon qtc)
323 expand (Tapp t1 t2) =
326 expand (Tforall tb t) =
328 return (Tforall tb t')
329 expapp (t@(Tcon (m,tc))) ts =
330 do env <- mlookupM tsenv_ tsenv eempty m
331 case elookup env tc of
332 Just (formals,rhs) | (length formals) == (length ts) -> return (substl formals ts rhs)
333 _ -> return (foldl Tapp t ts)
334 expapp (Tapp t1 t2) ts =
339 return (foldl Tapp t' ts)
342 mlookupM :: (Envs -> Env a b) -> Env a b -> Env a b -> Mname -> CheckResult (Env a b)
343 mlookupM selector external_env local_env m =
349 case elookup globalEnv m of
350 Just env' -> return (selector env')
351 Nothing -> fail ("undefined module name: " ++ show m)
353 qlookupM :: (Ord a, Show a) => (Envs -> Env a b) -> Env a b -> Env a b -> (Mname,a) -> CheckResult b
354 qlookupM selector external_env local_env (m,k) =
355 do env <- mlookupM selector external_env local_env m
359 checkLit :: Lit -> CheckResult Ty
363 do {- require (elem t [tIntzh, {- tInt32zh,tInt64zh, -} tWordzh, {- tWord32zh,tWord64zh, -} tAddrzh, tCharzh])
364 ("invalid int literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
367 do {- require (elem t [tFloatzh,tDoublezh])
368 ("invalid rational literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
371 do {- require (t == tCharzh)
372 ("invalid char literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
375 do {- require (t == tAddrzh)
376 ("invalid string literal: " ++ show lit ++ "\n" ++ "type: " ++ show t) -}
381 {- Split off tbs, arguments and result of a (possibly abstracted) arrow type -}
382 splitTy :: Ty -> ([Tbind],[Ty],Ty)
383 splitTy (Tforall tb t) = (tb:tbs,ts,tr)
384 where (tbs,ts,tr) = splitTy t
385 splitTy (Tapp(Tapp(Tcon tc) t0) t) | tc == tcArrow = (tbs,t0:ts,tr)
386 where (tbs,ts,tr) = splitTy t
387 splitTy t = ([],[],t)
390 {- Simultaneous substitution on types for type variables,
391 renaming as neceessary to avoid capture.
392 No checks for correct kindedness. -}
393 substl :: [Tvar] -> [Ty] -> Ty -> Ty
394 substl tvs ts t = f (zip tvs ts) t
399 Tvar v -> case lookup v env of
402 Tapp t1 t2 -> Tapp (f env t1) (f env t2)
404 if t `elem` free then
405 Tforall (t',k) (f ((t,Tvar t'):env) t1)
407 Tforall (t,k) (f (filter ((/=t).fst) env) t1)
408 where free = foldr union [] (map (freeTvars.snd) env)
411 {- Return free tvars in a type -}
412 freeTvars :: Ty -> [Tvar]
413 freeTvars (Tcon _) = []
414 freeTvars (Tvar v) = [v]
415 freeTvars (Tapp t1 t2) = (freeTvars t1) `union` (freeTvars t2)
416 freeTvars (Tforall (t,_) t1) = delete t (freeTvars t1)
418 {- Return any tvar *not* in the argument list. -}
419 freshTvar :: [Tvar] -> Tvar
420 freshTvar tvs = maximum ("":tvs) ++ "x" -- one simple way!