confusing GADT/scoped type variables behaviour
Ian Lynagh
igloo at earth.li
Mon Oct 22 20:23:56 EDT 2007
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
More information about the Glasgow-haskell-users
mailing list