Redundant signature required with RULES and GADTs

Here is a small program:

data T a where TInt :: T Int

foo :: T Int -> Int
foo TInt = 0

{-# RULES "foo"  forall x. foo x = case x of { TInt -> 0 } #-}

GHC complains:

    GADT pattern match with non-rigid result type `t'
      Solution: add a type signature for the entire case expression
    In a case alternative: TInt -> 0
    In the expression: case x of { TInt -> 0 }
    When checking the transformation rule "foo"

And indeed, changing the rule to

{-# RULES "foo"  forall x. foo x = case x of { TInt -> 0 } :: Int #-}

works. The signature is redundant, though, because the type of the case is determined by the type of the rule head.

Trac metadata

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