summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRichard Eisenberg <rae@richarde.dev>2020-03-17 15:13:38 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-03-20 20:44:17 -0400
commit9a96ff6b1c19c9d0af9c9a39fb2c086f311c7239 (patch)
treeeaeb55c6af88f39be3be50fd8811a826440ca0be
parentfaa36e5b3674a7b2cfc6b931eec27b3558fad33b (diff)
downloadhaskell-9a96ff6b1c19c9d0af9c9a39fb2c086f311c7239.tar.gz
Update core spec to reflect changes to Core.
Key changes: * Adds a new rule for forall-coercions over coercion variables, which was implemented but conspicuously missing from the spec. * Adds treatment for FunCo. * Adds treatment for ForAllTy over coercion variables. * Improves commentary (including restoring a Note lost in 03d4852658e1b7407abb4da84b1b03bfa6f6db3b) in the source. No changes to running code.
-rwxr-xr-x.gitlab/linters/check-cpp.py2
-rw-r--r--compiler/GHC/Core/Coercion.hs4
-rw-r--r--compiler/GHC/Core/Lint.hs7
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs63
-rw-r--r--compiler/GHC/Core/Type.hs1
-rw-r--r--compiler/GHC/Core/Unify.hs2
-rw-r--r--docs/core-spec/.gitignore1
-rw-r--r--docs/core-spec/CoreLint.ott35
-rw-r--r--docs/core-spec/CoreSyn.ott5
-rw-r--r--docs/core-spec/core-spec.mng47
-rw-r--r--docs/core-spec/core-spec.pdfbin366905 -> 374165 bytes
11 files changed, 135 insertions, 32 deletions
diff --git a/.gitlab/linters/check-cpp.py b/.gitlab/linters/check-cpp.py
index 5377fcb005..1b4b26a760 100755
--- a/.gitlab/linters/check-cpp.py
+++ b/.gitlab/linters/check-cpp.py
@@ -29,6 +29,8 @@ for l in linters:
# Don't lint font files
l.add_path_filter(lambda path: not path.parent == Path('docs','users_guide',
'rtd-theme', 'static', 'fonts'))
+ # Don't lint core spec
+ l.add_path_filter(lambda path: not path.name == 'core-spec.pdf')
if __name__ == '__main__':
run_linters(linters)
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 317ca00906..06dfa2e02b 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -1371,7 +1371,7 @@ promoteCoercion co = case co of
ForAllCo _ _ _
-> ASSERT( False )
mkNomReflCo liftedTypeKind
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
FunCo _ _ _
-> ASSERT( False )
@@ -1420,7 +1420,7 @@ promoteCoercion co = case co of
| otherwise
-> ASSERT( False)
mkNomReflCo liftedTypeKind
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
KindCo _
-> ASSERT( False )
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 5777940ba5..b7813eb667 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -1467,7 +1467,6 @@ lintType t@(ForAllTy (Bndr cv _vis) ty)
; checkValueKind k (text "the body of forall:" <+> ppr t)
; return liftedTypeKind
-- We don't check variable escape here. Namely, k could refer to cv'
- -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
@@ -1826,7 +1825,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
; (k3, k4, t1, t2, r) <- lintCoercion co
; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
; checkValueKind k4 (text "the body of a ForAllCo over covar:" <+> ppr co)
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
; in_scope <- getInScope
; let tyl = mkTyCoInvForAllTy cv1 t1
r2 = coVarRole cv1
@@ -1845,7 +1844,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
tyr = mkTyCoInvForAllTy cv2 $
substTy subst t2
; return (liftedTypeKind, liftedTypeKind, tyl, tyr, r) } }
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
lintCoercion co@(FunCo r co1 co2)
= do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
@@ -2019,7 +2018,7 @@ lintCoercion (InstCo co arg)
, CoercionTy s2' <- s2
-> do { return $
(liftedTypeKind, liftedTypeKind
- -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
, substTy (mkCvSubst in_scope $ unitVarEnv cv1 s1') t1
, substTy (mkCvSubst in_scope $ unitVarEnv cv2 s2') t2
, r) }
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index c1ca32fc3c..1f2fd6cf19 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -206,6 +206,9 @@ data Type
| ForAllTy
{-# UNPACK #-} !TyCoVarBinder
Type -- ^ A Π type.
+ -- INVARIANT: If the binder is a coercion variable, it must
+ -- be mentioned in the Type. See
+ -- Note [Unused coercion variable in ForAllTy]
| FunTy -- ^ t1 -> t2 Very common, so an important special case
-- See Note [Function types]
@@ -218,9 +221,10 @@ data Type
| CastTy
Type
KindCoercion -- ^ A kind cast. The coercion is always nominal.
- -- INVARIANT: The cast is never refl.
+ -- INVARIANT: The cast is never reflexive
-- INVARIANT: The Type is not a CastTy (use TransCo instead)
- -- See Note [Respecting definitional equality] (EQ2) and (EQ3)
+ -- INVARIANT: The Type is not a ForAllTy over a type variable
+ -- See Note [Respecting definitional equality] (EQ2), (EQ3), (EQ4)
| CoercionTy
Coercion -- ^ Injection of a Coercion into a type
@@ -567,10 +571,19 @@ be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
our (EQ) property.
-Lastly, in order to detect reflexive casts reliably, we must make sure not
+In order to detect reflexive casts reliably, we must make sure not
to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
-In sum, in order to uphold (EQ), we need the following three invariants:
+One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy].
+The kind of the body is the same as the kind of the ForAllTy. Accordingly,
+
+ ForAllTy tv (ty |> co) and (ForAllTy tv ty) |> co
+
+are `eqType`. But only the first can be split by splitForAllTy. So we forbid
+the second form, instead pushing the coercion inside to get the first form.
+This is done in mkCastTy.
+
+In sum, in order to uphold (EQ), we need the following invariants:
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
@@ -578,7 +591,7 @@ In sum, in order to uphold (EQ), we need the following three invariants:
(EQ2) No reflexive casts in CastTy.
(EQ3) No nested CastTys.
(EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type.
+ See Note [Weird typing rule for ForAllTy]
These invariants are all documented above, in the declaration for Type.
@@ -607,6 +620,45 @@ There are cases we want to skip the check. For example, the check is
unnecessary when it is known from the context that the input variable
is a type variable. In those cases, we use mkForAllTy.
+Note [Weird typing rule for ForAllTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here is the (truncated) typing rule for the dependent ForAllTy:
+
+ inner : TYPE r
+ tyvar is not free in r
+ ----------------------------------------
+ ForAllTy (Bndr tyvar vis) inner : TYPE r
+
+Note that the kind of `inner` is the kind of the overall ForAllTy. This is
+necessary because every ForAllTy over a type variable is erased at runtime.
+Thus the runtime representation of a ForAllTy (as encoded, via TYPE rep, in
+the kind) must be the same as the representation of the body. We must check
+for skolem-escape, though. The skolem-escape would prevent a definition like
+
+ undefined :: forall (r :: RuntimeRep) (a :: TYPE r). a
+
+because the type's kind (TYPE r) mentions the out-of-scope r. Luckily, the real
+type of undefined is
+
+ undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a
+
+and that HasCallStack constraint neatly sidesteps the potential skolem-escape
+problem.
+
+If the bound variable is a coercion variable:
+
+ inner : TYPE r
+ covar is free in inner
+ ------------------------------------
+ ForAllTy (Bndr covar vis) inner : Type
+
+Here, the kind of the ForAllTy is just Type, because coercion abstractions
+are *not* erased. The "covar is free in inner" premise is solely to maintain
+the representation invariant documented in
+Note [Unused coercion variable in ForAllTy]. Though there is surface similarity
+between this free-var check and the one in the tyvar rule, these two restrictions
+are truly unrelated.
+
-}
-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
@@ -1003,6 +1055,7 @@ data Coercion
-- The TyCon is never a synonym;
-- we expand synonyms eagerly
-- But it can be a type function
+ -- TyCon is never a saturated (->); use FunCo instead
| AppCo Coercion CoercionN -- lift AppTy
-- AppCo :: e -> N -> e
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 3af971c101..3e86e86cf4 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -1382,6 +1382,7 @@ mkCastTy (CastTy ty co1) co2
mkCastTy (ForAllTy (Bndr tv vis) inner_ty) co
-- (EQ4) from the Note
+ -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep.
| isTyVar tv
, let fvs = tyCoVarsOfCo co
= -- have to make sure that pushing the co in doesn't capture the bound var!
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index 8719746f67..10b1a85342 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -1507,7 +1507,7 @@ ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
-- subst2 <- ty_co_match menv subst1 s2 eta2 kco3 kco4
-- Question: How do we get kcoi?
-- 2. Given:
--- lkco :: <*> -- See Note [Weird typing rule for ForAllTy] in GHC.Core.Type
+-- lkco :: <*> -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
-- rkco :: <*>
-- Wanted:
-- ty_co_match menv' subst2 ty1 co2 lkco' rkco'
diff --git a/docs/core-spec/.gitignore b/docs/core-spec/.gitignore
index dac3bd2547..d5181cb718 100644
--- a/docs/core-spec/.gitignore
+++ b/docs/core-spec/.gitignore
@@ -4,3 +4,4 @@
CoreOtt.tex
core-spec.tex
*.fls
+*.out
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 606e45c190..3004802ad4 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -232,8 +232,8 @@ G |-co g1 : s1 k1~R k'1 t1
G |-co g2 : s2 k2~R k'2 t2
G |-arrow k1 -> k2 : k
G |-arrow k'1 -> k'2 : k'
-------------------------- :: TyConAppCoFunTy
-G |-co (->)_R g1 g2 : (s1 -> s2) k~R k' (t1 -> t2)
+------------------------- :: FunCo
+G |-co g1 ->_R g2 : (s1 -> s2) k~R k' (t1 -> t2)
T /= (->)
</ Ri // i /> = take(length </ gi // i />, tyConRolesX R T)
@@ -258,9 +258,19 @@ G |-app (t2 : k2') : k2 ~> k4
G |-co g1 g2 : (s1 t1) k3~Ph k4 (s2 t2)
G |-co h : k1 *~Nom * k2
-G, z_k1 |-co g : t1 k3~R k4 t2
------------------------------------------------------------------- :: ForAllCo
-G |-co forall z:h. g : (forall z_k1. t1) k3~R k4 (forall z_k2. (t2[z |-> z_k2 |> sym h]))
+G, alpha_k1 |-co g : t1 k3~R k4 t2
+------------------------------------------------------------------ :: ForAllCo_Tv
+G |-co forall alpha:h. g : (forall alpha_k1. t1) k3~R k4 (forall alpha_k2. (t2[alpha |-> alpha_k2 |> sym h]))
+
+G |-co h : k1 *~Nom * k2
+G, x_k1 |-co g : t1 {TYPE s1}~R {TYPE s2} t2
+R2 = coercionRole x_k1
+h' = downgradeRole R2 h
+h1 = nth R2 2 h'
+h2 = nth R2 3 h'
+almostDevoid x g
+------------------------------------------- :: ForAllCo_Cv
+G |-co forall x:h.g : (forall x_k1. t1) *~R * (forall x_k2. (t2[ x |-> h1 ; x_k2 ; sym h2 ]))
z_phi elt G
phi = t1 k1~#k2 t2
@@ -495,10 +505,17 @@ G |-app </ (ti : ki) // i /> : tyConKind T ~> k
G |-ty T </ ti // i /> : k
G |-ki k1 ok
-G, z_k1 |-ty t : TYPE s
-not (z elt fv(s))
------------------------- :: ForAllTy
-G |-ty forall z_k1. t : TYPE s
+G, alpha_k1 |-ty t : TYPE s
+not (alpha elt fv(s))
+------------------------ :: ForAllTy_Tv
+G |-ty forall alpha_k1. t : TYPE s
+
+phi = s1 k1~#k2 s2
+G |-ki phi ok
+G, x_phi |-ty t : TYPE s
+x elt fv(t)
+--------------------- :: ForAllTy_Cv
+G |-ty forall x_phi.t : *
G |-tylit lit : k
-------------- :: LitTy
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index cb9f1fc275..9ce8b5e16d 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -143,6 +143,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| < t > R mg :: :: GRefl {{ com \ctor{GRefl}: Generalized Reflexivity }}
{{ tex {\langle [[t]] \rangle}^{[[mg]]}_{[[R]]} }}
| T RA </ gi // i /> :: :: TyConAppCo {{ com \ctor{TyConAppCo}: Type constructor application }}
+ | g1 -> RA g2 :: :: FunCo {{ com \ctor{FunCo}: Functions }}
| g1 g2 :: :: AppCo {{ com \ctor{AppCo}: Application }}
| forall z : h . g :: :: ForAllCo {{ com \ctor{ForAllCo}: Polymorphism }}
{{ tex [[forall]] [[z]]{:}[[h]].[[g]] }}
@@ -162,6 +163,7 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
| sub g :: :: SubCo {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
| ( g ) :: M :: Parens {{ com Parentheses }}
| t $ liftingsubst :: M :: Lifted {{ com Type lifted to coercion }}
+ | downgradeRole R g :: M :: downgradeRole {{ com \textsf{downgradeRole} }}
prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/TyCoRep.hs}{UnivCoProvenance} }}
| UnsafeCoerceProv :: :: UnsafeCoerceProv {{ com From \texttt{unsafeCoerce\#} }}
@@ -396,8 +398,10 @@ terminals :: 'terminals_' ::=
| --> :: :: steps {{ tex \longrightarrow }}
| coercionKind :: :: coercionKind {{ tex \textsf{coercionKind} }}
| coercionRole :: :: coercionRole {{ tex \textsf{coercionRole} }}
+ | downgradeRole :: :: downgradeRole {{ tex \textsf{downgradeRole} }}
| take :: :: take {{ tex \textsf{take}\! }}
| coaxrProves :: :: coaxrProves {{ tex \textsf{coaxrProves} }}
+ | almostDevoid :: :: almostDevoid {{ tex \textsf{almostDevoid} }}
| Just :: :: Just {{ tex \textsf{Just} }}
| \\ :: :: newline {{ tex \\ }}
| classifiesTypeWithValues :: :: ctwv {{ tex \textsf{classifiesTypeWithValues} }}
@@ -483,6 +487,7 @@ formula :: 'formula_' ::=
| z elt vars :: :: in_vars
| split _ I s = types :: :: split_type
{{ tex \mathop{\textsf{split} }_{[[I]]} [[s]] = [[types]] }}
+ | almostDevoid x g :: :: almostDevoid
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Subrules and Parsing %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 167ca85644..ea488921be 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -7,6 +7,7 @@
\usepackage{xcolor}
\usepackage{fullpage}
\usepackage{multirow}
+\usepackage{hyperref}
\usepackage{url}
\newcommand{\ghcfile}[1]{\textsl{#1}}
@@ -106,10 +107,10 @@ There are a few key invariants about expressions:
\item The right-hand sides of all top-level and recursive $[[let]]$s
must be of lifted type, with one exception: the right-hand side of a top-level
$[[let]]$ may be of type \texttt{Addr\#} if it's a primitive string literal.
-See \verb|#top_level_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
+See \verb|#top_level_invariant#| in \ghcfile{GHC.Core}.
\item The right-hand side of a non-recursive $[[let]]$ and the argument
of an application may be of unlifted type, but only if the expression
-is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{coreSyn/CoreSyn.hs}.
+is ok-for-speculation. See \verb|#let_app_invariant#| in \ghcfile{GHC.Core}.
\item We allow a non-recursive $[[let]]$ for bind a type variable.
\item The $[[_]]$ case for a $[[case]]$ must come first.
\item The list of case alternatives must be exhaustive.
@@ -119,7 +120,7 @@ In other words, the payload inside of a \texttt{Type} constructor must not turn
to be built with \texttt{CoercionTy}.
\item Join points (introduced by $[[join]]$ expressions) follow the invariants
laid out in \verb|Note [Invariants on join points]| in
-\ghcfile{coreSyn/CoreSyn.hs}:
+\ghcfile{GHC.Core}:
\begin{enumerate}
\item All occurrences must be tail calls. This is enforced in our typing
rules using the label environment $[[D]]$.
@@ -166,13 +167,14 @@ A program is just a list of bindings:
\gram{\ottprogram}
\subsection{Types}
+\label{sec:types}
\gram{\ottt}
\ctor{FunTy} is the special case for non-dependent function type. The
-\ctor{TyBinder} in \ghcfile{types/TyCoRep.hs} distinguishes whether a binder is
+\ctor{TyBinder} in \ghcfile{GHC.Core.TyCo.Rep} distinguishes whether a binder is
anonymous (\ctor{FunTy}) or named (\ctor{ForAllTy}). See
-\verb|Note [TyBinders]| in \ghcfile{types/TyCoRep.hs}.
+\verb|Note [TyBinders]| in \ghcfile{GHC.Core.TyCo.Rep}.
There are some invariants on types:
\begin{itemize}
@@ -191,7 +193,7 @@ a term-level literal, but we are ignoring this distinction here.
\item If $[[forall n. t]]$ is a polymorphic type over a coercion variable (i.e.
$[[n]]$ is a coercion variable), then $[[n]]$ must appear in $[[t]]$;
otherwise it should be represented as a \texttt{FunTy}. See \texttt{Note
- [Unused coercion variable in ForAllTy]} in \ghcfile{types/TyCoRep.hs}.
+ [Unused coercion variable in ForAllTy]} in \ghcfile{GHC.Core.TyCo.Rep}.
\end{itemize}
Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
@@ -216,14 +218,15 @@ Invariants on coercions:
reflexive, use $[[T_R </ gi // i />]]$, never $[[<T> g1 g2]] \ldots$.
\item The $[[T]]$ in $[[T_R </gi//i/>]]$ is never a type synonym, though it could
be a type function.
-\item Every non-reflexive coercion coerces between two distinct types.
\item The name in a coercion must be a term-level name (\ctor{Id}).
\item The contents of $[[<t>]]$ must not be a coercion. In other words,
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\item If $[[forall z: h .g]]$ is a polymorphic coercion over a coercion variable
(i.e. $[[z]]$ is a coercion variable), then $[[z]]$ can only appear in
- \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note[Unused coercion
- variable in ForAllCo] in \ghcfile{types/Coercion.hs}}.
+ \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note [Unused coercion
+ variable in ForAllCo] in \ghcfile{GHC.Core.Coercion}}.
+\item Prefer $[[g1 ->_R g2]]$ over $[[(->)_R g1 g2]]$; that is, we use \ctor{FunCo},
+never \ctor{TyConAppCo}, for coercions over saturated uses of $[[->]]$.
\end{itemize}
The \texttt{UnivCo} constructor takes several arguments: the two types coerced
@@ -327,7 +330,7 @@ synonym for $[[TYPE 'Unlifted]]$.
\section{Contexts}
-The functions in \ghcfile{coreSyn/CoreLint.hs} use the \texttt{LintM} monad.
+The functions in \ghcfile{GHC.Core.Lint} use the \texttt{LintM} monad.
This monad contains a context with a set of bound variables $[[G]]$ and a set
of bound labels $[[D]]$. The formalism treats $[[G]]$ and $[[D]]$ as ordered
lists, but GHC uses sets as its
@@ -432,6 +435,15 @@ a dead id and for one-tuples. These checks are omitted here.
\ottdefnlintType{}
+Note the contrast between \ottdrulename{Ty\_ForAllTy\_Tv} and \ottdrulename{Ty\_ForAllTy\_Cv}.
+The former checks type abstractions, which are erased at runtime. Thus, the kind of the
+body must be the same as the kind of the $[[forall]]$-type (as these kinds indicate
+the runtime representation). The latter checks coercion abstractions, which are \emph{not}
+erased at runtime. Accordingly, the kind of a coercion abstraction is $[[*]]$. The
+\ottdrulename{Ty\_ForAllTy\_Cv} rule also asserts that the bound variable $[[x]]$ is
+actually used in $[[t]]$: this is to uphold a representation invariant, documented
+with the grammar for types, Section~\ref{sec:types}.
+
\subsection{Kind validity}
\ottdefnlintKind{}
@@ -451,6 +463,19 @@ and \ottdrulename{Co\_CoVarCoRepr}.
See Section~\ref{sec:tyconroles} for more information about $[[tyConRolesX]]$, and
see Section~\ref{sec:axiom_rules} for more information about $[[coaxrProves]]$.
+The $[[downgradeRole R g]]$ function returns a new coercion that relates the same
+types as $[[g]]$ but with role $[[R]]$. It assumes that the role of $[[g]]$ is a
+sub-role ($\leq$) of $[[R]]$.
+
+The $[[almostDevoid x g]]$ function makes sure that, if $[[x]]$ appears at all
+in $[[g]]$, it appears only within a \ctor{Refl} or \ctor{GRefl} node. See
+Section 5.8.5.2 of Richard Eisenberg's thesis for the details, or the ICFP'17
+paper ``A Specification for Dependently-Typed Haskell''. (Richard's thesis
+uses a technical treatment of this idea that's very close to GHC's implementation.
+The ICFP'17 paper approaches the same restriction in a different way, by using
+\emph{available sets} $\Delta$, as explained in Section 4.2 of that paper.
+We believe both technical approaches are equivalent in what coercions they accept.)
+
\subsection{Name consistency}
\label{sec:name_consistency}
@@ -463,7 +488,7 @@ There are three very similar checks for names, two performed as part of
The point of the extra checks on $[[t']]$ is that a join point's type cannot be
polymorphic in its return type; see \texttt{Note [The polymorphism rule of join
-points]} in \ghcfile{coreSyn/CoreSyn.hs}.
+points]} in \ghcfile{GHC.Core}.
\ottdefnlintBinder{}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index ad2d57196c..75bb620edc 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf
Binary files differ