GADT and explicit forall on ghc 7.8.2

3
votes

I'm playing with GADTs and explicit forall on ghc 7.8.2. Let's look at the following simple example:

{-# LANGUAGE GADTs, RankNTypes #-}

data T1 a where
   T1 :: (b -> a) -> b -> T1 a

data T2 a where
   T2 :: forall b. (b -> a) -> b -> T2 a

Here ghc fails with:

Test.hs:7:26: Not in scope: type variable ‘a’
Test.hs:7:35: Not in scope: type variable ‘a’

When T2 is commented out type checking succeeds. But T1 and T2 are seemingly equivalent. Is this a bug in ghc or some limitation of GADTs? If the latter then what is the difference between the two?

2
haskellghcexistential-typegadt
I think this is just about quantification. The compiler probably has some rule that you either use explicit or implicit quantification, not a mixture of both. – luqui
BTW, the a in data T2 a does not extend down to the constructors; it's irrelevant what it's named. – luqui
@luqui That's weird. Is there a reason why would a be in scope for T1 but not in scope for T2? I just fail to see why explicit quantification should shadow it. – projedi
@projedi, because T1 is using implicit quantification (all variables implicitly forall'd), and T2 is using explicit quantification (and you didn't quantify a) – luqui
@luqui Ah, I see. So a in T1 is not binded at data T1 a but implicitly at T1 constructor. Thanks! – projedi

2 Answers

4
votes

I originally assumed that a in T1 constructor was binded at data T1 a declaration. But it actually is implicitly quantified in a constructor itself. Therefore T2 constructor is wrong because it explicitly quantifies b and doesn't quantify a.

0
votes

I was struggling with a similar problem. Based on chi's comment, I came up with this solution:

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data T2 :: * -> * where
   T2 :: forall a b. (b -> a) -> b -> T2 a

I would rather have preferred the b to stand out in comparison to the a, but I guess this is still better than an implicit forall for those who prefer it explicit, which includes myself.