[GHC] #9291: Don't reconstruct sum types if the type subtly changes

[GHC]

#9291: Don't reconstruct sum types if the type subtly changes
----------------------------+----------------------------------------------
        Reporter:  schyler  |            Owner:
            Type:  feature  |           Status:  new
  request                   |        Milestone:
        Priority:  normal   |          Version:  7.8.2
       Component:           |         Keywords:
  Compiler                  |     Architecture:  Unknown/Multiple
      Resolution:           |       Difficulty:  Moderate (less than a day)
Operating System:           |       Blocked By:
  Unknown/Multiple          |  Related Tickets:
 Type of failure:           |
  None/Unknown              |
       Test Case:           |
        Blocking:           |
----------------------------+----------------------------------------------

Comment (by goldfire):

 The way that we have proved Haskell's type system safe is precisely
 because Core is proved safe. Haskell itself, from a formal standpoint, is
 defined solely by its transformation into Core. If the compiler used
 `unsafeCoerce` internally, then any claims of safety would be bogus.

 What is seems you're asking for is a strange new beast in Core...
 something of a dependently-typed coercion, that requires a proof that the
 term it is coercing is built with the constructors whose type is not
 changing. I don't think this is impossible, but I don't envy the person
 that does the proof!

 This is somewhat disappointing, because I agree that it would be great to
 have this optimization! Perhaps others see the theory differently...

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