[commit: ghc] master: Update core-spec for Coercion Quantification (3905c3c)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/3905c3c07ba2735e5b3d2dc3389272d5dbb1c503/ghc

>---------------------------------------------------------------

commit 3905c3c07ba2735e5b3d2dc3389272d5dbb1c503
Author: Ningning Xie <xnningxie at gmail.com>
Date:   Thu Oct 25 22:01:21 2018 +0800

    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


>---------------------------------------------------------------

3905c3c07ba2735e5b3d2dc3389272d5dbb1c503
 docs/core-spec/Makefile      |   4 +++-
 docs/core-spec/core-spec.mng |  10 +++++++++-
 docs/core-spec/core-spec.pdf | Bin 356480 -> 366926 bytes
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/docs/core-spec/Makefile b/docs/core-spec/Makefile
index de0cac6..06b41ca 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 952a172..bdebc32 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 a0a73cb..0c238c5 100644
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ