Wow, I didn't seriously expect it was a real bug. This is my first time finding a confirmed compiler bug. Thanks for the response!
On Wed, Aug 18, 2010 at 2:49 AM, Simon Peyton-Jones <simo...@microsoft.com> wrote: > | {-# 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 > > -- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer) _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users