GHC 6.6 GADT type unification vs GHC 6.8

Hello, I was wresting with the problem of converting our type witness code in darcs to work with ghc 6.8 and it occurred to me that someone has probably document the change somewhere. In particular, I'm seeing this error message a lot, but 6.6 doesn't give this message: GADT pattern match in non-rigid context for `NilRL' Tell GHC HQ if you'd like this to unify the context The main difference I have observed is that 6.6 infers types in case statements fully, but 6.8 seems to skip them and expects type signatures. Sometimes I'm at a loss to figure out where to add the type signature to satisfy 6.8 and the process becomes tedious and time consuming. I'm using 6.8.2 and I did see this thread: http://www.haskell.org/pipermail/glasgow-haskell-users/2007-December/013952.... What version of GHC do I need to see the improved diagnostics mentioned in that thread? Will the GADT unification in 6.10 be compatible with 6.6? If so, maybe I shouldn't convert the code to work for 6.8. Also, can someone point me to a discussion of the difference or a paper about it? Thanks, Jason

GHC 6.6 was a bit more generous than GHC 6.8, but erroneously so. Specifically, GHC 6.8 and all subsequent versions require that when you pattern match on a value of GADT type, * the type of the scrutinee * the type of the result of the case * the types of any free variables used inside the case alternatives are all completely known ("rigid" in GHC's terminology) at the case expression. The easiest way to make a variable have a rigid type is to give it a type signature. I don't expect to revert to GHC 6.6's behaviour because I don't know how to do (robust, complete) type inference for that. I'll add these remarks to the user manual. Simon From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Jason Dagit Sent: 21 July 2008 20:44 To: glasgow-haskell-users@haskell.org Subject: GHC 6.6 GADT type unification vs GHC 6.8 Hello, I was wresting with the problem of converting our type witness code in darcs to work with ghc 6.8 and it occurred to me that someone has probably document the change somewhere. In particular, I'm seeing this error message a lot, but 6.6 doesn't give this message: GADT pattern match in non-rigid context for `NilRL' Tell GHC HQ if you'd like this to unify the context The main difference I have observed is that 6.6 infers types in case statements fully, but 6.8 seems to skip them and expects type signatures. Sometimes I'm at a loss to figure out where to add the type signature to satisfy 6.8 and the process becomes tedious and time consuming. I'm using 6.8.2 and I did see this thread: http://www.haskell.org/pipermail/glasgow-haskell-users/2007-December/013952.... What version of GHC do I need to see the improved diagnostics mentioned in that thread? Will the GADT unification in 6.10 be compatible with 6.6? If so, maybe I shouldn't convert the code to work for 6.8. Also, can someone point me to a discussion of the difference or a paper about it? Thanks, Jason

On Tue, Jul 29, 2008 at 1:07 AM, Simon Peyton-Jones
GHC 6.6 was a bit more generous than GHC 6.8, but erroneously so. Specifically, GHC 6.8 and all subsequent versions require that when you pattern match on a value of GADT type,
· the type of the scrutinee
· the type of the result of the case
· the types of any free variables used inside the case alternatives
are all completely known ("rigid" in GHC's terminology) at the case expression.
Thanks, this makes sense and helps. Is this described in the wobbly types paper, or is paper covering a different topics? I would like to have a cite-able reference.
The easiest way to make a variable have a rigid type is to give it a type signature.
I don't expect to revert to GHC 6.6's behaviour because I don't know how to do (robust, complete) type inference for that.
In that case, good thing I finally figured out what changes to make to darcs so that our type witness code compiles in both 6.6 and 6.8. My changes match what you describe.
I'll add these remarks to the user manual.
Great! Thanks, Jason

Thanks, this makes sense and helps. Is this described in the wobbly types paper, or is paper covering a different topics? I would like to have a cite-able reference.
Excellent question. I believe that what I describe below is a restriction of the system described in the POPL'06 paper
http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf
At this moment I can't remember when we changed to the additional restrictions below. I think the reason was that we wanted to avoid the complexity of "fresh" mgus described in the paper, but memory is failing me. Dimitrios or Stephanie may have a better memory.
Simon
From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users-bounces@haskell.org] On Behalf Of Jason Dagit
Sent: 29 July 2008 15:14
To: Simon Peyton-Jones
Cc: glasgow-haskell-users@haskell.org
Subject: Re: GHC 6.6 GADT type unification vs GHC 6.8
On Tue, Jul 29, 2008 at 1:07 AM, Simon Peyton-Jones

On Tue, Jul 29, 2008 at 7:40 AM, Simon Peyton-Jones
Thanks, this makes sense and helps. Is this described in the wobbly types paper, or is paper covering a different topics? I would like to have a cite-able reference.
Excellent question. I believe that what I describe below is a * restriction* of the system described in the POPL'06 paper
http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf
At this moment I can't remember when we changed to the additional restrictions below. I think the reason was that we wanted to avoid the complexity of "fresh" mgus described in the paper, but memory is failing me. Dimitrios or Stephanie may have a better memory.
Thank you. I'm reading it now, and I believe it will work just perfect for my needs. Thanks, Jason
participants (2)
-
Jason Dagit
-
Simon Peyton-Jones