Update core-spec for Coercion Quantification

Summary:
Update details for `ForAllTy` and `ForAllCo` in core-spec, as they
can now quantify over coercion variables.

Test Plan: Please read core-spec.pdf

Reviewers: goldfire, simonpj, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15497, #15589

Differential Revision: https://phabricator.haskell.org/D5247

3 files changed, 12 insertions, 2 deletions

diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index de0cac6e24..06b41cac88 100644
--- a/docs/core-spec/Makefile
+++ b/docs/core-spec/Makefile
@@ -3,6 +3,8 @@ OTT_TEX   = CoreOtt.tex
 OTT_OPTS  = -tex_show_meta false
 TARGET    = core-spec
 
+all: $(TARGET).pdf
+
 $(TARGET).pdf: $(TARGET).tex $(OTT_TEX)
 	latex -output-format=pdf $<
 	latex -output-format=pdf $<
@@ -13,6 +15,6 @@ $(TARGET).tex: $(TARGET).mng $(OTT_FILES)
 $(OTT_TEX): $(OTT_FILES)
 	ott -tex_wrap false $(OTT_OPTS) -o $@ $^
 
-.PHONY: clean
+.PHONY: all clean
 clean:
 	rm -f $(TARGET).pdf $(TARGET).tex $(OTT_TEX) *.aux *.fdb_latexmk *.log *.fls
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 952a172e6f..bdebc32c90 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -188,6 +188,10 @@ The constructor for a saturated $[[(->)]]$ is \texttt{FunTy}.
 a term-level literal, but we are ignoring this distinction here.
 \item A coercion used as a type should appear only in the right-hand side of
   an application.
+\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}.
 \end{itemize}
 
 Note that the use of the $[[T </ ti // i />]]$ form and the $[[t1 -> t2]]$ form
@@ -195,7 +199,7 @@ are purely representational. The metatheory would remain the same if these forms
 were removed in favor of $[[t1 t2]]$. Nevertheless, we keep all three forms in
 this documentation to accurately reflect the implementation.
 
-The \texttt{ArgFlag} field of a \texttt{TyVarBinder} (the first argument to a
+The \texttt{ArgFlag} field of a \texttt{TyCoVarBinder} (the first argument to a
 \texttt{ForAllTy}) also tracks visibility of arguments. Visibility affects
 only source Haskell, and is omitted from this presentation.
 
@@ -216,6 +220,10 @@ be a type function.
 \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}}.
 \end{itemize}
 
 The \texttt{UnivCo} constructor takes several arguments: the two types coerced
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index a0a73cbaba..0c238c577a 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf