[GHC] #9117: Coercible constraint solver misses one

[GHC]

#9117: Coercible constraint solver misses one
-------------------------------------+------------------------------------
        Reporter:  goldfire          |            Owner:  nomeata
            Type:  bug               |           Status:  new
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:                    |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by goldfire):

 It strikes me that what we have here is a nice little programming-
 languages problem that would probably submit to standard techniques.
 Specifically, we have a specification of what things are coercible -- the
 typing rules for representational coercions -- and an algorithm for
 checking whether two things are coercible. The algorithm is
 straightforward and could be formalized beyond its Haskell implementation.
 Then, we could verify if the algorithm is sound and/or complete w.r.t. the
 specification. If it's not sound, we have the possibility of a Core Lint
 error. If it's not complete, we have the possibility of failing
 inappropriately.

 To be clear, I'm not quite volunteering to do this tonight or saying that
 it's an essential step, but it might be a nice thing to try if we want to
 understand this better.

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