Possible bug with GADTs?

[Dan Knapp]

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
<simonpj at 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)