#2206: GADT pattern match with non-rigid return type
--------------------------+-------------------------------------------------
Reporter: simonpj | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.8.2
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: gadt-escape1 | Architecture: Unknown
Os: Unknown |
--------------------------+-------------------------------------------------
Comment (by chak):
The implementation of GADTs in the development version of GHC recently
changed completely. It's now based on a combination of implication
constraints and type equality constraints. I believe what happens is the
following. In the case alternative, we have `a :: ExpGADT t` together
with an equality constraint `t ~ Int`. So, GHC is right to claim that `t`
escapes its scope; it does albeit escape in conjunction with the equality
`t ~ Int`.
At the moment, GHC does not properly enforce the constraints on type
rigidity, but in the course of investigating the interaction between GADTs
and type families, we came to the conclusion that we need to require not
only that the type of the scrutinee of a GADT match is rigid, but '''also
its return type'''. Hence, the example code should indeed be rejected,
but ideally the error message should point out that the return type should
be rigid (instead of the somewhat unhelpful message produced currently).
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2206#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
