Rules: "Forall'd constraint ‘Num Int’ is not bound in RULE lhs"
Consider
foo :: (forall a. [a] -> Int) -> Int
foo len = len [1,2,3] + len "abc"
{-# RULES "foo" forall (f :: forall a. [a] -> Int). foo (\xs -> 1 + f xs) = 2 + foo f #-}
{-# NOINLINE foo #-}
bar :: Int
bar = foo f
where
f xs = 1 + length xs
Apart from the fact that the RULE does not fire today (I came up with the example as a motivation for !9343 (closed)), GHC emits the following warning:
test.hs:12:11: warning: [GHC-40548]
Forall'd constraint ‘Num Int’ is not bound in RULE lhs
Orig bndrs: [$dNum_aQO, $dNum_aQQ, f]
Orig lhs: foo
(\ (@a) (xs :: [a]) ->
+ @Int $dNum_aQO (GHC.Types.I# 1#) (f @a xs))
optimised lhs: foo
(\ (@a) (xs :: [a]) ->
+ @Int $dNum_aQO (GHC.Types.I# 1#) (f @a xs))
|
12 | {-# RULES "foo" forall (f :: forall a. [a] -> Int). foo (\xs -> 1 + f xs) = 2 + foo f #-}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
I think that warning is wrong: The Num Int
dictionaries should not actually need to be quantified over but rather solved directly. I'm not sure what's going on here.