Zonk the existential type variables in tcPatSynDecl
[ghc.git] / docs / core-spec / core-spec.mng
1 \documentclass{article}
2
3 \usepackage{supertabular}
4 \usepackage{amsmath}
5 \usepackage{amssymb}
6 \usepackage{stmaryrd}
7 \usepackage{xcolor}
8 \usepackage{fullpage}
9 \usepackage{multirow}
10 \usepackage{url}
11
12 \newcommand{\ghcfile}[1]{\textsl{#1}}
13 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
14
15 \input{CoreOtt}
16
17 % increase spacing between rules for ease of reading:
18 \renewcommand{\ottusedrule}[1]{\[#1\]\\[1ex]}
19
20 \setlength{\parindent}{0in}
21 \setlength{\parskip}{1ex}
22
23 \newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
24
25 \begin{document}
26
27 \begin{center}
28 \LARGE
29 System FC, as implemented in GHC\footnote{This
30 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
31 but it should be maintained by anyone who edits the functions or data structures
32 mentioned in this file. Please feel free to contact Richard for more information.}\\
33 \Large 21 November, 2013
34 \end{center}
35
36 \section{Introduction}
37
38 This document presents the typing system of System FC, very closely to how it is
39 implemented in GHC. Care is taken to include only those checks that are actually
40 written in the GHC code. It should be maintained along with any changes to this
41 type system.
42
43 Who will use this? Any implementer of GHC who wants to understand more about the
44 type system can look here to see the relationships among constructors and the
45 different types used in the implementation of the type system. Note that the
46 type system here is quite different from that of Haskell---these are the details
47 of the internal language, only.
48
49 At the end of this document is a \emph{hypothetical} operational semantics for GHC.
50 It is hypothetical because GHC does not strictly implement a concrete operational
51 semantics anywhere in its code. While all the typing rules can be traced back to
52 lines of real code, the operational semantics do not, in general, have as clear
53 a provenance.
54
55 There are a number of details elided from this presentation. The goal of the
56 formalism is to aid in reasoning about type safety, and checks that do not
57 work toward this goal were omitted. For example, various scoping checks (other
58 than basic context inclusion) appear in the GHC code but not here.
59
60 \section{Grammar}
61
62 \subsection{Metavariables}
63
64 We will use the following metavariables:
65
66 \ottmetavars{}\\
67
68 \subsection{Literals}
69
70 Literals do not play a major role, so we leave them abstract:
71
72 \gram{\ottlit}
73
74 We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType}
75 and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
76
77 \subsection{Variables}
78 \enlargethispage{10pt} % without this first line of "z" definition is placed on
79                        % second page and it becomes the only line of text on that
80                        % page, resulting in whole page being empty.
81 GHC uses the same datatype to represent term-level variables and type-level
82 variables:
83
84 \gram{
85 \ottz
86 }
87
88 \gram{
89 \ottn
90 }
91
92 \subsection{Expressions}
93
94 The datatype that represents expressions:
95
96 \gram{\otte}
97
98 There are a few key invariants about expressions:
99 \begin{itemize}
100 \item The right-hand sides of all top-level and recursive $[[let]]$s
101 must be of lifted type.
102 \item The right-hand side of a non-recursive $[[let]]$ and the argument
103 of an application may be of unlifted type, but only if the expression
104 is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.lhs}.
105 \item We allow a non-recursive $[[let]]$ for bind a type variable.
106 \item The $[[_]]$ case for a $[[case]]$ must come first.
107 \item The list of case alternatives must be exhaustive.
108 \item Types and coercions can only appear on the right-hand-side of an application.
109 \end{itemize}
110
111 Bindings for $[[let]]$ statements:
112
113 \gram{\ottbinding}
114
115 Case alternatives:
116
117 \gram{\ottalt}
118
119 Constructors as used in patterns:
120
121 \gram{\ottKp}
122
123 Notes that can be inserted into the AST. We leave these abstract:
124
125 \gram{\otttick}
126
127 A program is just a list of bindings:
128
129 \gram{\ottprogram}
130
131 \subsection{Types}
132
133 \gram{\ottt}
134
135 There are some invariants on types:
136 \begin{itemize}
137 \item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
138 $[[T]]$. It should be another application or a type variable.
139 \item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp}) 
140 does \emph{not} need to be saturated.
141 \item A saturated application of $[[(->) t1 t2]]$ should be represented as 
142 $[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
143 The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
144 \item A type-level literal is represented in GHC with a different datatype than
145 a term-level literal, but we are ignoring this distinction here.
146 \end{itemize}
147
148 \subsection{Coercions}
149
150 \gram{\ottg}
151
152 Invariants on coercions:
153 \begin{itemize}
154 \item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
155 \item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
156 reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
157 \item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
158 be a type function.
159 \end{itemize}
160
161 Roles label what equality relation a coercion is a witness of. Nominal equality
162 means that two types are identical (have the same name); representational equality
163 means that two types have the same representation (introduced by newtypes); and
164 phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles}
165 for more background.
166
167 \gram{\ottR}
168
169 Is it a left projection or a right projection?
170
171 \gram{\ottLorR}
172
173 Axioms:
174
175 \gram{
176 \ottC\ottinterrule
177 \ottaxBranch
178 }
179
180 The definition for $[[axBranch]]$ above does not include the list of
181 incompatible branches (field \texttt{cab\_incomps} of \texttt{CoAxBranch}),
182 as that would unduly clutter this presentation. Instead, as the list
183 of incompatible branches can be computed at any time, it is checked for
184 in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
185
186 Axiom rules, produced by the type-nats solver:
187
188 \gram{\ottmu}
189
190 \label{sec:axiom_rules}
191 An axiom rule $[[mu]] = [[M(I, role_list, R')]]$ is an axiom name $[[M]]$, with a
192 type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
193 and an output role $[[R']]$. The definition within GHC also includes a field named
194 $[[coaxrProves]]$ which computes the output coercion from a list of types and
195 a list of coercions. This is elided in this presentation, as we simply identify
196 axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
197 and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
198
199 \subsection{Type constructors}
200
201 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
202 for this formalism:
203
204 \gram{\ottT}
205
206 We include some representative primitive type constructors. There are many more in \ghcfile{prelude/TysPrim.lhs}.
207
208 \gram{\ottH}
209
210 \section{Contexts}
211
212 The functions in \ghcfile{coreSyn/CoreLint.lhs} use the \texttt{LintM} monad.
213 This monad contains a context with a set of bound variables $[[G]]$. The
214 formalism treats $[[G]]$ as an ordered list, but GHC uses a set as its
215 representation.
216
217 \gram{
218 \ottG
219 }
220
221 We assume the Barendregt variable convention that all new variables are
222 fresh in the context. In the implementation, of course, some work is done
223 to guarantee this freshness. In particular, adding a new type variable to
224 the context sometimes requires creating a new, fresh variable name and then
225 applying a substitution. We elide these details in this formalism, but
226 see \coderef{types/Type.lhs}{substTyVarBndr} for details.
227
228 \section{Typing judgments}
229
230 The following functions are used from GHC. Their names are descriptive, and they
231 are not formalized here: \coderef{types/TyCon.lhs}{tyConKind},
232 \coderef{types/TyCon.lhs}{tyConArity}, \coderef{basicTypes/DataCon.lhs}{dataConTyCon}, \coderef{types/TyCon.lhs}{isNewTyCon}, \coderef{basicTypes/DataCon.lhs}{dataConRepType}.
233
234 \subsection{Program consistency}
235
236 Check the entire bindings list in a context including the whole list. We extract
237 the actual variables (with their types/kinds) from the bindings, check for duplicates,
238 and then check each binding.
239
240 \ottdefnlintCoreBindings{}
241
242 Here is the definition of $[[vars_of]]$, taken from \coderef{coreSyn/CoreSyn.lhs}{bindersOf}:
243
244 \[
245 \begin{array}{ll}
246 [[vars_of n = e]] &= [[n]] \\
247 [[vars_of rec </ ni = ei // i />]] &= [[</ ni // i />]]
248 \end{array}
249 \]
250
251 \subsection{Binding consistency}
252
253 \ottdefnlintXXbind{}
254
255 \ottdefnlintSingleBinding{}
256
257 In the GHC source, this function contains a number of other checks, such
258 as for strictness and exportability. See the source code for further information.
259
260 \subsection{Expression typing}
261
262 \ottdefnlintCoreExpr{}
263
264 \begin{itemize}
265 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
266 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
267 to check each substituted type $[[s'i]]$ in a context containing all the types
268 that come before it in the list of bindings. The $[[G'i]]$ are contexts
269 containing the names and kinds of all type variables (and term variables,
270 for that matter) up to the $i$th binding. This logic is extracted from
271 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
272
273 \item There is one more case for $[[G |-tm e : t]]$, for type expressions.
274 This is included in the GHC code but is elided
275 here because the case is never used in practice. Type expressions
276 can only appear in arguments to functions, and these are handled
277 in \ottdrulename{Tm\_AppType}.
278
279 \item The GHC source code checks all arguments in an application expression
280 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
281 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
282 has been unfolded for presentation here.
283
284 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
285 (scoping) checks.
286
287 \item The rule for $[[case]]$ statements also checks to make sure that
288 the alternatives in the $[[case]]$ are well-formed with respect to the
289 invariants listed above. These invariants do not affect the type or
290 evaluation of the expression, so the check is omitted here.
291
292 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
293 a dead id and for one-tuples. These checks are omitted here.
294 \end{itemize}
295
296 \subsection{Kinding}
297
298 \ottdefnlintType{}
299
300 \subsection{Kind validity}
301
302 \ottdefnlintKind{}
303
304 \subsection{Coercion typing}
305
306 In the coercion typing judgment, the $\#$ marks are left off the equality
307 operators to reduce clutter. This is not actually inconsistent, because
308 the GHC function that implements this check, \texttt{lintCoercion}, actually
309 returns four separate values (the kind, the two types, and the role), not
310 a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
311 these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
312 and \ottdrulename{Co\_CoVarCoRepr}.
313
314 \ottdefnlintCoercion{}
315
316 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
317 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
318 folding the substitution over the kinds for kind-checking.
319
320 See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
321 see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
322
323 \subsection{Name consistency}
324
325 There are two very similar checks for names, one declared as a local function:
326
327 \ottdefnlintSingleBindingXXlintBinder{}
328
329 \ottdefnlintBinder{}
330
331 \subsection{Substitution consistency}
332
333 \ottdefncheckTyKind{}
334
335 \subsection{Case alternative consistency}
336
337 \ottdefnlintCoreAlt{}
338
339 \subsection{Telescope substitution}
340
341 \ottdefnapplyTys{}
342
343 \subsection{Case alternative binding consistency}
344
345 \ottdefnlintAltBinders{}
346
347 \subsection{Arrow kinding}
348
349 \ottdefnlintArrow{}
350
351 \subsection{Type application kinding}
352
353 \ottdefnlintXXapp{}
354
355 \subsection{Sub-kinding}
356
357 \ottdefnisSubKind{}
358
359 \subsection{Roles}
360 \label{sec:tyconroles}
361
362 During type-checking, role inference is carried out, assigning roles to the
363 arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
364 roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
365 $[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
366 for potential oversaturation.
367
368 The checks encoded in the following
369 judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
370 when \texttt{-dcore-lint} is set.
371
372 \ottdefncheckValidRoles{}
373
374 \ottdefncheckXXdcXXroles{}
375
376 In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
377 The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
378
379 \gram{\ottO}
380
381 \ottdefncheckXXtyXXroles{}
382
383 These judgments depend on a sub-role relation:
384
385 \ottdefnltRole{}
386
387 \subsection{Branched axiom conflict checking}
388 \label{sec:no_conflict}
389
390 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
391 sure that a type family application cannot unify with any previous branch
392 in the axiom. The actual code scans through only those branches that are
393 flagged as incompatible. These branches are stored directly in the
394 $[[axBranch]]$. However, it is cleaner in this presentation to simply
395 check for compatibility here.
396
397 \ottdefncheckXXnoXXconflict{}
398
399 The judgment $[[apart]]$ checks to see whether two lists of types are surely
400 apart. $[[apart( </ ti // i />, </ si // i /> )]]$, where $[[ </ ti // i />
401 ]]$ is a list of types and $[[ </ si // i /> ]]$ is a list of type
402 \emph{patterns} (as in a type family equation), first flattens the $[[ </ ti
403     // i /> ]]$ using \coderef{types/FamInstEnv.lhs}{flattenTys} and then checks to
404 see if \coderef{types/Unify.lhs}{tcUnifyTysFG} returns \texttt{SurelyApart}.
405 Flattening takes all type family applications and replaces them with fresh variables,
406 taking care to map identical type family applications to the same fresh variable.
407
408 The algorithm $[[unify]]$ is implemented in \coderef{types/Unify.lhs}{tcUnifyTys}.
409 It performs a standard unification, returning a substitution upon success.
410
411 \section{Operational semantics}
412
413 \subsection{Disclaimer}
414 GHC does not implement an operational semantics in any concrete form. Most
415 of the rules below are implied by algorithms in, for example, the simplifier
416 and optimizer. Yet, there is no one place in GHC that states these rules,
417 analogously to \texttt{CoreLint.lhs}.
418 Nevertheless, these rules are included in this document to help the reader
419 understand System FC.
420
421 \subsection{The context $[[S]]$}
422 We use a context $[[S]]$ to keep track of the values of variables in a (mutually)
423 recursive group. Its definition is as follows:
424 \[
425 [[S]] \quad ::= \quad [[ empty ]] \ |\ [[S]], [[ [n |-> e] ]]
426 \]
427 The presence of the context $[[S]]$ is solely to deal with recursion. If your
428 use of FC does not require modeling recursion, you will not need to track $[[S]]$.
429
430 \subsection{Operational semantics rules}
431
432 \ottdefnstep{}
433
434 \subsection{Notes}
435
436 \begin{itemize}
437 \item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
438 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
439 for all of the mutually recursive equations. Then, after perhaps many steps,
440 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
441 in the $[[let]]\ [[rec]]$, the context is popped.
442 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
443 lists of arguments: two lists of types and a list of terms. The types passed
444 in are the universally and, respectively, existentially quantified type variables
445 to the constructor. The terms are the regular term arguments stored in an
446 algebraic datatype. Coercions (say, in a GADT) are considered term arguments.
447 \item The rule \ottdrulename{S\_CasePush} is the most complex rule.
448 \begin{itemize}
449 \item The logic in this rule is implemented in \coderef{coreSyn/CoreSubst.lhs}{exprIsConApp\_maybe}.
450 \item The $[[coercionKind]]$ function (\coderef{types/Coercion.lhs}{coercionKind})
451 extracts the two types (and their kind) from
452 a coercion. It does not require a typing context, as it does not \emph{check} the
453 coercion, just extracts its types.
454 \item The $[[dataConRepType]]$ function (\coderef{basicTypes/DataCon.lhs}{dataConRepType}) extracts the full type of a data constructor. Following the notation for
455 constructor expressions, the parameters to the constructor are broken into three
456 groups: universally quantified types, existentially quantified types, and terms.
457 \item The substitutions in the last premise to the rule are unusual: they replace
458 \emph{type} variables with \emph{coercions}. This substitution is called lifting
459 and is implemented in \coderef{types/Coercion.lhs}{liftCoSubst}. The notation is
460 essentially a pun on the fact that types and coercions have such similar structure.
461 \item Note that the types $[[ </ sbb // bb /> ]]$---the existentially quantified
462 types---do not change during this step.
463 \end{itemize}
464 \end{itemize}
465
466 \end{document}