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 <simonpj@microsoft.com> wrote:

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