Don't introduce too many variables (#1961)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: isovector

Diff for: plugins/hls-tactics-plugin/src/Wingman/Tactics.hs

@@ -127,21 +127,23 @@ intros' names = rule $ \jdg -> do
   let g  = jGoal jdg
   case tacticsSplitFunTy $ unCType g of
     (_, _, [], _) -> throwError $ GoalMismatch "intros" g
-    (_, _, as, b) -> do
+    (_, _, args, res) -> do
       ctx <- ask
-      let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
-          num_args = length vs
+      let occs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) args) names
+          num_occs = length occs
           top_hole = isTopHole ctx jdg
-          hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
+          bindings = zip occs $ coerce args
+          bound_occs = fmap fst bindings
+          hy' = lambdaHypothesis top_hole bindings
           jdg' = introduce ctx hy'
-               $ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg
+               $ withNewGoal (CType $ mkFunTys' (drop num_occs args) res) jdg
       ext <- newSubgoal jdg'
       pure $
         ext
-          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show vs) <> "}")
+          & #syn_trace %~ rose ("intros {" <> intercalate ", " (fmap show bound_occs) <> "}")
                         . pure
           & #syn_scoped <>~ hy'
-          & #syn_val   %~ noLoc . lambda (fmap bvar' vs) . unLoc
+          & #syn_val   %~ noLoc . lambda (fmap bvar' bound_occs) . unLoc
 
 
 ------------------------------------------------------------------------------

Diff for: plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs

@@ -38,4 +38,5 @@ spec = do
     metaTest  4 28 "MetaUseSymbol"
     metaTest  7 53 "MetaDeepOf"
     metaTest  2 34 "MetaWithArg"
+    metaTest  2 12 "IntrosTooMany"
 

Diff for: plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs

@@ -0,0 +1,2 @@
+too_many :: a -> b -> c
+too_many a b = _

Diff for: plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs

@@ -0,0 +1,2 @@
+too_many :: a -> b -> c
+too_many = [wingman| intros a b c d e f g h i j k l m n o p q r s t u v w x y z |]