Possible bug with GADTs?

[Simon Peyton-Jones]

| {-# LANGUAGE GADTs #-}
| module Foo where
| 
| data TemplateValue t where
|   TemplateList :: [x] -> TemplateValue [x]
|
| instance (Eq b) => Eq (TemplateValue b) where
|     (==) (TemplateList p) (TemplateList q) = (==) p q

A good example.  Yes, GHC 6.12 fails on this and will always fail because its type checker is inadequate.  I'm hard at work [today] on the new typechecker, which compiles it just fine.

Here's the reasoning (I have done a bit of renaming).

* The TemplateList constructor really has type
	TemplateList :: forall a. forall x. (a~[x]) => [x] -> TemplateValue a

* So in the pattern match we have
	(Eq b) available from the instance header
	TemplateList p :: TemplateValue b
	x is a skolem, existentially bound by the pattern
	p :: [x]
	b ~ [x] available from the pattern match

* On the RHS we find we need (Eq [x]).

* So the constraint problem we have is
	(Eq b, b~[x]) => Eq [x]
          ["Given"  =>  "Wanted"]
  Can we prove this?  From the two given constraints we can see
  that we also have Eq [x], and that certainly proves Eq [x].


Nevertheless, it's a bit delicate.  If we didn't notice all the 
consequences of the "given" constraints, we might use the 
top-level Eq a => Eq [a] instance to solve the wanted Eq [x].
And now we need Eq x, which *isn't* a consequence of (Eq b, b~[x]).


Still, there is a unique proof, and GHC (now) finds it.  It'll all
be in 6.16.

Simon