On Mon, Oct 22, 2007 at 09:46:39PM +0100, Ganesh Sittampalam wrote:
{-# OPTIONS_GHC -fglasgow-exts #-} module GADT where
data C x y where C :: P x y -> C x x
data P x y where P :: Q x y -> P x y
data Q x y where Q :: Q x y
data D x y where D :: C y z -> D x z
f :: D x y -> () f (D (C (p :: P y z))) | P q :: P y z <- (\p@(P a) -> p) p = case q of Q -> ()
Although this program is the one that finally worked in both 6.6 and 6.8, I don't understand why it worked in either: y is not an existentially quantified variable, so shouldn't be allowed to be introduced by a type signature there based on my reading of the user guide. Here's a simpler example: f :: a -> a f (x :: b) = x and here's the bit of the user guide that's confusing me (in all of the 6.6.1 release, 6.8 and HEAD branches): http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html... There is only one situation in which you can write a pattern type signature that mentions a type variable that is not already in scope, namely in pattern match of an existential data constructor. In the simpler program above 'b' is not in scope, so I would expect the program to be rejected, but "ghc-6.6.1 -fglasgow-exts" and "ghc-6.8 -XPatternSignatures -XScopedTypeVariables" both accept the program. "ghc-6.8 -XPatternSignatures" rejects it with z.hs:3:8: Not in scope: type variable `b' which also doesn't really make sense to me. I'm not sure if this is a bug in the compiler, or if I'm just reading the docs wrong? Thanks Ian