#2040: GADT regression
-------------------------------------+--------------------------------------
Reporter: guest | Owner: chak
Type: bug | Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler (Type checker) | Version: 6.8.2
Severity: normal | Resolution:
Keywords: gadt | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-------------------------------------+--------------------------------------
Changes (by simonpj):
* owner: => chak
* difficulty: => Unknown
* milestone: => 6.10 branch
Comment:
Thanks for a good report.
Having looked at the code, I think it's quite surprising that 6.8.1 worked
at all. Just for the record (I don't expect users to understand this
bit), the problem is this. Here's a smaller version of the code,
decorated with constraints:
{{{
foo2 :: W (S ()) -> W (S ()) -> ()
foo2 (W (_ :: W a1)) -- C a1 b1, S () ~ S b1
(W (_ :: W a2)) -- C a2 b2, S () ~ S b2
=
case {-# Needs C a1 (S ()) #-}
proof :: Teq a1 (S ()) of
Teq -> {-# Provides a1~S () #-}
{-# Needs: C a2 (S ()) #-}
(proof :: Teq a2 (S ()))
`seq` ()
}}}
The inner use of `proof` gives rise to a constraint `(C a2 (S ()))`. This
is wrapped in an implication constraint because of the enclosing case
expression. But the `tci_reft` of that implication constraint does not
include the type refinements from the enclosing pattern matches. So when
`reduceImplication` makes that the current type refinement, we're missing
the outer refinements.
This is a clear bug in 6.8.2, since there is no use of type functions. It
would in principle be fixable in 6.8.3, but it's not completely trivial to
do, so I'm disinclined to attempt it since we are rejigging the whole
machinery for the HEAD.
Meanwhile the HEAD falls over (which it should not) because the constraint
simplifier is not deducing all the things it should. This is Manuel's
pigeon at the moment, so I'm assigning the bug to him. In due course this
program should join the test suite.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2040#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
