update core-spec for GRefl and re-factored Refl

Ticket #15192 introduced the generalized reflexive coercion `GRefl` and
nominal reflexive `Refl`, and removed `CoherenceCo`. Update core-spec
accordingly.  Not sure about notations though; suggestions on more
concise notations would be great.

Test Plan: Read core-spec.pdf

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, carter

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

5 files changed, 41 insertions, 15 deletions

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index d18525a028..6ace483cb5 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -217,7 +217,16 @@ by
 
 G |-ty t : k
 ---------------------- :: Refl
-G |-co <t>_R : t k~R k t
+G |-co <t> : t k~Nom k t
+
+G |-ty t : k
+---------------------- :: GReflMRefl
+G |-co <t> R MRefl : t k~R k t
+
+G |-ty t : k1
+G |-co g : k1 *~Nom * k2
+---------------------- :: GReflMCo
+G |-co <t> R MCo g : t k1~R k2 (t |> g)
 
 G |-co g1 : s1 k1~R k'1 t1
 G |-co g2 : s2 k2~R k'2 t2
@@ -339,11 +348,6 @@ G |-ty t2 : k'
 G |-co C ind </ gi // i /> : s2 k~R0 k' t2
 
 G |-co g : t1 k1~R k2 t2
-G |-ty t1 |> h : k1'
----------------------------------- :: CoherenceCo
-G |-co g |> h : t1 |> h k1'~R k2 t2
-
-G |-co g : t1 k1~R k2 t2
 -------------------------- :: KindCo
 G |-co kind g : k1 *~Nom * k2
 
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 57ed6e261d..b11730c276 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -138,8 +138,10 @@ t {{ tex \tau }}, k {{ tex \kappa }}, s {{ tex \sigma }}, phi {{ tex \phi }}
 %% COERCIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coderef{types/TyCoRep.lhs}{Coercion} }}
-  | < t > _ R               ::   :: Refl          {{ com \ctor{Refl}: Reflexivity }}
-    {{ tex {\langle [[t]] \rangle}_{[[R]]} }}
+  | < t >                   ::   :: Refl          {{ com \ctor{Refl}: Nominal Reflexivity }}
+    {{ tex {\langle [[t]] \rangle} }}
+  | < 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 g2                   ::   :: AppCo         {{ com \ctor{AppCo}: Application }}
   | forall z : h . g        ::   :: ForAllCo      {{ com \ctor{ForAllCo}: Polymorphism }}
@@ -156,7 +158,6 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
     {{ tex \textsf{nth}^{[[I]]}_{[[R]]}\,[[g]] }}
   | LorR g                  ::   :: LRCo          {{ com \ctor{LRCo}: Left/right projection }}
   | g @ h                   ::   :: InstCo        {{ com \ctor{InstCo}: Instantiation }}
-  | g |> h                  ::   :: CoherenceCo   {{ com \ctor{CoherenceCo}: Coherence }}
   | kind g                  ::   :: KindCo        {{ com \ctor{KindCo}: Kind extraction }}
   | sub g                   ::   :: SubCo         {{ com \ctor{SubCo}: Sub-role --- convert nominal to representational }}
   | ( g )                   :: M :: Parens        {{ com Parentheses }}
@@ -170,6 +171,11 @@ prov :: 'UnivCoProvenance_' ::= {{ com \ctor{UnivCo} provenance, \coderef{types/
   | ProofIrrelProv     ::   :: ProofIrrelProv    {{ com From proof irrelevance }}
     {{ tex \mathsf{irrel} }}
 
+mg {{ tex m }} :: 'MCoercion_' ::= {{ com A possibly reflexive coercion , \coderef{types/TyCoRep.lhs}{MCoercion} }}
+  | MRefl            ::   :: MRefl                {{ com \ctor{MRefl}: A trivial reflexive coercion }}
+  | MCo g            ::   :: MCo                  {{ com \ctor{MCo}: Other coercions }}
+    {{ tex [[g]] }}
+
 LorR :: 'LeftOrRight_' ::= {{ com left or right deconstructor, \coderef{types/TyCoRep.lhs}{LeftOrRight} }}
   | Left             ::   :: CLeft                {{ com \ctor{CLeft}: Left projection }}
   | Right            ::   :: CRight               {{ com \ctor{CRight}: Right projection }}
@@ -397,6 +403,8 @@ terminals :: 'terminals_' ::=
   | classifiesTypeWithValues :: :: ctwv   {{ tex \textsf{classifiesTypeWithValues} }}
   | 0            ::   :: zero             {{ tex 0 }}
   | +1           ::   :: succ             {{ tex +1 }}
+  | MRefl        ::   :: mrefl            {{ tex \cdot }}
+  | MCo          ::   :: mco
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%  Formulae  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 389c5e8106..b9dc4ff893 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -52,7 +52,7 @@ not e2 is_a_coercion
 g' = sym (nth Nom 0 g)
 t' = t |> g'
 -------------------------------------------------------- :: TPush
-((\n.e) |> g) t --> ((\n.e) t') |> (g @ (<t>_Nom |> g'))
+((\n.e) |> g) t --> ((\n.e) t') |> (g @ (sym <t> Nom MCo g'))
 
 % g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6)
 % g2 : t3 ~Rep# t6
@@ -103,7 +103,7 @@ case e as n return t of </ alti // i /> --> u[n |-> e]
 T </ taa // aa /> k'~Rep# k T </ t'aa // aa /> = coercionKind g
 </ Raa // aa /> = tyConRoles T
 forall </ alphaaa_kaa // aa />. forall </ betabb_k'bb // bb />. </ t1cc // cc /> $ -> T </ alphaaa_kaa // aa /> = dataConRepType K
-</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>_Nom] // bb />) // cc />
+</ e'cc = ecc |> (t1cc $ </ [alphaaa_kaa |-> nth Raa aa g] // aa /> </ [betabb_k'bb |-> <sbb>] // bb />) // cc />
 --------------------------- :: CasePush
 case (K </ taa // aa /> </ sbb // bb /> </ ecc // cc />) |> g as n return t2 of </ alti // i /> --> \\ case K </ t'aa // aa /> </ sbb // bb /> </ e'cc // cc /> as n return t2 of </ alti // i />
 
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 19dabcb1bd..952a172e6f 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -207,14 +207,14 @@ We use the notation $[[t1 k1~#k2 t2]]$ to stand for $[[(~#) k1 k2 t1 t2]]$.
 
 Invariants on coercions:
 \begin{itemize}
-\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 $[[<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_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>_R]]$ must not be a coercion. In other words,
+\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}.
 \end{itemize}
 
@@ -232,6 +232,20 @@ for more background.
 
 \gram{\ottR}
 
+The \texttt{GRefl} constructor taks an $[[mg]]$. It wraps a kind coercion, which
+might be reflexive or any coercion:
+
+\gram{\ottmg}
+
+A nominal reflexive coercion is quite common, so we keep the special form
+\texttt{Refl}. Invariants on reflexive coercions:
+
+\begin{itemize}
+\item Always use $[[<t>]]$; never $[[<t> Nom MRefl]]$.
+\item All invariants on $[[<t>]]$ hold for $[[<t> R MRefl]]$.
+\item Use $[[<t> Rep MRefl]]$; never $[[sub <t>]]$.
+\end{itemize}
+
 Is it a left projection or a right projection?
 
 \gram{\ottLorR}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 21a8852d04..a0a73cbaba 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf