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 |