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.

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