confusing GADT/scoped type variables behaviour

[Simon Peyton-Jones]

Ganesh

Sorry to be slow on this.  Thanks for the bug report.

| 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
| So, is there a good explanation of the errors from 6.8? Is 6.8 behaving
| as expected?

This is a definite bug in 6.8, in the interaction of GADTs and scoped type variables.  I know exactly why it happens, but probably won't fix it because it'll fall out naturally of the work we (mainly Manuel) are doing to fully implement type equalities.

I've added http://hackage.haskell.org/trac/ghc/ticket/1823, which gives an even smaller test case.

| 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?

I'm quite surprised 6.6 works:

| f :: forall x y . D x y -> ()
| f (D (C p))
|   | P q <- (\p@(P a) -> p) p
|    = case q of

The fact that q has a rigid type is quite complicated to figure out.  Did you really need that lambda?

Meanwhile Ian asks:

| Although this program is the one that finally worked in both 6.6 and
| 6.8, I don't understand why it worked in either: y is not an
| existentially quantified variable, so shouldn't be allowed to be
| introduced by a type signature there based on my reading of the user
| guide.

The user guide is at fault.  You can bind a type variable with a pattern type signature if type of the pattern is "rigid".  (With GADTs the idea of "existential" becomes fuzzier.)  So this defn is a bit more generous than before.  I've updated the manual.   See the GADT wobbly-type paper for a description of rigidity.

Simon