Strange and incorrect type error when using rewrite rules with type families

[dreixel]

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.

[simonpj]

You are right, that is bogus. Fixed by

Fri Jul 17 16:57:22 BST 2009  simonpj@microsoft.com
  * Fix Trac #3346: tcSimplify for LHS of RULES with type equalities

    M ./compiler/typecheck/TcSimplify.lhs -2 +12

There was special handling for constraints on the LHS of a RULE, which hadn't been updated to account for type families.

Thanks for the report. I've added a regression test

Simon