[GHC] #15248: Coercions from plugins cannot be stopped from floating out

[GHC]

#15248: Coercions from plugins cannot be stopped from floating out
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       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):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by adamgundry):

 * cc: adamgundry (added)


Comment:

 In this case, in principle, shouldn't the evidence produced for the plugin
 directly depend on the evidence for the assumptions? That is, rather than
 "proving" `(a <? c) ~ True` by `UnivCo`, you would "prove"

 {{{
   (((a <? b) ~ True, (b <? c) ~ True) => a <? c)
 ~ (((a <? b) ~ True, (b <? c) ~ True) => True)
 }}}

 by `UnivCo` and then instantiate it with your evidence for `(a <? b) ~
 True` and `(b <? c) ~ True`.

 That said, your suggestion might make things easier in practice...

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