#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