id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
1823,GADTs and scoped type variables don't work right,simonpj,chak,"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.  ",bug,closed,normal,6.10 branch,Compiler (Type checker),6.8.1,fixed,,ganesh@…,Unknown/Multiple,Unknown/Multiple,,Unknown,gadt/scoped.hs,,,