From 80ecf9846106e4fe39ce15d6fb7825591b4b7d0a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 24 Jun 2021 21:10:02 -0700
Subject: [PATCH] Don't introduce too many variables (#1961)

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
---
 .../hls-tactics-plugin/src/Wingman/Tactics.hs    | 16 +++++++++-------
 .../test/CodeAction/RunMetaprogramSpec.hs        |  1 +
 .../test/golden/IntrosTooMany.expected.hs        |  2 ++
 .../test/golden/IntrosTooMany.hs                 |  2 ++
 4 files changed, 14 insertions(+), 7 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs

diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index b2893e043cc..a78d0c4f05a 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/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 --git a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
index 03efe5c2660..2c0e44b5bc7 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/RunMetaprogramSpec.hs
+++ b/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 --git a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
new file mode 100644
index 00000000000..0deb964ab6d
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.expected.hs
@@ -0,0 +1,2 @@
+too_many :: a -> b -> c
+too_many a b = _
diff --git a/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs b/plugins/hls-tactics-plugin/test/golden/IntrosTooMany.hs
new file mode 100644
index 00000000000..066f123a478
--- /dev/null
+++ b/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 |]