[GHC] #14975: Refactor (Maybe Coercion)

[GHC]

#14975: Refactor (Maybe Coercion)
-------------------------------------+-------------------------------------
        Reporter:  tdammers          |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11735            |  Differential Rev(s):  Phab:D4699
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Richard Eisenberg <rae@…>):

 In [changeset:"55a3f8552c9dc9b84e204ec6623c698912795347/ghc" 55a3f85/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="55a3f8552c9dc9b84e204ec6623c698912795347"
 Refactor coercion rule

 Summary:
 The patch is an attempt on #15192.

 It defines a new coercion rule

 ```
  | GRefl Role Type MCoercion
 ```

 which correspondes to the typing rule

 ```
      t1 : k1
   ------------------------------------
   GRefl r t1 MRefl: t1 ~r t1

      t1 : k1       co :: k1 ~ k2
   ------------------------------------
   GRefl r t1 (MCo co) : t1 ~r t1 |> co
 ```

 MCoercion wraps a coercion, which might be reflexive (MRefl)
 or not (MCo co). To know more about MCoercion see #14975.

 We keep Refl ty as a special case for nominal reflexive coercions,
 naemly, Refl ty :: ty ~n ty.

 This commit is meant to be a general performance improvement,
 but there are a few regressions. See #15192, comment:13 for
 more information.

 Test Plan: ./validate

 Reviewers: bgamari, goldfire, simonpj

 Subscribers: rwbarton, thomie, carter

 GHC Trac Issues: #15192

 Differential Revision: https://phabricator.haskell.org/D4747
 }}}

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