Revert "Support for multiple signature files in scope."
[ghc.git] / docs / core-spec / core-spec.mng
index 246be06..7830e89 100644 (file)
@@ -7,6 +7,7 @@
 \usepackage{xcolor}
 \usepackage{fullpage}
 \usepackage{multirow}
+\usepackage{url}
 
 \newcommand{\ghcfile}[1]{\textsl{#1}}
 \newcommand{\arraylabel}[1]{\multicolumn{2}{l}{\!\!\!\!\!\!\!\!\!\text{\underline{#1}:}}}
@@ -19,7 +20,7 @@
 \setlength{\parindent}{0in}
 \setlength{\parskip}{1ex}
 
-\newcommand{\gram}[1]{\ottgrammartabular{#1\ottinterrule}}
+\newcommand{\gram}[1]{\ottgrammartabular{#1\ottafterlastrule}}
 
 \begin{document}
 
@@ -29,7 +30,7 @@ System FC, as implemented in GHC\footnote{This
 document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}),
 but it should be maintained by anyone who edits the functions or data structures
 mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large 2 August, 2013
+\Large 23 April 2015
 \end{center}
 
 \section{Introduction}
@@ -74,7 +75,9 @@ We also leave abstract the function \coderef{basicTypes/Literal.lhs}{literalType
 and the judgment \coderef{coreSyn/CoreLint.lhs}{lintTyLit} (written $[[G |-tylit lit : k]]$).
 
 \subsection{Variables}
-
+\enlargethispage{10pt} % without this first line of "z" definition is placed on
+                       % second page and it becomes the only line of text on that
+                       % page, resulting in whole page being empty.
 GHC uses the same datatype to represent term-level variables and type-level
 variables:
 
@@ -133,9 +136,9 @@ There are some invariants on types:
 \begin{itemize}
 \item The type $[[t1]]$ in the form $[[t1 t2]]$ must not be a type constructor
 $[[T]]$. It should be another application or a type variable.
-\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp}) 
+\item The form $[[T </ ti // i /> ]]$ (\texttt{TyConApp})
 does \emph{not} need to be saturated.
-\item A saturated application of $[[(->) t1 t2]]$ should be represented as 
+\item A saturated application of $[[(->) t1 t2]]$ should be represented as
 $[[t1 -> t2]]$. This is a different point in the grammar, not just pretty-printing.
 The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
 \item A type-level literal is represented in GHC with a different datatype than
@@ -148,13 +151,21 @@ a term-level literal, but we are ignoring this distinction here.
 
 Invariants on coercions:
 \begin{itemize}
-\item $[[<t1 t2>]]$ is used; never $[[<t1> <t2>]]$.
-\item If $[[<T>]]$ is applied to some coercions, at least one of which is not
-reflexive, use $[[T </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
-\item The $[[T]]$ in $[[T </gi//i/>]]$ is never a type synonym, though it could
+\item $[[<t1 t2>_R]]$ is used; never $[[<t1>_R <t2>_Nom]]$.
+\item If $[[<T>_R]]$ is applied to some coercions, at least one of which is not
+reflexive, use $[[T_R </ gi // i />]]$, never $[[<T>_R g1 g2]] \ldots$.
+\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
 be a type function.
 \end{itemize}
 
+Roles label what equality relation a coercion is a witness of. Nominal equality
+means that two types are identical (have the same name); representational equality
+means that two types have the same representation (introduced by newtypes); and
+phantom equality includes all types. See \url{http://ghc.haskell.org/trac/ghc/wiki/Roles}
+for more background.
+
+\gram{\ottR}
+
 Is it a left projection or a right projection?
 
 \gram{\ottLorR}
@@ -172,6 +183,31 @@ as that would unduly clutter this presentation. Instead, as the list
 of incompatible branches can be computed at any time, it is checked for
 in the judgment $[[no_conflict]]$. See Section~\ref{sec:no_conflict}.
 
+Axiom rules, produced by the type-nats solver:
+
+\gram{\ottmu}
+
+\label{sec:axiom_rules}
+An axiom rule $[[mu]] = [[M(I, role_list, R')]]$ is an axiom name $[[M]]$, with a
+type arity $[[I]]$, a list of roles $[[role_list]]$ for its coercion parameters,
+and an output role $[[R']]$. The definition within GHC also includes a field named
+$[[coaxrProves]]$ which computes the output coercion from a list of types and
+a list of coercions. This is elided in this presentation, as we simply identify
+axiom rules by their names $[[M]]$. See also \coderef{typecheck/TcTypeNats.lhs}{mkBinAxiom}
+and \coderef{typecheck/TcTypeNats.lhs}{mkAxiom1}.
+
+In \ottdrulename{Co\_UnivCo}, function $ \textsf{compatibleUnBoxedTys} $ stands for following checks:
+\begin{itemize}
+    \item both types are unboxed;
+    \item types should have same size;
+    \item both types should be either integral or floating;
+    \item coercion between vector types are not allowed;
+    \item unboxed tuples should have same length and each element should be coercible to
+    appropriate element of the target tuple;
+\end{itemize}
+For function implementation see \coderef{coreSyn/CoreLint.lhs}{checkTypes}.
+For futher discussion see \url{https://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions}.
+
 \subsection{Type constructors}
 
 Type constructors in GHC contain \emph{lots} of information. We leave most of it out
@@ -237,12 +273,6 @@ as for strictness and exportability. See the source code for further information
 
 \ottdefnlintCoreExpr{}
 
-%\arraylabel{\coderef{coreSyn/CoreLint.lhs}{checkCaseAlts}} \\
-%\multicolumn{2}{l}{[[checkCaseAlts]] \text{ checks ordering and exhaustivity constr%aints}} \\
-
-%\end{array}
-%\]
-
 \begin{itemize}
 \item Some explication of \ottdrulename{Tm\_LetRec} is helpful: The idea behind the
 second premise ($[[</ G, G'i |-ty s'i : ki // i />]]$) is that we wish
@@ -285,12 +315,23 @@ a dead id and for one-tuples. These checks are omitted here.
 
 \subsection{Coercion typing}
 
+In the coercion typing judgment, the $\#$ marks are left off the equality
+operators to reduce clutter. This is not actually inconsistent, because
+the GHC function that implements this check, \texttt{lintCoercion}, actually
+returns four separate values (the kind, the two types, and the role), not
+a type with head $[[(~#)]]$ or $[[(~R#)]]$. Note that the difference between
+these two forms of equality is interpreted in the rules \ottdrulename{Co\_CoVarCoNom}
+and \ottdrulename{Co\_CoVarCoRepr}.
+
 \ottdefnlintCoercion{}
 
 In \ottdrulename{Co\_AxiomInstCo}, the use of $[[inits]]$ creates substitutions from
-the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of 
+the first $i$ mappings in $[[ </ [ni |-> si] // i /> ]]$. This has the effect of
 folding the substitution over the kinds for kind-checking.
 
+See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
+see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
+
 \subsection{Name consistency}
 
 There are two very similar checks for names, one declared as a local function:
@@ -327,6 +368,34 @@ There are two very similar checks for names, one declared as a local function:
 
 \ottdefnisSubKind{}
 
+\subsection{Roles}
+\label{sec:tyconroles}
+
+During type-checking, role inference is carried out, assigning roles to the
+arguments of every type constructor. The function $[[tyConRoles]]$ extracts these
+roles. Also used in other judgments is $[[tyConRolesX]]$, which is the same as
+$[[tyConRoles]]$, but with an arbitrary number of $[[Nom]]$ at the end, to account
+for potential oversaturation.
+
+The checks encoded in the following
+judgments are run from \coderef{typecheck/TcTyClsDecls.lhs}{checkValidTyCon}
+when \texttt{-dcore-lint} is set.
+
+\ottdefncheckValidRoles{}
+
+\ottdefncheckXXdcXXroles{}
+
+In the following judgment, the role $[[R]]$ is an \emph{input}, not an output.
+The metavariable $[[O]]$ denotes a \emph{role context}, as shown here:
+
+\gram{\ottO}
+
+\ottdefncheckXXtyXXroles{}
+
+These judgments depend on a sub-role relation:
+
+\ottdefnltRole{}
+
 \subsection{Branched axiom conflict checking}
 \label{sec:no_conflict}
 
@@ -377,11 +446,13 @@ use of FC does not require modeling recursion, you will not need to track $[[S]]
 \subsection{Notes}
 
 \begin{itemize}
-\item The \ottdrulename{S\_LetRec} and \ottdrulename{S\_LetRecReturn} rules
+\item The \ottdrulename{S\_LetRec} rules
 implement recursion. \ottdrulename{S\_LetRec} adds to the context $[[S]]$ bindings
 for all of the mutually recursive equations. Then, after perhaps many steps,
 when the body of the $[[let]]\ [[rec]]$ contains no variables that are bound
-in the $[[let]]\ [[rec]]$, the context is popped.
+in the $[[let]]\ [[rec]]$, the context is popped in \ottdrulename{S\_LetRecReturn}.
+The other \ottdrulename{S\_LetRecXXX}
+rules are there to prevent reduction from getting stuck.
 \item In the $[[case]]$ rules, a constructor $[[K]]$ is written taking three
 lists of arguments: two lists of types and a list of terms. The types passed
 in are the universally and, respectively, existentially quantified type variables