Cannot find a RULE that has a forall'd function called with a forall'd argument

[roboguy13]

I narrowed the error this down to this example

main :: IO ()
main = return ()

grab :: a -> a
grab = error "No grabs should be in generated code"
{-# NOINLINE grab #-}

{-# RULES "grab-intro" [~]
      forall f x.
        grab (f x)
          =
        (grab f) (grab x)
  #-}

And I have a HERMIT session that looks like this:

[starting HERMIT v1.0.0.1 on GrabProblem.hs]
% ghc GrabProblem.hs -fforce-recomp -O2 -dcore-lint -fsimple-list-literals -fexpose-all-unfoldings -fplugin=HERMIT -fplugin-opt=HERMIT:*:
[1 of 1] Compiling Main             ( GrabProblem.hs, GrabProblem.o )

GrabProblem.hs:8:11: Warning:
    Forall'd type variable ‘a’ is not bound in RULE lhs
      Orig bndrs: [a, a, f, x]
      Orig lhs: grab @ a (f x)
      optimised lhs: grab @ a (f x)

module Main where
  main ∷ IO ()
  main ∷ IO ()
hermit<0> flatten-module
module Main where
  main ∷ IO ()
  main ∷ IO ()
hermit<1> rule-to-lemma grab-intro
Error in expression: rule-to-lemma grab-intro
Query failed: failed to find rule: grab-intro. If you think the rule exists, try running the flatten-module command at the top level.

The warning looks suspicious (I'm not sure I've seen it before), but I can get rid of it if I monomorphize the types (for example, if I make f :: Int -> Int and x :: Int in the RULE definition). The same problem remains though, so the warning might be unrelated.

I also notice that if I change the rule to

{-# RULES "grab-intro" [~]
      forall f x.
        const (grab (f x)) x
          =
        (grab f) (grab x)
  #-}

The warning goes away (and changes to a warning about const possibly inlining, which I think is ok) and rule-to-lemma grab-intro works fine.

I'm using GHC 7.10.3.

[roboguy13]

It works and HERMIT can find the RULE just fine if I add explicit type annotations to it and make the types more specialized (and add a module Main where at the top):

{-# RULES "grab-intro" [~]
      forall (f :: a -> a) (x :: a).
        grab (f x)
          =
        (grab f) (grab x)
  #-}

But if I make the type annotation for f more general like this, it doesn't work:

{-# RULES "grab-intro" [~]
      forall (f :: a -> b) (x :: a).
        grab (f x)
          =
        (grab f) (grab x)
  #-}

even though this should be a valid type. Also, GHC doesn't give any kind of error for this (just the warning from the original post), HERMIT just can't find the RULE with rule-to-lemma.

[xich]

IIRC, GHC drops the rule when one of those warnings triggers, which is why HERMIT probably can't find it. Can you paste the warning? I've seen these before, but can't remember the details at this point.

Is the type of grab: grab :: a -> a or grab :: forall a. a -> a?

[roboguy13]

The warning is

GrabProblem.hs:15:11: Warning:
    Forall'd type variable ‘a’ is not bound in RULE lhs
      Orig bndrs: [a, b, f, x]
      Orig lhs: grab @ b (f x)
      optimised lhs: grab @ b (f x)

(line 15 is the first line of the RULE).

[ecaustin]

I'm surprised you weren't getting rigid type variable errors too with the way you wrote your third rule.

I believe what you want is this:

{-# RULES "grab" [~]
  forall (f :: forall a. a -> b) x.
    grab (f x) = (grab f) (grab x) #-}

[ecaustin]

To clarify my answer, every variable that shows up on the rhs of a rule has to appear on the lhs too, terms and types both.

You can't have grab @ (a -> b) f for the rhs because a never appears on the lhs: grab @ b (f x).

Making the type of f universal in its first argument forces a seemingly superfluous type application on the lhs so that a is available on the rhs:
forall b a f x. grab @ b (f @ a x) ≡ grab @ (a -> b) (f @ a) (grab @ a x)

[ecaustin]

Ideally, we would write the rule like this:

{-# RULES "grab" [~]
  tyforall a b. forall (f :: a -> b) (x :: a).
    grab (f x) = (grab f) (grab x) #-}

But the rewrite rule syntax does not allow for bound type variables outside of type ascriptions.

Unless they added something with GHC 8 that I don't know about?
It seems like that would be an obvious thing to add with explicit type applications, but I don't think it was done.

[roboguy13]

@ecaustin It might be a little late for GHC 8, but maybe this would make a decent feature request?

[ecaustin]

Does anyone have GHC 8 installed to test if your original version of the rule works or not?
SPJ left this comment at https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase1:
"We should discuss simplifyRule. I'm still a little mystified about how RULES are typechecked."

So maybe the type-checking of RULES is already fixed/addressed in GHC 8?

[ecaustin]

If not I can set up a VM and look into this more this weekend. I've just been short on free time as of late.

[ecaustin]

Typechecking of RULES appears to be unchanged in GHC 8.0.

[roboguy13]

Well, I think I found a way to temporarily bypass the type checker in, hopefully, a relatively safe way to turn functions into endofunctions (of the form a -> a) and then change them back later. Not my favorite thing, but maybe it will work for the time being.

Maybe it's worth mentioning this restriction to the GHC devs though?