| {-# 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