[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 rwbarton):

 I think the lens package uses this pattern extensively, or at least
 something closely related.

 In discussion with "napping" on IRC the idea arose to extend Core-level
 `case` with the power to generalize the type of its scrutinee. For
 example, if `x :: Either Int String`, then (using a syntax inspired by as-
 patterns, and omitting some noisy details)
 {{{
 case x of _ {
   xLeft@(Left int) -> {- here xLeft :: Either Int b (we don't use it) -}
     Left @ String @ String (show @ Int int)
   xRight@(Right str) -> {- here xRight :: Either a String -}
     xRight @ String
 }
 }}}

 The appropriate amount of type generalization would depend on the type
 variables that appear in the fields of the constructor that was matched,
 after translating GADT constructors into type equality constraints. For
 example given the type `data X a b where MkX :: b -> X Int b`, if we match
 `x :: X Int Char` with `MkX Char`, we cannot generalize the type of `x` to
 `X a Char`, since the translated type of `MkX` is `MkX :: (a ~ Int) => b
 -> X a b` which does mention `a` on the left-hand side (in a constraint).
 This is all rather similar to role inference for data types, I imagine,
 except done on a per-constructor basis.

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