[GHC] #15497: Coercion Quantification

[GHC]

#15497: Coercion Quantification
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:
      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:D5054
       Wiki Page:                    |
  https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2|
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * owner:  ningning => (none)
 * status:  closed => new
 * resolution:  fixed =>


Comment:

 I came across `Note [Emitting the residual implication in simplifyInfer]`
 in `TcSimplify`.
 It says “We can't form types like (forall co. blah), so we can't
 generalise over the coercion variable, …”

 But when you commit coercion quantification, we ''can'' quantify over
 coercions in types.  So it is possible that this bit of cruft could be
 tidied up, with a significant simplification.

 I'll re-open the ticket to keep this idea on the radar.

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