Revert "Support for multiple signature files in scope."
[ghc.git] / docs / core-spec / CoreLint.ott
1 %%
2 %% CoreLint.ott
3 %%
4 %% defines formal version of core typing rules
5 %%
6 %% See accompanying README file
7
8 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
9 %%  Static semantics  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
11
12 defns
13 CoreLint :: '' ::=
14
15 defn |- prog program ::  :: lintCoreBindings :: 'Prog_' {{ com Program typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreBindings} }}
16   {{ tex \labeledjudge{prog} [[program]] }}
17 by
18
19 G = </ vars_of bindingi // i />
20 no_duplicates </ bindingi // i />
21 </ G |-bind bindingi // i />
22 --------------------- :: CoreBindings
23 |-prog </ bindingi // i />
24
25 defn G |- bind binding ::  :: lint_bind :: 'Binding_' {{ com Binding typing, \coderef{coreSyn/CoreLint.lhs}{lint\_bind} }}
26   {{ tex [[G]] \labeledjudge{bind} [[binding]] }}
27 by
28
29 G |-sbind n <- e
30 ---------------------- :: NonRec
31 G |-bind n = e
32
33 </ G |-sbind ni <- ei // i />
34 ---------------------- :: Rec
35 G |-bind rec </ ni = ei // i />
36
37 defn G  |- sbind n <- e ::  :: lintSingleBinding :: 'SBinding_' {{ com Single binding typing, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding} }}
38   {{ tex [[G]] \labeledjudge{sbind} [[n]] [[<-]] [[e]] }}
39 by
40
41 G |-tm e : t
42 G |-name z_t ok
43 </ mi // i /> = fv(t)
44 </ mi elt G // i />
45 ----------------- :: SingleBinding
46 G |-sbind z_t <- e
47
48 defn G  |- tm e : t ::  :: lintCoreExpr :: 'Tm_'
49   {{ com Expression typing, \coderef{coreSyn/CoreLint.lhs}{lintCoreExpr} }}
50   {{ tex [[G]] \labeledjudge{tm} [[e]] : [[t]] }}
51 by
52
53 x_t elt G
54 not (t is_a_coercion)
55 ------------------ :: Var
56 G |-tm x_t : t
57
58 t = literalType lit
59 ------------------- :: Lit
60 G |-tm lit : t
61
62 G |-tm e : s
63 G |-co g : s ~Rep k t
64 ------------------- :: Cast
65 G |-tm e |> g : t
66
67 G |-tm e : t
68 ------------------- :: Tick
69 G |-tm e {tick} : t
70
71 G' = G, alpha_k
72 G |-ki k ok
73 G' |-subst alpha_k |-> s ok
74 G' |-tm e[alpha_k |-> s] : t
75 --------------------------- :: LetTyKi
76 G |-tm let alpha_k = s in e : t
77
78 G |-sbind x_s <- u
79 G |-ty s : k
80 G, x_s |-tm e : t
81 ------------------------- :: LetNonRec
82 G |-tm let x_s = u in e : t
83
84 </ G'i @ // i /> = inits(</ zi_si // i />)
85 </ G, G'i |-ty si : ki // i />
86 no_duplicates </ zi // i />
87 G' = G, </ zi_si // i />
88 </ G' |-sbind zi_si <- ui // i />
89 G' |-tm e : t
90 ------------------------ :: LetRec
91 G |-tm let rec </ zi_si = ui // i /> in e : t
92
93 % lintCoreArg is incorporated in these next two rules
94
95 G |-tm e1 : forall alpha_k.t
96 G |-subst alpha_k |-> s ok
97 ---------------- :: AppType
98 G |-tm e1 s : t[alpha_k |-> s]
99
100 not (e2 is_a_type)
101 G |-tm e1 : t1 -> t2
102 G |-tm e2 : t1
103 ---------------- :: AppExpr
104 G |-tm e1 e2 : t2
105
106 G |-ty t : k
107 G, x_t |-tm e : s
108 ----------------- :: LamId
109 G |-tm \x_t.e : t -> s
110
111 G' = G, alpha_k
112 G |-ki k ok
113 G' |-tm e : t
114 --------------------------- :: LamTy
115 G |-tm \alpha_k.e : forall alpha_k. t
116
117 G |-tm e : s
118 G |-ty s : k1
119 G |-ty t : k2
120 </ G, z_s; s |-altern alti : t // i />
121 ---------------------------------------------------- :: Case
122 G |-tm case e as z_s return t of </ alti // i /> : t
123
124 G |-co g : t1 ~Nom k t2
125 -------------------- :: CoercionNom
126 G |-tm g : t1 ~#k t2
127
128 G |-co g : t1 ~Rep k t2
129 ----------------------- :: CoercionRep
130 G |-tm g : (~R#) k t1 t2
131
132 defn G  |- name n ok ::  :: lintSingleBinding_lintBinder :: 'Name_'
133   {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }}
134   {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }}
135 by
136
137 G |-ty t : k
138 ----------------- :: Id
139 G |-name x_t ok
140
141 ----------------- :: TyVar
142 G |-name alpha_k ok
143
144 defn G |- bnd n ok ::  :: lintBinder :: 'Binding_'
145   {{ com Binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintBinder} }}
146   {{ tex [[G]] \labeledjudge{bnd} [[n]] [[ok]] }}
147 by
148
149 G |-ty t : k
150 --------------------------------- :: Id
151 G |-bnd x_t ok
152
153 G |-ki k ok
154 ---------------------------------------- :: TyVar
155 G |-bnd alpha_k ok
156
157 defn G  |- co g : t1 ~ R k t2 ::  :: lintCoercion :: 'Co_'
158   {{ com Coercion typing, \coderef{coreSyn/CoreLint.lhs}{lintCoercion} }}
159   {{ tex [[G]] \labeledjudge{co} [[g]] : [[t1]] \mathop{\sim_{[[R]]}^{[[k]]} } [[t2]] }}
160 by
161
162 G |-ty t : k
163 ---------------------- :: Refl
164 G |-co <t>_R : t ~R k t
165
166 G |-co g1 : s1 ~R k1 t1
167 G |-co g2 : s2 ~R k2 t2
168 G |-arrow k1 -> k2 : k
169 ------------------------- :: TyConAppCoFunTy
170 G |-co (->)_R g1 g2 : (s1 -> s2) ~R k (t1 -> t2)
171
172 T /= (->)
173 </ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
174 </ G |-co gi : si ~Ri ki ti // i />
175 G |-app </ (si : ki) // i /> : tyConKind T ~> k
176 --------------------------------- :: TyConAppCo
177 G |-co T_R </ gi // i /> : T </ si // i />  ~R k T </ ti // i />
178
179 G |-co g1 : s1 ~R k1 t1
180 G |-co g2 : s2 ~Nom k2 t2
181 G |-app (s2 : k2) : k1 ~> k
182 --------------------- :: AppCo
183 G |-co g1 g2 : (s1 s2) ~R k (t1 t2)
184
185 G |-co g1 : s1 ~Ph k1 t1
186 G |-co g2 : s2 ~Ph k2 t2
187 G |-app (s2 : k2) : k1 ~> k
188 --------------------- :: AppCoPhantom
189 G |-co g1 g2 : (s1 s2) ~Ph k (t1 t2)
190
191 G |-ki k1 ok
192 G, z_k1 |-co g : s ~R k2 t
193 --------------------------- :: ForAllCo
194 G |-co forall z_k1. g : (forall z_k1.s) ~R k2 (forall z_k1.t)
195
196 z_(t ~#BOX t) elt G
197 ----------------------- :: CoVarCoBox
198 G |-co z_(t ~#BOX t) : t ~Nom BOX t
199
200 z_(s ~#k t) elt G
201 k /= BOX
202 ----------------------- :: CoVarCoNom
203 G |-co z_(s ~#k t) : s ~Nom k t
204
205 z_(s ~R#k t) elt G
206 k /= BOX
207 ----------------------- :: CoVarCoRepr
208 G |-co z_(s ~R#k t) : s ~Rep k t
209
210 G |-ty t1 : k1
211 G |-ty t2 : k2
212 R <= Ph \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2
213 ------------------------------------------------------------------------ :: UnivCo
214 G |-co t1 ==>!_R t2 : t1 ~R k2 t2
215
216 G |-co g : t1 ~R k t2
217 ------------------------- :: SymCo
218 G |-co sym g : t2 ~R k t1
219
220 G |-co g1 : t1 ~R k t2
221 G |-co g2 : t2 ~R k t3
222 ----------------------- :: TransCo
223 G |-co g1 ; g2 : t1 ~R k t3
224
225 G |-co g : (T </ sj // j />) ~R k (T </ tj // j />)
226 length </ sj // j /> = length </ tj // j />
227 i < length </ sj // j />
228 G |-ty si : k
229 R' = (tyConRolesX R T)[i]
230 ---------------------- :: NthCo
231 G |-co nth i g : si ~R' k ti
232
233 G |-co g : (s1 s2) ~Nom k' (t1 t2)
234 G |-ty s1 : k
235 ----------------------- :: LRCoLeft
236 G |-co Left g : s1 ~Nom k t1
237
238 G |-co g : (s1 s2) ~Nom k' (t1 t2)
239 G |-ty s2 : k
240 ----------------------- :: LRCoRight
241 G |-co Right g : s2 ~Nom k t2
242
243 G |-co g : forall m.s ~R k forall n.t
244 G |-ty t0 : k0
245 m = z_k1
246 k0 <: k1
247 --------------------- :: InstCo
248 G |-co g t0 : s[m |-> t0] ~R k t[n |-> t0]
249
250 C = T_R0 </ axBranchkk // kk />
251 0 <= ind < length </ axBranchkk // kk />
252 forall </ ni_^^Ri // i />. (</ s1j // j /> ~> t1) = (</ axBranchkk // kk />)[ind]
253 </ G |-co gi : s'i ~Ri k'i t'i // i />
254 </ substi @ // i /> = inits(</ [ ni |-> s'i ] // i />)
255 </ ni = zi_ki // i />
256 </ k'i <: substi(ki) // i />
257 no_conflict(C, </ s2j // j />, ind, ind-1)
258 </ s2j = s1j </ [ni |-> s'i] // i/> // j />
259 t2 = t1 </ [ni |-> t'i] // i />
260 G |-ty t2 : k
261 ------------------------------------------------------ :: AxiomInstCo
262 G |-co C ind </ gi // i /> : T </ s2j // j /> ~R0 k t2
263
264 G |-co g : s ~Nom k t
265 ------------------------- :: SubCo
266 G |-co sub g : s ~Rep k t
267
268 mu = M(i, </ Rj // j />, R')
269 </ G |-ty ti : ki // i />
270 </ G |-co gj : sj ~Rj k'j s'j // j />
271 Just (t'1, t'2) = coaxrProves mu </ ti // i /> </ (sj, s'j) // j />
272 G |-ty t'1 : k0
273 G |-ty t'2 : k0
274 --------------------------------------------------------------------- :: AxiomRuleCo
275 G |-co mu </ ti // i /> </ gj // j /> : t'1 ~R' k0 t'2
276
277 defn validRoles T ::  :: checkValidRoles :: 'Cvr_'
278   {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }}
279 by
280
281 </ Ki // i /> = tyConDataCons T
282 </ Rj // j /> = tyConRoles T
283 </ validDcRoles </ Rj // j /> Ki // i />
284 ------------------------------------ :: DataCons
285 validRoles T
286
287 defn validDcRoles </ Raa // aa /> K :: :: check_dc_roles :: 'Cdr_'
288   {{ com Data constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_dc\_roles} }}
289 by
290
291 forall </ naa // aa />. forall </ mbb // bb />. </ tcc // cc /> @ -> T </ naa // aa /> = dataConRepType K
292 </ </ naa : Raa // aa />, </ mbb : Nom // bb /> |- tcc : Rep // cc />
293 --------------------------------- :: Args
294 validDcRoles </ Raa // aa /> K
295
296 defn O |- t : R  ::   :: check_ty_roles :: 'Ctr_'
297   {{ com Type role validity, \coderef{typecheck/TcTyClsDecls.lhs}{check\_ty\_roles} }}
298   {{ tex [[O]] \labeledjudge{ctr} [[t]] : [[R]] }}
299 by
300
301 O(n) = R'
302 R' <= R
303 ---------- :: TyVarTy
304 O |- n : R
305
306 </ Ri // i /> = tyConRoles T
307 </ Ri elt { Nom, Rep } => O |- ti : Ri // i />
308 -------------------------- :: TyConAppRep
309 O |- T </ ti // i /> : Rep
310
311 </ O |- ti : Nom // i />
312 --------------------------- :: TyConAppNom
313 O |- T </ ti // i /> : Nom
314
315 O |- t1 : R
316 O |- t2 : Nom
317 -------------------------- :: AppTy
318 O |- t1 t2 : R
319
320 O |- t1 : R
321 O |- t2 : R
322 ------------------- :: FunTy
323 O |- t1 -> t2 : R
324
325 O, n : Nom |- t : R
326 --------------------- :: ForAllTy
327 O |- forall n. t : R
328
329 ------------------ :: LitTy
330 O |- lit : R
331
332 defn R1 <= R2 ::  :: ltRole :: 'Rlt_'
333   {{ com Sub-role relation, \coderef{types/Coercion.lhs}{ltRole} }}
334   {{ tex [[R1]] \leq [[R2]] }}
335 by
336
337 -------- :: Nominal
338 Nom <= R
339
340 -------- :: Phantom
341 R <= Ph
342
343 ------- :: Refl
344 R <= R
345
346 defn G |- ki k ok ::  :: lintKind :: 'K_'
347   {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }}
348   {{ tex [[G]] \labeledjudge{k} [[k]] [[ok]] }}
349 by
350
351 G |-ty k : BOX
352 -------------- :: Box
353 G |-ki k ok
354
355 defn G |- ty t : k ::  :: lintType :: 'Ty_'
356   {{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }}
357   {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }}
358 by
359
360 z_k elt G
361 ------------ :: TyVarTy
362 G |-ty z_k : k
363
364 G |-ty t1 : k1
365 G |-ty t2 : k2
366 G |-app (t2 : k2) : k1 ~> k
367 --------------- :: AppTy
368 G |-ty t1 t2 : k
369
370 G |-ty t1 : k1
371 G |-ty t2 : k2
372 G |-arrow k1 -> k2 : k
373 ------------------- :: FunTy
374 G |-ty t1 -> t2 : k
375
376 not (isUnLiftedTyCon T) \/ length </ ti // i /> = tyConArity T
377 </ G |-ty ti : ki // i />
378 G |-app </ (ti : ki) // i /> : tyConKind T ~> k
379 --------------------------- :: TyConApp
380 G |-ty T </ ti // i /> : k
381
382 G |-ki k1 ok
383 G, z_k1 |-ty t : k2
384 ------------------------ :: ForAllTy
385 G |-ty forall z_k1. t : k2
386
387 G |-tylit lit : k
388 -------------- :: LitTy
389 G |-ty lit : k
390
391 defn G |- subst n |-> t ok ::  :: checkTyKind :: 'Subst_'
392   {{ com Substitution consistency, \coderef{coreSyn/CoreLint.lhs}{checkTyKind} }}
393   {{ tex [[G]] \labeledjudge{subst} [[n]] [[|->]] [[t]] [[ok]] }}
394 by
395
396 G |-ki k ok
397 ------------------------ :: Kind
398 G |-subst z_BOX |-> k ok
399
400 k1 /= BOX
401 G |-ty t : k2
402 k2 <: k1
403 ---------------------- :: Type
404 G |-subst z_k1 |-> t ok
405
406 defn G ; s |- altern alt : t ::  :: lintCoreAlt :: 'Alt_'
407   {{ com Case alternative consistency, \coderef{coreSyn/CoreLint.lhs}{lintCoreAlt} }}
408   {{ tex [[G]];[[s]] \labeledjudge{alt} [[alt]] : [[t]] }}
409 by
410
411 G |-tm e : t
412 --------------------- :: DEFAULT
413 G; s |-altern _ -> e : t
414
415 s = literalType lit
416 G |-tm e : t
417 ---------------------------------------- :: LitAlt
418 G; s |-altern lit -> e : t
419
420 T = dataConTyCon K
421 not (isNewTyCon T)
422 t1 = dataConRepType K
423 t2 = t1 {</ sj // j />}
424 </ G |-bnd ni ok // i />
425 G' = G, </ ni // i />
426 G' |-altbnd </ ni // i /> : t2 ~> T </ sj // j />
427 G' |-tm e : t
428 --------------------------------------- :: DataAlt
429 G; T </ sj // j /> |-altern K </ ni // i /> -> e : t
430
431 defn t' = t { </ si // , // i /> } ::  :: applyTys :: 'ApplyTys_'
432   {{ com Telescope substitution, \coderef{types/Type.lhs}{applyTys} }}
433 by
434
435 --------------------- :: Empty
436 t = t { }
437
438 t' = t{</ si // i />}
439 t'' = t'[n |-> s]
440 -------------------------- :: Ty
441 t'' = (forall n. t) { s, </ si // i /> }
442
443 defn G |- altbnd vars : t1 ~> t2 ::  :: lintAltBinders :: 'AltBinders_'
444   {{ com Case alternative binding consistency, \coderef{coreSyn/CoreLint.lhs}{lintAltBinders} }}
445   {{ tex [[G]] \labeledjudge{altbnd} [[vars]] : [[t1]] [[~>]] [[t2]] }}
446 by
447
448 ------------------------- :: Empty
449 G |-altbnd empty : t ~> t
450
451 G |-subst beta_k' |-> alpha_k ok
452 G |-altbnd </ ni // i /> : t[beta_k' |-> alpha_k] ~> s
453 ------------------------------------------------------ :: TyVar
454 G |-altbnd alpha_k, </ ni // i /> : (forall beta_k'.t) ~> s
455
456 G |-altbnd </ ni // i /> : t2 ~> s
457 ----------------------------------------------- :: Id
458 G |-altbnd x_t1, </ ni // i /> : (t1 -> t2) ~> s
459
460 defn G |- arrow k1 -> k2 : k ::  :: lintArrow :: 'Arrow_'
461   {{ com Arrow kinding, \coderef{coreSyn/CoreLint.lhs}{lintArrow} }}
462   {{ tex [[G]] \labeledjudge{\rightarrow} [[k1]] [[->]] [[k2]] : [[k]] }}
463 by
464
465 ------------------------- :: Box
466 G |-arrow BOX -> k2 : BOX
467
468 k1 elt { *, #, Constraint }
469 k2 elt { *, #, Constraint }
470 ------------------------- :: Kind
471 G |-arrow k1 -> k2 : *
472
473 defn G |- app kinded_types : k1 ~> k2 ::  :: lint_app :: 'App_'
474   {{ com Type application kinding, \coderef{coreSyn/CoreLint.lhs}{lint\_app} }}
475   {{ tex [[G]] \labeledjudge{app} [[kinded_types]] : [[k1]] [[~>]] [[k2]] }}
476 by
477
478 --------------------- :: Empty
479 G |-app empty : k ~> k
480
481 k <: k1
482 G |-app </ (ti : ki) // i /> : k2 ~> k'
483 ---------------------------------------------------- :: FunTy
484 G |-app (t : k), </ (ti : ki) // i /> : (k1 -> k2) ~> k'
485
486 k <: k1
487 G |-app </ (ti : ki) // i /> : k2[z_k1 |-> t] ~> k'
488 -------------------------------------------------------- :: ForAllTy
489 G |-app (t : k), </ (ti : ki) // i /> : (forall z_k1. k2) ~> k'
490
491 defn k1 <: k2 ::  :: isSubKind :: 'SubKind_'
492   {{ com Sub-kinding, \coderef{types/Kind.lhs}{isSubKind} }}
493 by
494
495 ------ :: Refl
496 k <: k
497
498 -------------------- :: UnliftedTypeKind
499 # <: OpenKind
500
501 ------------------- :: LiftedTypeKind
502 * <: OpenKind
503
504 ---------------------- :: Constraint
505 Constraint <: OpenKind
506
507 ------------------- :: ConstraintLifted
508 Constraint <: *
509
510 ------------------ :: LiftedConstraint
511 * <: Constraint
512
513 defn no_conflict ( C , </ sj // j /> , ind1 , ind2 ) ::  :: check_no_conflict :: 'NoConflict_'
514   {{ com \parbox{5in}{Branched axiom conflict checking, \coderef{types/OptCoercion.lhs}{checkAxInstCo} \\ and \coderef{types/FamInstEnv.lhs}{compatibleBranches} } }}
515 by
516
517 ------------------------------------------------ :: NoBranch
518 no_conflict(C, </ si // i/>, ind, -1)
519
520 C = T_R </ axBranchkk // kk />
521 forall </ ni_Ri // i />. (</ tj // j /> ~> t') = (</ axBranchkk // kk />)[ind2]
522 apart(</ sj // j />, </ tj // j />)
523 no_conflict(C, </ sj // j />, ind1, ind2-1)
524 ------------------------------------------------ :: Incompat
525 no_conflict(C, </ sj // j />, ind1, ind2)
526
527 C = T_R </ axBranchkk // kk />
528 forall </ ni_Ri // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
529 forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
530 apart(</ tj // j />, </ t'j // j />)
531 no_conflict(C, </ sj // j />, ind1, ind2-1)
532 ------------------------------------------- :: CompatApart
533 no_conflict(C, </ sj // j />, ind1, ind2)
534
535 C = T_R </ axBranchkk // kk />
536 forall </ ni_Ri // i />. (</ tj // j /> ~> s) = (</ axBranchkk // kk />)[ind1]
537 forall </ n'i_R'i // i />. (</ t'j // j /> ~> s') = (</ axBranchkk // kk />)[ind2]
538 unify(</ tj // j />, </ t'j // j />) = subst
539 subst(s) = subst(s')
540 ----------------------------------------- :: CompatCoincident
541 no_conflict(C, </ sj // j />, ind1, ind2)