#1823: GADTs and scoped type variables don't work right
----------------------------------------+-----------------------------------
Reporter: simonpj | Owner: chak
Type: bug | Status: new
Priority: normal | Milestone: 6.10 branch
Component: Compiler (Type checker) | Version: 6.8.1
Severity: normal | Keywords:
Difficulty: Unknown | Testcase: gadt/scoped.hs
Architecture: Unknown | Os: Unknown
----------------------------------------+-----------------------------------
In this program, which is also in the testsuite as `gadt/scoped.hs`, all
three definitions of g should work
{{{
{-# OPTIONS_GHC -XGADTs -XScopedTypeVariables -XPatternSignatures #-}
module GADT where
data C x y where
C :: a -> C a a
data D x y where
D :: C b c -> D a c
------- All these should be ok
-- Rejected!
g1 :: forall x y . C x y -> ()
-- C (..) :: C x y
-- Inside match on C, x=y
g1 (C (p :: y)) = ()
-- OK!
g2 :: forall x y . C x y -> ()
-- C (..) :: C x y
-- Inside match on C, x=y
g2 (C (p :: x)) = ()
-- Rejected!
g3 :: forall x y . D x y -> ()
-- D (..) :: D x y
-- C (..) :: C sk y
-- sk = y
-- p :: sk
g3 (D (C (p :: y))) = ()
}}}
But they don't. The reason is that the "refinement" is applied to the
environment only after checking an entire pattern; but the refinement is
needed during checking the pattern if scoped type variables are to work
right.
I don't propose to fix this, because it'll come out in the wash when we
get rid of type refinements in favour of equality constraints.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1823>
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
