confusing GADT/scoped type variables behaviour

22 Oct 2007

      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

confusing GADT/scoped type variables behaviour

Ganesh Sittampalam