Be more careful when reporting unbound RULE binderswip/T22471

See Note [Variables unbound on the LHS] in GHC.HsToCore.Binds.

Fixes #22471.

7 files changed, 88 insertions, 32 deletions

diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 6451eab75e..65b654356e 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -36,7 +36,7 @@ module GHC.Core.FVs (
         ruleLhsFreeIds, ruleLhsFreeIdsList,
         ruleRhsFreeVars, rulesRhsFreeIds,
 
-        expr_fvs,
+        exprFVs,
 
         -- * Orphan names
         orphNamesOfType, orphNamesOfCo, orphNamesOfAxiom,
diff --git a/compiler/GHC/Core/Subst.hs b/compiler/GHC/Core/Subst.hs
index 5d8cd11758..4f87e5ad8e 100644
--- a/compiler/GHC/Core/Subst.hs
+++ b/compiler/GHC/Core/Subst.hs
@@ -577,7 +577,7 @@ substDVarSet subst@(Subst _ _ tv_env cv_env) fvs
      = tyCoFVsOfCo fv_co (const True) emptyVarSet $! acc
      | otherwise
      , let fv_expr = lookupIdSubst subst fv
-     = expr_fvs fv_expr isLocalVar emptyVarSet $! acc
+     = exprFVs fv_expr (const True) emptyVarSet $! acc
 
 ------------------
 substTickish :: Subst -> CoreTickish -> CoreTickish
diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs
index 3a3128489c..2ceb918fb1 100644
--- a/compiler/GHC/HsToCore.hs
+++ b/compiler/GHC/HsToCore.hs
@@ -48,7 +48,7 @@ import GHC.Core.Type
 import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.TyCon       ( tyConDataCons )
 import GHC.Core
-import GHC.Core.FVs       ( exprsSomeFreeVarsList )
+import GHC.Core.FVs       ( exprsSomeFreeVarsList, exprFreeVars )
 import GHC.Core.SimpleOpt ( simpleOptPgm, simpleOptExpr )
 import GHC.Core.Utils
 import GHC.Core.Unfold.Make
@@ -463,7 +463,7 @@ dsRule (L loc (HsRule { rd_name = name
         -- Substitute the dict bindings eagerly,
         -- and take the body apart into a (f args) form
         ; dflags <- getDynFlags
-        ; case decomposeRuleLhs dflags bndrs'' lhs'' of {
+        ; case decomposeRuleLhs dflags bndrs'' lhs'' (exprFreeVars rhs'') of {
                 Left msg -> do { diagnosticDs msg; return Nothing } ;
                 Right (final_bndrs, fn_id, args) -> do
 
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index c33b753d07..7d1eeb3268 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -708,7 +708,7 @@ dsSpec mb_poly_rhs (L loc (SpecPrag poly_id spec_co spec_inl))
          --                         , text "spec_co:" <+> ppr spec_co
          --                         , text "ds_rhs:" <+> ppr ds_lhs ]) $
          dflags <- getDynFlags
-       ; case decomposeRuleLhs dflags spec_bndrs ds_lhs of {
+       ; case decomposeRuleLhs dflags spec_bndrs ds_lhs (mkVarSet spec_bndrs) of {
            Left msg -> do { diagnosticDs msg; return Nothing } ;
            Right (rule_bndrs, _fn, rule_lhs_args) -> do
 
@@ -835,6 +835,7 @@ SPEC f :: ty                [n]   INLINE [k]
 -}
 
 decomposeRuleLhs :: DynFlags -> [Var] -> CoreExpr
+                 -> VarSet   -- Free vars of the RHS
                  -> Either DsMessage ([Var], Id, [CoreExpr])
 -- (decomposeRuleLhs bndrs lhs) takes apart the LHS of a RULE,
 -- The 'bndrs' are the quantified binders of the rules, but decomposeRuleLhs
@@ -842,47 +843,63 @@ decomposeRuleLhs :: DynFlags -> [Var] -> CoreExpr
 --
 -- Returns an error message if the LHS isn't of the expected shape
 -- Note [Decomposing the left-hand side of a RULE]
-decomposeRuleLhs dflags orig_bndrs orig_lhs
-  | not (null unbound)    -- Check for things unbound on LHS
-                          -- See Note [Unused spec binders]
-  = Left (DsRuleBindersNotBound unbound orig_bndrs orig_lhs lhs2)
+decomposeRuleLhs dflags orig_bndrs orig_lhs rhs_fvs
   | Var funId <- fun2
   , Just con <- isDataConId_maybe funId
   = Left (DsRuleIgnoredDueToConstructor con) -- See Note [No RULES on datacons]
-  | Just (fn_id, args) <- decompose fun2 args2
-  , let extra_bndrs = mk_extra_bndrs fn_id args
-  = -- pprTrace "decomposeRuleLhs" (vcat [ text "orig_bndrs:" <+> ppr orig_bndrs
-    --                                  , text "orig_lhs:" <+> ppr orig_lhs
-    --                                  , text "lhs1:"     <+> ppr lhs1
-    --                                  , text "extra_bndrs:" <+> ppr extra_bndrs
-    --                                  , text "fn_id:" <+> ppr fn_id
-    --                                  , text "args:"   <+> ppr args]) $
-    Right (orig_bndrs ++ extra_bndrs, fn_id, args)
 
-  | otherwise
+  | Nothing <- mb_lhs_app
   = Left (DsRuleLhsTooComplicated orig_lhs lhs2)
+
+  | not (null unbound)    -- Check for things unbound on LHS
+                          -- See Note [Unused spec binders]
+  = -- pprTrace "decomposeRuleLhs 1" (vcat [ text "orig_bndrs:" <+> ppr orig_bndrs
+    --                                     , text "orig_lhs:" <+> ppr orig_lhs
+    --                                     , text "lhs_fvs:" <+> ppr lhs_fvs
+    --                                     , text "rhs_fvs:" <+> ppr rhs_fvs
+    --                                     , text "unbound:" <+> ppr unbound
+    --                                     ]) $
+    Left (DsRuleBindersNotBound unbound orig_bndrs orig_lhs lhs2)
+
+  | otherwise
+  = -- pprTrace "decomposeRuleLhs 2" (vcat [ text "orig_bndrs:" <+> ppr orig_bndrs
+    --                                    , text "orig_lhs:" <+> ppr orig_lhs
+    --                                    , text "lhs1:"     <+> ppr lhs1
+    --                                    , text "extra_bndrs:" <+> ppr extra_bndrs
+    --                                    , text "fn_id:" <+> ppr fn_id
+    --                                    , text "args:"   <+> ppr args
+    --                                    , text "args fvs:" <+> ppr (exprsFreeVarsList args)
+    --                                    ]) $
+    Right (trimmed_bndrs ++ extra_bndrs, fn_id, args)
+
  where
-   simpl_opts   = initSimpleOpts dflags
+   simpl_opts    = initSimpleOpts dflags
+   orig_bndr_set = mkVarSet orig_bndrs
+
    lhs1         = drop_dicts orig_lhs
    lhs2         = simpleOptExpr simpl_opts lhs1  -- See Note [Simplify rule LHS]
    (fun2,args2) = collectArgs lhs2
 
-   lhs_fvs    = exprFreeVars lhs2
-   unbound    = filterOut (`elemVarSet` lhs_fvs) orig_bndrs
+   mb_lhs_app = decompose fun2 args2
+   Just (fn_id, args) = mb_lhs_app
 
-   orig_bndr_set = mkVarSet orig_bndrs
+   -- See Note [Variables unbound on the LHS]
+   lhs_fvs       = exprsFreeVars args
+   all_fvs       = lhs_fvs `unionVarSet` rhs_fvs
+   trimmed_bndrs = filter (`elemVarSet` all_fvs) orig_bndrs
+   unbound       = filterOut (`elemVarSet` lhs_fvs) trimmed_bndrs
+                   -- Needed on RHS but not bound on LHS
 
         -- Add extra tyvar binders: Note [Free tyvars on rule LHS]
         -- and extra dict binders: Note [Free dictionaries on rule LHS]
-   mk_extra_bndrs fn_id args
-     = scopedSort unbound_tvs ++ unbound_dicts
+   extra_bndrs = scopedSort extra_tvs ++ extra_dicts
      where
-       unbound_tvs   = [ v | v <- unbound_vars, isTyVar v ]
-       unbound_dicts = [ mkLocalId (localiseName (idName d)) ManyTy (idType d)
-                       | d <- unbound_vars, isDictId d ]
-       unbound_vars  = [ v | v <- exprsFreeVarsList args
-                           , not (v `elemVarSet` orig_bndr_set)
-                           , not (v == fn_id) ]
+       extra_tvs   = [ v | v <- extra_vars, isTyVar v ]
+       extra_dicts = [ mkLocalId (localiseName (idName d)) ManyTy (idType d)
+                     | d <- extra_vars, isDictId d ]
+       extra_vars  = [ v | v <- exprsFreeVarsList args
+                         , not (v `elemVarSet` orig_bndr_set)
+                         , not (v == fn_id) ]
          -- fn_id: do not quantify over the function itself, which may
          -- itself be a dictionary (in pathological cases, #10251)
 
@@ -926,6 +943,27 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs
        needed' = (needed `minusVarSet` rhs_fvs) `extendVarSet` d
 
 {-
+Note [Variables unbound on the LHS]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We obviously want to complain about
+   RULE   forall x. f True = not x
+because the forall'd variable `x` is not bound on the LHS.
+
+It can be a bit delicate when dictionaries are involved.
+Consider #22471
+  {-# RULES "foo" forall (f :: forall a. [a] -> Int).
+                  foo (\xs. 1 + f xs) = 2 + foo f #-}
+
+We get two dicts on the LHS, one from `1` and one from `+`.
+For reasons described in Note [The SimplifyRule Plan] in
+GHC.Tc.Gen.Rule, we quantify separately over those dictionaries:
+   forall f (d1::Num Int) (d2 :: Num Int).
+   foo (\xs. (+) d1 (fromInteger d2 1) xs) = ...
+
+Now the desugarer shortcircuits (fromInteger d2 1) to (I# 1); so d2 is
+not mentioned at all (on LHS or RHS)! We don't want to complain about
+and unbound d2.  Hence the trimmed_bndrs.
+
 Note [Decomposing the left-hand side of a RULE]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 There are several things going on here.
@@ -956,6 +994,9 @@ Moreover, we have to do something rather similar for dictionaries;
 see Note [Free dictionaries on rule LHS].   So that's why we look for
 type variables free on the LHS, and quantify over them.
 
+This relies on there not being any in-scope tyvars, which is true for
+user-defined RULEs, which are always top-level.
+
 Note [Free dictionaries on rule LHS]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When the LHS of a specialisation rule, (/\as\ds. f es) has a free dict,
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index 047c0559bf..121c43b987 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -167,7 +167,8 @@ tcRule (HsRule { rd_ext  = ext
                                 , text "rule_ty:" <+> ppr rule_ty
                                 , text "ty_bndrs:" <+> ppr ty_bndrs
                                 , text "qtkvs ++ tpl_ids:" <+> ppr (qtkvs ++ tpl_ids)
-                                , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
+                                , text "tpl_id info:" <+>
+                                  vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ]
                   ])
 
        -- SimplfyRule Plan, step 5
diff --git a/testsuite/tests/simplCore/should_compile/T22471.hs b/testsuite/tests/simplCore/should_compile/T22471.hs
new file mode 100644
index 0000000000..8da285a4c6
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T22471.hs
@@ -0,0 +1,13 @@
+{-# OPTIONS_GHC -Wno-inline-rule-shadowing #-}
+-- Otherwise we get stuff about (+) may inline, which is
+-- true enough, but not the point of this test
+
+module T22471 where
+
+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 #-}
+
+
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 5d80e76d58..823a8bcb04 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -437,6 +437,7 @@ test('T22097', [grep_errmsg(r'case.*wgoEven') ], multimod_compile, ['T22097', '-
 
 test('T13873',  [ grep_errmsg(r'SPEC') ], compile, ['-O -ddump-rules'])
 test('T22357',  normal, compile, ['-O'])
+test('T22471',  normal, compile, ['-O'])
 test('T22347',  normal, compile, ['-O -fno-full-laziness'])
 test('T22347a', normal, compile, ['-O2 -fno-full-laziness'])