Bind type variables in RULES

Roman writes: here's an example I came across while working on the recycling paper and which I subsequently forgot about. Suppose we have:

{-# LANGUAGE Rank2Types #-}
module T where

class T t where
   to   :: [a] -> t a
   from :: t a -> [a]
   tmap :: (a -> a) -> t a -> t a

{-# RULES

"myrule" forall f x.
     from (tmap f (to x)) = map f (from (to x))
  #-}

Alas, this fails with:

     Ambiguous type variable `t' in the constraint:
       `T t' arising from a use of `to' at T.hs:12:40-43
     Probable fix: add a type signature that fixes these type variable(s)

Of course, I'd like the t on the rhs to be the same as on the lhs but I don't see how to tell this to GHC. Is it actually possible? The only solution I've found was to add a dummy argument to 'to':

to' :: t a -> [a] -> t a

to = to' undefined

{-# RULES

"myrule" forall f t x.
     from (tmap f (to' t x)) = map f (from (to' t x))
  #-}

That's ugly, of course. Am I missing something or is this just impossible to do with the current system?

Trac metadata

Trac field	Value
Version	6.8.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Unknown
Architecture	Unknown