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