GADT related bug in GHC type checker

[George Giorgidze]

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