GADT related bug in GHC type checker

[Daniel Fischer]

On Wednesday 14 July 2010 00:11:00, George Giorgidze wrote:
> Hi,
>
> I have encountered a bug in GHC type checker. I have stripped down my
> code to small manageable example that illustrates the bug:
>
> {-# LANGUAGE GADTs #-}
> {-# OPTIONS -Wall #-}
>
> module StrangeGADT where
>
> data Q a where
>   ToQ :: (QA a) => a -> Q a
>   Sum :: (QA a, Num a) => Q [a] -> Q a
>
> class QA a where
>   toQ :: a -> Q a
>   fromQ :: Q a -> a
>
> instance QA Int where
>   toQ = ToQ
>   fromQ q = case q of
>              ToQ a -> a
>              Sum as -> sum (fromQ as)
>
> instance QA a => QA [a] where
>   toQ = ToQ
>   fromQ q = case q of
>              ToQ a -> a
>              -- Sum _ -> ([] + 13)
>
> The above program typechecks but GHC wrongly warns that last pattern
> match is not exhaustive.

That warning is correct. Uncommenting the Sum case:

*StrangeGADT> fromQ (Sum $ ToQ [[1 :: Int .. 10]])
[]

Of course, to make it work, I needed

instance (Num a) => Num [a] where
    (+) = zipWith (+)
<and so on>
    fromInteger = repeat . fromInteger

But since that instance is possible, both constructors can appear as 
arguments to fromQ for the list instance, hence the warning.

>
> Furthermore, if I uncomment the last line of the code it typechecks
> (without warnings) and does not reject ([] + 13) as type incorrect
> expression.

It's type correct:

Prelude> :t [] + 13
[] + 13 :: (Num [a]) => [a]

It's usable only when a Num instance for a list is in scope, though.

>
> It would be very much appreciated if someone could suggest how to
> circumvent the problem.

For the code you posted, there is no problem to circumvent. GHC behaves 
correctly since it works on an open world assumption, it doesn't rely on 
the instances in scope but takes other possible instances into account.

>
> Is there a version of GHC that behaves correctly in this case?
>
> Is this yet another instance of GADT related bugs already reported in
> GHC trac? or it is unrelated and I better report it as a separate
> ticket.
>
> Cheers, George
>