[GHC] #8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!)

[GHC]

#8423: contraint solver doesn't  reduce reducible closed type family expressions
(even with undecidable instances!)
--------------------------------------------+------------------------------
        Reporter:  carter                   |            Owner:
            Type:  feature request          |           Status:  new
        Priority:  normal                   |        Milestone:  7.10.1
       Component:  Compiler (Type checker)  |          Version:  7.7
      Resolution:                           |         Keywords:
Operating System:  Unknown/Multiple         |     Architecture:
 Type of failure:  None/Unknown             |  Unknown/Multiple
       Test Case:                           |       Difficulty:  Unknown
        Blocking:                           |       Blocked By:
                                            |  Related Tickets:  #4259
--------------------------------------------+------------------------------

Comment (by goldfire):

 If you just want a way to check things, please see
 [https://gist.github.com/goldfirere/6902431 here]. The key step is that
 you do in fact have to write proofs! These proofs may, sadly, have runtime
 significance. But, from the optimization results in the "Deferred type
 errors" [http://research.microsoft.com/en-
 us/um/people/simonpj/papers/ext-f/icfp12.pdf paper] lead me to wonder if
 these runtime traces are optimized away. (I haven't checked -- doing so is
 beyond the scope of my morning Haskell stretches.) I did check, though,
 that the inliner will remove calls to `gcoerce` and make `go` properly
 tail-recursive (ignoring the type-cast, which I know is removed at
 runtime).

 Thanks for posting this! It's made me realize that `gcoerce` from that
 example should probably be in the Data.Type.Equality module anyway.

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