[GHC] #15453: Bug in opt_trans_rule in OptCoercion

[GHC]

#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  ningning
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D5018
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 OK done!  Here is the original publication: [https://www.microsoft.com/en-
 us/research/publication/evidence-normalization-system-fc-2/ Evidence
 normalisation in System FC].
 {{{
 commit 3a065617b168813ec7e356ddd4eb25d125e9ff59
 Author: Simon Peyton Jones <simonpj at microsoft.com>
 Date:   Tue Jul 31 13:17:58 2018 +0100

     Add the paper "Evidence normalisation in System FC"


     This is with a view to editing it to include new developments in
     the coercion infrastructure.


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

 3a065617b168813ec7e356ddd4eb25d125e9ff59
  docs/opt-coercion/Makefile                  |    9 +
  docs/{storage-mgt => opt-coercion}/code.sty |    2 +
  docs/opt-coercion/denot.sty                 |  120 +
  docs/opt-coercion/fc-normalization-rta.bib  | 7157
 +++++++++++++++++++++++++++  docs/opt-coercion/fc-normalization-rta.tex  |
 1627 ++++++
  docs/opt-coercion/lipics.cls                |  647 +++
  docs/opt-coercion/prooftree.sty             |  347 ++
  7 files changed, 9909 insertions(+)


 }}}
 Please edit away!  Perhaps you can include a preamble saying "This is an
 updated version of the published paper.   This version is intended to
 evolve to accurately reflect GHC".

 If you want use OTT, like `core-spec` then fine.  But it may be easier
 just to work with the formatting as-is.

 A first step would be to include `GRefl` and anything else that isn't
 reflected in the paper.

 Thank you!

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15453#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler