confusing GADT/scoped type variables behaviour

[Ian Lynagh]

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#pattern-type-sigs

    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