Open roboguy13 opened 8 years ago
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
.
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
?
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
).
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) #-}
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)
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.
@ecaustin It might be a little late for GHC 8, but maybe this would make a decent feature request?
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?
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.
Typechecking of RULES appears to be unchanged in GHC 8.0.
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?
I narrowed the error this down to this example
And I have a HERMIT session that looks like this:
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
andx :: 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
The warning goes away (and changes to a warning about
const
possibly inlining, which I think is ok) andrule-to-lemma grab-intro
works fine.I'm using GHC 7.10.3.