1 \documentclass{article}
3 \usepackage{supertabular}
4 \usepackage{amsmath}
5 \usepackage{amssymb}
6 \usepackage{stmaryrd}
7 \usepackage{xcolor}
8 \usepackage{fullpage}
9 \usepackage{multirow}
11 \newcommand{\ghcfile}[1]{\textsl{#1}}
12 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
14 \input{CoreOtt}
16 % increase spacing between rules for ease of reading:
205 \subsection{Binding consistency}
207 \ottdefnlintXXbind{}
209 \ottdefnlintSingleBinding{}
211 In the GHC source, this function contains a number of other checks, such
212 as for strictness and exportability. See the source code for further information.
214 \subsection{Expression typing}
216 \ottdefnlintCoreExpr{}
218 %\arraylabel{\coderef{coreSyn/CoreLint.lhs}{checkCaseAlts}} \\
219 %\multicolumn{2}{l}{[[checkCaseAlts]] \text{ checks ordering and exhaustivity constr%aints}} \\
221 %\end{array}
222 %\]
224 \begin{itemize}
225 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
226 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
227 to check each substituted type $[[s'i]]$ in a context containing all the types
228 that come before it in the list of bindings. The $[[G'i]]$ are contexts
229 containing the names and kinds of all type variables (and term variables,
230 for that matter) up to the $i$th binding. This logic is extracted from
231 \coderef{coreSyn/CoreLint.lhs}{lintAndScopeIds}.
233 \item There is one more case for $[[G |-tm e : t]]$, for type expressions.
234 This is included in the GHC code but is elided
235 here because the case is never used in practice. Type expressions
236 can only appear in arguments to functions, and these are handled
237 in \ottdrulename{Tm\_AppType}.
239 \item The GHC source code checks all arguments in an application expression
240 all at once using \coderef{coreSyn/CoreSyn.lhs}{collectArgs}
241 and \coderef{coreSyn/CoreLint.lhs}{lintCoreArgs}. The operation
242 has been unfolded for presentation here.
244 \item If a $[[tick]]$ contains breakpoints, the GHC source performs additional
245 (scoping) checks.
247 \item The rule for $[[case]]$ statements also checks to make sure that
248 the alternatives in the $[[case]]$ are well-formed with respect to the
249 invariants listed above. These invariants do not affect the type or
250 evaluation of the expression, so the check is omitted here.
252 \item The GHC source code for \ottdrulename{Tm\_Var} contains checks for
253 a dead id and for one-tuples. These checks are omitted here.
254 \end{itemize}
256 \subsection{Kinding}
258 \ottdefnlintType{}
260 \subsection{Kind validity}
262 \ottdefnlintKind{}
264 \subsection{Coercion typing}
266 \ottdefnlintCoercion{}
268 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
269 the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of
270 folding the substitution over the kinds for kind-checking.
272 \subsection{Name consistency}
274 There are two very similar checks for names, one declared as a local function:
276 \ottdefnlintSingleBindingXXlintBinder{}
278 \ottdefnlintBinder{}
280 \subsection{Substitution consistency}
282 \ottdefncheckTyKind{}
284 \subsection{Case alternative consistency}
286 \ottdefnlintCoreAlt{}
288 \subsection{Telescope substitution}
290 \ottdefnapplyTys{}
292 \subsection{Case alternative binding consistency}
294 \ottdefnlintAltBinders{}
296 \subsection{Arrow kinding}
298 \ottdefnlintArrow{}
300 \subsection{Type application kinding}
302 \ottdefnlintXXapp{}
304 \subsection{Sub-kinding}
306 \ottdefnisSubKind{}
308 \subsection{Branched axiom conflict checking}
310 The following judgment is used within \ottdrulename{Co\_AxiomInstCo} to make
311 sure that a type family application cannot unify with any previous branch
312 in the axiom.
314 \ottdefncheckXXnoXXconflict{}
316 The judgment $[[apart]]$ checks to see whether two lists of types are surely apart.
317 It checks to see if \coderef{types/Unify.lhs}{tcApartTys} returns \texttt{SurelyApart}.
318 Two types are apart if neither type is a type family application and if they do not
319 unify.
321 \end{document}