Opened 9 years ago

Last modified 4 months ago

#2600 new feature request

Bind type variables in RULES

Reported by: simonpj Owned by: simonpj
Priority: lowest Milestone:
Component: Compiler Version: 6.8.3
Keywords: Cc: pho@…, mail@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #2110 Differential Rev(s):
Wiki Page:

Description

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?

Attachments (1)

T2600.hs (225 bytes) - added by morabbin 5 years ago.
Exhibits issue described in #2600

Download all attachments as: .zip

Change History (24)

comment:1 Changed 9 years ago by simonpj

Owner: set to simonpj

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.

Incidentally, once the rule is parsed and typechecked, the simplifier will have no trouble doing the right thing.

comment:2 Changed 9 years ago by simonpj

One other syntactic question: what if there are multiple type binders? We could say

  forall (type a :: *) (type b :: *) (f :: a->b).   <blah>

or perhaps just one type keyword to introduce all type binders? But then you'd need something to say when the type binders stopped. A semicolon perhaps?

  forall type (a :: *) (b :: *); (f :: a->b).   <blah>

More syntactic suggestions welcome. Once we have the syntax, the implementation should not be hard.

Simon

comment:3 Changed 9 years ago by igloo

Milestone: 6.12 branch

comment:4 Changed 9 years ago by simonmar

Architecture: UnknownUnknown/Multiple

comment:5 Changed 9 years ago by simonmar

Operating System: UnknownUnknown/Multiple

comment:6 Changed 9 years ago by PHO

Cc: pho@… added

comment:7 Changed 8 years ago by rl

I'd like to resurrect this ticket. I think prefixing every type binder with type is ok, i.e., let's go with

forall (type a :: *) (type b :: *) (f :: a->b).   <blah>

comment:8 Changed 8 years ago by simonpj

Type of failure: None/Unknown

See also #2110

comment:9 Changed 7 years ago by igloo

Milestone: 6.12 branch6.12.3

comment:10 Changed 7 years ago by igloo

Milestone: 6.12.36.14.1
Priority: normallow

comment:11 Changed 7 years ago by igloo

Milestone: 7.0.17.0.2

comment:12 Changed 7 years ago by igloo

Milestone: 7.0.27.2.1

comment:13 Changed 6 years ago by igloo

Milestone: 7.2.17.4.1

comment:14 Changed 6 years ago by igloo

Milestone: 7.4.17.6.1
Priority: lowlowest

comment:15 Changed 6 years ago by nomeata

Cc: mail@… added

comment:16 Changed 5 years ago by igloo

Milestone: 7.6.17.6.2

Changed 5 years ago by morabbin

Attachment: T2600.hs added

Exhibits issue described in #2600

comment:17 Changed 5 years ago by morabbin

comment:18 Changed 3 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:19 Changed 3 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:20 Changed 3 years ago by thoughtpolice

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:21 Changed 2 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:22 Changed 21 months ago by thomie

Milestone: 8.0.1

comment:23 Changed 4 months ago by goldfire

Ideas to fix this are in this recent proposal.

Note: See TracTickets for help on using tickets.