Strange and incorrect type error when using rewrite rules with type families
The following code
{-# OPTIONS_GHC -fglasgow-exts -O1 #-}
module Main where
{-# RULES "rule1" forall x. to (from x) = x #-}
{-# RULES "rule2" forall x. from (to x) = x #-}
class EP a where
type Result a
from :: a -> Result a
to :: Result a -> a
gives the compilation error with GHC 6.11.20090703:
Couldn't match expected type `Result a'
against inferred type `Result a'
NB: `Result' is a type function, and may not be injective
In the first argument of `to', namely `(from x)'
In the expression: to (from x)
When checking the transformation rule "rule1"
I don't understand this error. rule2 seems unproblematic, though.
The similar code with functional dependencies
{-# RULES "rule3" forall x. to' (from' x) = x #-}
{-# RULES "rule4" forall x. from' (to' x) = x #-}
class EP' a b | a -> b where
from' :: a -> b
to' :: b -> a
raises no errors.
Trac metadata
| Trac field | Value |
|---|---|
| Version | 6.11 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |