#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