[commit: ghc] master: Modernize S_TPush in the core spec (7fe4993)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/7fe4993673e43e5b21f38d79ecc8b5163e97ee84/ghc

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

commit 7fe4993673e43e5b21f38d79ecc8b5163e97ee84
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Mon Jul 16 18:10:01 2018 -0400

    Modernize S_TPush in the core spec
    
    Summary:
    The specification for the `S_TPush` rule in the core spec's
    operational semantics is woefully out-of-date. Let's bring it in line
    with the presentation in //System FC with Explicit Kind Equality//.
    
    Test Plan: Read it
    
    Reviewers: goldfire, bgamari
    
    Reviewed By: goldfire
    
    Subscribers: rwbarton, thomie, carter
    
    Differential Revision: https://phabricator.haskell.org/D4970


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

7fe4993673e43e5b21f38d79ecc8b5163e97ee84
 docs/core-spec/OpSem.ott     |  10 ++++++++--
 docs/core-spec/core-spec.pdf | Bin 354450 -> 354354 bytes
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/docs/core-spec/OpSem.ott b/docs/core-spec/OpSem.ott
index efed85a..389c5e8 100644
--- a/docs/core-spec/OpSem.ott
+++ b/docs/core-spec/OpSem.ott
@@ -45,8 +45,14 @@ not e2 is_a_coercion
 ----------------------------------------------- :: Push
 ((\n.e1) |> g) e2 --> (\n.e1 |> g1) (e2 |> g0)
 
----------------------------------------- :: TPush
-((\n.e) |> g) t --> (\n.(e |> g n)) t
+% g : (forall (a : k1). t1) ~Rep# (forall (a : k2). t2)
+% t : k2
+% g' : k2 ~# k1
+% t' : k1
+g' = sym (nth Nom 0 g)
+t' = t |> g'
+-------------------------------------------------------- :: TPush
+((\n.e) |> g) t --> ((\n.e) t') |> (g @ (<t>_Nom |> g'))
 
 % g : ((t1 ~rho# t2) -> t3) ~Rep# ((t4 ~rho# t5) -> t6)
 % g2 : t3 ~Rep# t6
diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf
index 97694dc..21a8852 100644
Binary files a/docs/core-spec/core-spec.pdf and b/docs/core-spec/core-spec.pdf differ