Fix parse errors in core-spec.pdf

Summary:
`core-spec.pdf` was emitting parse errors due to not specifying
role arguments in some uses of `nth`. This patch adds those
role arguments. (Credit goes to Richard Eisenberg for actually
figuring out what said arguments should be.)

Test Plan: Read it

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15373

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

3 files changed, 25 insertions, 7 deletions

diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott
index c8615ad8a6..57ed6e261d 100644
--- a/docs/core-spec/CoreSyn.ott
+++ b/docs/core-spec/CoreSyn.ott
@@ -275,6 +275,7 @@ ind, I {{ tex i }} :: 'Ind_' ::= {{ com Indices, numbers }}
   | 0                           :: M :: zero
   | 1                           :: M :: one
   | 2                           :: M :: two
+  | 3                           :: M :: three
 
 terms :: 'Terms_' ::= {{ com List of terms }}
   | </ ei // i />      ::   :: List
@@ -388,6 +389,7 @@ terminals :: 'terminals_' ::=
   | validDcRoles ::   :: validDcRoles     {{ tex \textsf{validDcRoles} }}
   | -->          ::   :: steps            {{ tex \longrightarrow }}
   | coercionKind ::   :: coercionKind     {{ tex \textsf{coercionKind} }}
+  | coercionRole ::   :: coercionRole     {{ tex \textsf{coercionRole} }}
   | take         ::   :: take             {{ tex \textsf{take}\! }}
   | coaxrProves  ::   :: coaxrProves      {{ tex \textsf{coaxrProves} }}
   | Just         ::   :: Just             {{ tex \textsf{Just} }}
@@ -465,6 +467,7 @@ formula :: 'formula_' ::=
   | no other case matches              ::   :: no_other_case
     {{ tex \text{no other case matches} }}
   | t = coercionKind g                 ::   :: coercionKind
+  | R = coercionRole g                 ::   :: coercionRole
   | Just ( t1 , t2 ) = coaxrProves mu </ si // i /> </ ( s'j , s''j ) // j />
                                        ::   :: coaxrProves
   | mu1 = mu2                          ::   :: mu_rewrite
diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index 03be476bbb..efed85a5f5 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -34,8 +34,12 @@ e1 e2 --> e1' e2
 ----------------------------- :: Beta
 (\n.e1) e2 --> e1[n |-> e2]
 
-g0 = sym (nth 0 g)
-g1 = nth 1 g
+% g : (t1 -> t2) ~Rep# (t3 -> t4)
+% e2 : t3
+% g0 : t3 ~Rep# t1
+% g1 : t2 ~Rep# t4
+g0 = sym (nth Rep 2 g)
+g1 = nth Rep 3 g
 not e2 is_a_type
 not e2 is_a_coercion
 ----------------------------------------------- :: Push
@@ -44,9 +48,19 @@ not e2 is_a_coercion
 ---------------------------------------- :: TPush
 ((\n.e) |> g) t --> (\n.(e |> g n)) t
 
-g0 = nth 1 (nth 0 g)
-g1 = sym (nth 2 (nth 0 g))
-g2 = nth 1 g
+% g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6)
+% g2 : t3 ~Rep# t6
+% g' : t4 ~rho# t5
+% g0 : t1 ~rho# t4
+% g1 : t5 ~rho# t2
+% recall that (->) :: forall r1 r2. TYPE r1 -> TYPE r2 -> Type
+% and that (~#) :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
+% so pulling out the first visible argument for both is argument 2,
+% and the second visible argument for both is argument 3
+R = coercionRole g'
+g0 = nth R 2 (nth Rep 2 g)
+g1 = sym (nth R 3 (nth Rep 2 g))
+g2 = nth Rep 3 g
 ------------------------------- :: CPush
 ((\n.e) |> g) g' --> (\n.e |> g2) (g0 ; g' ; g1)
 
@@ -80,9 +94,10 @@ no other case matches
 ------------------------------------------------------------ :: MatchDefault
 case e as n return t of </ alti // i /> --> u[n |-> e]
 
-T </ taa // aa /> k'~#k T </ t'aa // aa /> = coercionKind g
+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 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>_Nom] // 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.pdf b/docs/core-spec/core-spec.pdf
index 372a18dff8..97694dcfc2 100644
--- a/docs/core-spec/core-spec.pdf
+++ b/docs/core-spec/core-spec.pdf