Instance inference failure with GADTs

Consider the following code:

{-# LANGUAGE GADTs, FlexibleInstances #-}

class Stringable a where
  toString :: a -> String

data GADT a where
  GInt :: GADT Int
  GBool :: GADT Bool

instance Stringable (GADT Int) where
  toString _ = "constructor GInt"
instance Stringable (GADT Bool) where
  toString _ = "constructor GBool"

mkString :: GADT a -> String
mkString g = toString g

mkString' :: GADT a -> String
mkString' g = case g of
  GInt  -> toString g
  GBool -> toString g

The function mkString does not compile, while the function mkString' does. The problem seems to be that there is no instance declaration for GADT a, although there are instances for all the possible instantiations of a. It seems that requiring a case statement where all patterns are accounted for and all branches contain the same expression should be unnecessary.

This was tested on 7.5.20120426.

Trac metadata

Trac field	Value
Version	7.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture