confusing GADT/scoped type variables behaviour
Hi, I'm having some trouble writing code that uses GADTs. I finally got something that is portable between GHC 6.6 and 6.8, but I don't really understand what's going on, and I'm a bit unhappy with the number of type signatures required. I'll explain them with a series of cut-down examples below, so please forgive the gratuitous beta-redexes. My testing has been with GHC 6.6 and 6.8.0.20070921, but I believe from more limited testing that 6.6.1 behaves the same as 6.6. My first program works fine with both GHC 6.6 and 6.8: {-# 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 :: forall x y . D x y -> () f (D (C p)) | P q <- (\p -> p) p = case q of Q -> () {- end of program -} However, when I change it slightly to make the lambda expression inspect the structure of p: {-# 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 :: forall x y . D x y -> () f (D (C p)) | P q <- (\p@(P a) -> p) p = case q of Q -> () {- end of program -} it continues to work with 6.6, but 6.8 complains that q has a wobbly type and I should add a type annotation. So, I do so, also adding one to the original pattern for p otherwise my type variables aren't in scope: {-# 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 :: forall x y . D x y -> () f (D (C (p :: P w z))) | P q :: P w z <- (\p@(P a) -> p) p = case q of Q -> () {- end of program -} Fine with 6.8, but now 6.6 is unhappy. The type variable 'w' is actually the same as 'y', and 6.6 seems to have noticed this fact and says I should have given them the same name. So, I do so: {-# 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 :: forall x y . D x y -> () f (D (C (p :: P y z))) | P q :: P y z <- (\p@(P a) -> p) p = case q of Q -> () {- end of program -} Now 6.6 is happy. But 6.8 doesn't believe they are the same, and rejects it. I finally got it to work with both by removing the forall in the signature of f: {-# 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 -> () {- end of program -} But, I don't really understand why this is so. I guess the 'y' in the outer signature is no longer a scoped type variable, so 6.6 doesn't complain, and is no longer the same as the inner 'y', so 6.8 doesn't complain, but it all feels a bit unsatisfactory. So, is there a good explanation of the errors from 6.8? Is 6.8 behaving as expected? Finally, ideally I'd like not to have any type signatures in the body of f - is this feasible with 6.8 like it was with 6.6? Cheers, Ganesh
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
Ganesh Sorry to be slow on this. Thanks for the bug report. | Now 6.6 is happy. But 6.8 doesn't believe they are the same, and rejects | it. I finally got it to work with both by removing the forall in the | So, is there a good explanation of the errors from 6.8? Is 6.8 behaving | as expected? This is a definite bug in 6.8, in the interaction of GADTs and scoped type variables. I know exactly why it happens, but probably won't fix it because it'll fall out naturally of the work we (mainly Manuel) are doing to fully implement type equalities. I've added http://hackage.haskell.org/trac/ghc/ticket/1823, which gives an even smaller test case. | Finally, ideally I'd like not to have any type signatures in the body of f | - is this feasible with 6.8 like it was with 6.6? I'm quite surprised 6.6 works: | f :: forall x y . D x y -> () | f (D (C p)) | | P q <- (\p@(P a) -> p) p | = case q of The fact that q has a rigid type is quite complicated to figure out. Did you really need that lambda? Meanwhile Ian asks: | 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. The user guide is at fault. You can bind a type variable with a pattern type signature if type of the pattern is "rigid". (With GADTs the idea of "existential" becomes fuzzier.) So this defn is a bit more generous than before. I've updated the manual. See the GADT wobbly-type paper for a description of rigidity. Simon
participants (3)
-
Ganesh Sittampalam -
Ian Lynagh -
Simon Peyton-Jones