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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
