[commit: ghc] wip/tdammers/D4394: Caching coercion roles in NthCo and coercionKindsRole refactoring (#11735) (c8efa15)

[git at git.haskell.org]

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

On branch  : wip/tdammers/D4394
Link       : http://ghc.haskell.org/trac/ghc/changeset/c8efa159be470d7039d4c09405bc04c7d3499d36/ghc

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

commit c8efa159be470d7039d4c09405bc04c7d3499d36
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Fri Jan 26 22:28:42 2018 -0500

    Caching coercion roles in NthCo and coercionKindsRole refactoring (#11735)
    
    Reviewers: goldfire, bgamari
    
    Subscribers: rwbarton, thomie, carter
    
    Differential Revision: https://phabricator.haskell.org/D4394


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

c8efa159be470d7039d4c09405bc04c7d3499d36
 docs/core-spec/CoreLint.ott  |   5 +++--
 docs/core-spec/CoreSyn.ott   |   6 ++++--
 docs/core-spec/core-spec.mng |   2 +-
 docs/core-spec/core-spec.pdf | Bin 354307 -> 355707 bytes
 4 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 3a3468d..1fb9e09 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -299,12 +299,13 @@ G |-ty ti : k2'
 not (si is_a_coercion)
 not (ti is_a_coercion)
 R' = (tyConRolesX R T)[i]
+R' <= R0
 ---------------------- :: NthCoTyCon
-G |-co nth i g : si k2~R' k2' ti
+G |-co nth R0 i g : si k2~R0 k2' ti
 
 G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2)
 --------------------------- :: NthCoForAll
-G |-co nth 0 g : k1 *~Nom * k2
+G |-co nth R0 0 g : k1 *~R0 * k2
 
 G |-co g : (s1 s2) k~Nom k' (t1 t2)
 G |-ty s1 : k1
diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index 78118d5..e12f68b 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -152,8 +152,8 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder
   | g1 ; g2                 ::   :: TransCo       {{ com \ctor{TransCo}: Transitivity }}
   | mu </ ti // i /> $ </ gj // j />
                             ::   :: AxiomRuleCo   {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }}
-  | nth I g                 ::   :: NthCo         {{ com \ctor{NthCo}: Projection (0-indexed) }}
-    {{ tex \textsf{nth}^{[[I]]}\,[[g]] }}
+  | nth R I g               ::   :: NthCo         {{ com \ctor{NthCo}: Projection (0-indexed) }}
+    {{ 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 }}
@@ -453,6 +453,8 @@ formula :: 'formula_' ::=
   | role_list1 = role_list2            ::   :: eq_role_list
   | R1 /= R2                           ::   :: role_neq
   | R1 = R2                            ::   :: eq_role
+  | R1 <= R2                           ::   :: lte_role
+    {{ tex [[R1]] \leq [[R2]] }}
   | </ Ki // i /> = tyConDataCons T    ::   :: tyConDataCons
   | O ( n ) = R                        ::   :: role_lookup
   | R elt role_list                    ::   :: role_elt
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 5800321..64e90bb 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -30,7 +30,7 @@ System FC, as implemented in GHC\footnote{This
 document was originally prepared by Richard Eisenberg (\texttt{eir at cis.upenn.edu}),
 but it should be maintained by anyone who edits the functions or data structures
 mentioned in this file. Please feel free to contact Richard for more information.}\\
-\Large 23 October, 2015
+\Large 26 January, 2018
 \end{center}
 
 \section{Introduction}
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 1e13911..3732818 100644
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ