The issue is different here. You are *lazily* matching the pattern, so it'd be
unsound in general to accept this. Same thing if you said
fstTy ~(a :-> b) = a
Now in this case the RHS is strict in 'a' so it's probably ok but it's not in
general. Nothing to do with rigidity. The error message is bad though
S
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Conal Elliott
Sent: 22 August 2007 23:34
To: Simon Peyton-Jones
Cc: [email protected]
Subject: Re: ghc 6.7 and GADT pattern-matching
How about this one (relative to same Ty def)?
fstTy :: Ty (a -> b) -> Ty a
fstTy (a :-> b) = a
fstTy' :: Ty (a -> b) -> Ty a
fstTy' ty = a where (a :-> b) = ty
The first definition works, while the second triggers the complaint about
non-rigidity. I don't know how to type-annotate the second one to provide
the required rigidity. Do you?
Of course, in this example, I can use the first def instead of the second. In
my real example, the type being deconstructed is synthesized, so the second
form is not so convenient.
I'm working around this problem, so no emergency, but still I'd like to know
what can be done.
Thanks, - Conal
On 8/22/07, Simon Peyton-Jones <[EMAIL PROTECTED]<mailto:[EMAIL PROTECTED]>>
wrote:
The issue is this. When doing GADT matching, getting type inference to work
well, and interact well with other features (e.g. indexed type families) is
MUCH easier if the type being matched is totally known - we say "rigid". When
you used "$" you made GHC less sure about the type of the GADT match. Our
GADT paper describes this rigidity reasoning
http://research.microsoft.com/~simonpj/papers/gadt/index.htm
<http://research.microsoft.com/%7Esimonpj/papers/gadt/index.htm>
GHC 6.6 was a bit more liberal, but the liberality was delicately balanced, and
made life too complicated when we added more stuff.
In any case, the solution is always "add a type signature", though in this case
you could also escape with "omit a $".
Simon
From: [EMAIL PROTECTED]<mailto:[EMAIL PROTECTED]> [mailto:[EMAIL
PROTECTED]<mailto:[EMAIL PROTECTED]>] On Behalf Of Conal Elliott
Sent: 22 August 2007 06:15
To: [email protected]<mailto:[email protected]>
Subject: ghc 6.7 and GADT pattern-matching
In going from ghc-6.6 to ghc-6.7, I've lost some GADT pattern matching that I'd
really like to have back. The message:
c:/conal/Haskell/Eros/src/gadt-example.hs :23:32:
GADT pattern match in non-rigid context for `:*'
Tell GHC HQ if you'd like this to unify the context
In the pattern: a :* b
In a lambda abstraction: \ (a :* b) -> ((f a) :* b)
In the second argument of `($)', namely
`\ (a :* b) -> ((f a) :* b)'
and the relevant code:
-- | Statically typed type representations
data Ty :: * -> * where
(:*) :: Ty a -> Ty b -> Ty (a, b)
(:->) :: Ty a -> Ty b -> Ty (a->b)
OtherTy :: TypeRep -> Ty a
-- | Type transformations
newtype TyFun a b = TyFun { unTyFun :: Ty a -> Ty b }
instance Arrow TyFun where
TyFun f >>> TyFun g = TyFun (f >>> g)
first (TyFun f) = TyFun $ \ (a :* b) -> (f a :* b)
second (TyFun g) = TyFun $ \ (a :* b) -> (a :* g b)
Full test module attached with many more example matchings.
I'd really like to get this code working in ghc-6.7. How likely is that? The
best alternative I know is *much* less readable.
Thanks, - Conal
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
