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. Furthermore, if I uncomment the last line of the code it typechecks (without warnings) and does not reject ([] + 13) as type incorrect expression. It would be very much appreciated if someone could suggest how to circumvent the problem. 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