Redundant signature required with RULES and GADTs

[rl]

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.

[simonpj]

Ha, well at least the error message was on target.

This'll be fixed when we switch to the  OutsideIn algorithm for inference.

Simon

[simonpj]

Indeed it is fixed. Regression test added

Simon