| {-# 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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
