Types in RULES

[Manuel M T Chakravarty]

Simon Peyton-Jones:
> [Widening to cvs-ghc; read Roman's message below first.]
>
> Roman
>
> How annoying. You're right, it's impossible, because the 't' isn't  
> mentioned in the type of 'f', or 'x'.
>
> What would we like to write?  Perhaps something like
>
> "myrule" forall (type t :: *->*) (f :: a->a) x.
>     from (tmap f (to x :: t a)) = map f (from (to x :: t a))
>
> We need a syntactic clue to distinguish the *type* binders in the  
> forall from the *term* binders.  Saying "the signature mentions "*"  
> seems a bit flaky to me.  My suggestion above is to re-use the  
> keyword 'type'.
>
> What do you think?  Manuel may have an opinion too.

I agree.  That seems to be the best option.

Manuel