[GHC] #15497: Coercion Quantification

[GHC]

#15497: Coercion Quantification
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  (none)
            Type:  task              |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:
      Resolution:  fixed             |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D5054
       Wiki Page:                    |
  https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2|
-------------------------------------+-------------------------------------

Comment (by simonpj):

 On coercion quantification, I think it would be helpful to update
 [wiki:DependentHaskell/Phase2]

 * Under "Why homogeneous equality is good" explain how homogeneous
 equality can help the simplifier (in `exprIsConApp_maybe`).

 * On the same page, under "A small wrinkle: we need coercion
 quantification back", remove or rephrase the stuff about `(~~)`; perhaps
 use the ''data type'' `:~~:` rather than the ''class'' `(~~)`.

 * Promote "Another approach" for the class `(~~)` which appears lower
 down. It may be another approach but it is Our Plan for solving a Real
 Problem in introducing homogeneous equality at the moment, and as time
 goes on it is really helpful to know what The Plan is, with other
 approaches being discussed later.

 TL;DR: make the page reflect our current thinking as directly as possible.

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