[GHC] #15192: Refactor of Coercion

[GHC]

#15192: Refactor of Coercion
-------------------------------------+-------------------------------------
           Reporter:  ningning       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.2.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This patch aims at defining the new coercion rule

 {{{#!hs
   | EraseEqCo Role Type Type KindCoercion
      -- "e" -> _ -> _ -> N -> e
 }}}

 which corresponds to the typing rule

 {{{
   t1 : k1   t2 : k2   |t1| = |t2|   g : k1 ~ k2
   ------------------------------------
   EraseEqCo r t1 t2 g : t1 ~r t2
 }}}

 Namely, if two types after erasure of casts and coercions are equivalent,
 then they can be casted from and to each other. This new coercion rule is
 designed to replace the current coherence rule

 {{{#!hs
   -- Coherence applies a coercion to the left-hand type of another
 coercion
   -- See Note [Coherence]
   | CoherenceCo Coercion KindCoercion
      -- :: e -> N -> e
 }}}

 The new rule is useful in several places. For example, now it is easier to
 define coercion {{{t |> k ~ t}}} without resorting to reflexivity
 coercion, and {{{t ~ t |> k}}} without resorting to symmetric rule.

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