From fae53e4805bfca13ef6ef4030584e90759cbbd43 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 12:37:16 -0800
Subject: [PATCH 01/12] Add name to HyInfo

---
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs   | 4 ++--
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs    | 2 +-
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs    | 5 +++--
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 75321a170c..33057262cf 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -61,7 +61,7 @@ buildHypothesis
   where
     go (occName -> occ, t)
       | Just ty <- t
-      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)
+      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo occ UserPrv $ CType ty)
       | otherwise = Nothing
 
 
@@ -97,7 +97,7 @@ introducing
     -> Judgement' a
 introducing f ns =
   field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
-    \(pos, (name, ty)) -> (name, HyInfo (f pos) ty))
+    \(pos, (name, ty)) -> (name, HyInfo name (f pos) ty))
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
index 559d983e31..9eea51b7ff 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
@@ -231,7 +231,7 @@ methodHypothesis ty = do
   pure $ mappend sc_methods $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in ( occName method
-       , HyInfo (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
+       , HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
        )
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index c9d1bdd514..1b5fdf0db4 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -218,7 +218,8 @@ instance Uniquable a => Ord (Uniquely a) where
 ------------------------------------------------------------------------------
 -- | The provenance and type of a hypothesis term.
 data HyInfo a = HyInfo
-  { hi_provenance :: Provenance
+  { hi_name       :: OccName
+  , hi_provenance :: Provenance
   , hi_type       :: a
   }
   deriving stock (Functor, Eq, Show, Generic, Ord)
@@ -227,7 +228,7 @@ data HyInfo a = HyInfo
 ------------------------------------------------------------------------------
 -- | Map a function over the provenance.
 overProvenance :: (Provenance -> Provenance) -> HyInfo a -> HyInfo a
-overProvenance f (HyInfo prv ty) = HyInfo (f prv) ty
+overProvenance f (HyInfo name prv ty) = HyInfo name (f prv) ty
 
 
 ------------------------------------------------------------------------------

From d9402d7e303598d61b97700f18120ca78f367d14 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 12:52:39 -0800
Subject: [PATCH 02/12] Use a newtype for Hypotheses

---
 .../src/Ide/Plugin/Tactic.hs                  | 12 ++---
 .../src/Ide/Plugin/Tactic/CodeGen.hs          |  6 +--
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 45 +++++++++++--------
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 +
 .../src/Ide/Plugin/Tactic/Naming.hs           |  6 +--
 .../src/Ide/Plugin/Tactic/Tactics.hs          | 17 +++----
 .../src/Ide/Plugin/Tactic/Types.hs            |  9 +++-
 7 files changed, 58 insertions(+), 39 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 494865d6ac..7ac74aefc3 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -216,7 +216,7 @@ filterBindingType
 filterBindingType p tp dflags plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
-   in fmap join $ for (M.toList hy) $ \(occ, hi_type -> CType ty) ->
+   in fmap join $ for (M.toList $ hyByName hy) $ \(occ, hi_type -> CType ty) ->
         case p (unCType g) ty of
           True  -> tp occ ty dflags plId uri range jdg
           False -> pure []
@@ -278,7 +278,7 @@ judgementForHole state nfp range = do
         HieFresh ->
           pure ( resulting_range
                , mkFirstJudgement
-                   (local_hy <> cls_hy)
+                   (local_hy <> Hypothesis cls_hy)
                    (isRhsHole rss tcs)
                    goal
                , ctx
@@ -287,10 +287,10 @@ judgementForHole state nfp range = do
 
 spliceProvenance
     :: Map OccName Provenance
-    -> Map OccName (HyInfo a)
-    -> Map OccName (HyInfo a)
-spliceProvenance provs =
-  M.mapWithKey $ \name hi ->
+    -> Hypothesis a
+    -> Hypothesis a
+spliceProvenance provs x =
+  Hypothesis $ flip M.mapWithKey (hyByName x) $ \name hi ->
     overProvenance (maybe id const $ M.lookup name provs) hi
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
index 0c1633d379..6e1a0cc11d 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -35,7 +35,7 @@ import           Type hiding (Var)
 useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
 useOccName jdg name =
   -- Only score points if this is in the local hypothesis
-  case M.lookup name $ jLocalHypothesis jdg of
+  case M.lookup name $ hyByName $ jLocalHypothesis jdg of
     Just{}  -> modify
              $ (withUsedVals $ S.insert name)
              . (field @"ts_unused_top_vals" %~ S.delete name)
@@ -75,7 +75,7 @@ destructMatches f scrut t jdg = do
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstOrigArgTys' dc apps
-          names <- mkManyGoodNames hy args
+          names <- mkManyGoodNames (hyNamesInScope hy) args
           let hy' = zip names $ coerce args
               j = introducingPat scrut dc hy'
                 $ withNewGoal g jdg
@@ -154,7 +154,7 @@ destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
 destruct' f term jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let hy = jHypothesis jdg
-  case M.lookup term hy of
+  case M.lookup term (hyByName hy) of
     Nothing -> throwError $ UndefinedHypothesis term
     Just (hi_type -> t) -> do
       useOccName jdg term
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 33057262cf..5a1c1087aa 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -26,6 +26,7 @@ module Ide.Plugin.Tactic.Judgements
   , mkFirstJudgement
   , hypothesisFromBindings
   , isTopLevel
+  , hyNamesInScope
   ) where
 
 import           Control.Lens hiding (Context)
@@ -48,15 +49,16 @@ import           Type
 
 ------------------------------------------------------------------------------
 -- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
-hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)
+hypothesisFromBindings :: RealSrcSpan -> Bindings -> Hypothesis CType
 hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
 
 
 ------------------------------------------------------------------------------
 -- | Convert a @Set Id@ into a hypothesis.
-buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)
+buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
 buildHypothesis
-  = M.fromList
+  = Hypothesis
+  . M.fromList
   . mapMaybe go
   where
     go (occName -> occ, t)
@@ -96,8 +98,8 @@ introducing
     -> Judgement' a
     -> Judgement' a
 introducing f ns =
-  field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
-    \(pos, (name, ty)) -> (name, HyInfo name (f pos) ty))
+  field @"_jHypothesis" <>~ Hypothesis (M.fromList (zip [0..] ns <&>
+    \(pos, (name, ty)) -> (name, HyInfo name (f pos) ty)))
 
 
 ------------------------------------------------------------------------------
@@ -149,7 +151,7 @@ filterAncestry
     -> Judgement
     -> Judgement
 filterAncestry ancestry reason jdg =
-    disallowing reason (M.keys $ M.filterWithKey go $ jHypothesis jdg) jdg
+    disallowing reason (M.keys $ M.filterWithKey go $ hyByName $ jHypothesis jdg) jdg
   where
     go name _
       = not
@@ -172,7 +174,7 @@ findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
 findPositionVal jdg defn pos = listToMaybe $ do
   -- It's important to inspect the entire hypothesis here, as we need to trace
   -- ancstry through potentially disallowed terms in the hypothesis.
-  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ jEntireHypothesis jdg
+  (name, hi) <- M.toList $ M.map (overProvenance expandDisallowed) $ hyByName $ jEntireHypothesis jdg
   case hi_provenance hi of
     TopLevelArgPrv defn' pos'
       | defn == defn'
@@ -188,7 +190,7 @@ findPositionVal jdg defn pos = listToMaybe $ do
 -- 'filterSameTypeFromOtherPositions'.
 findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
 findDconPositionVals jdg dcon pos = do
-  (name, hi) <- M.toList $ jHypothesis jdg
+  (name, hi) <- M.toList $ hyByName $ jHypothesis jdg
   case hi_provenance hi of
     PatternMatchPrv pv
       | pv_datacon  pv == Uniquely dcon
@@ -203,14 +205,15 @@ findDconPositionVals jdg dcon pos = do
 -- other term which might match.
 filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
 filterSameTypeFromOtherPositions dcon pos jdg =
-  let hy = jHypothesis
+  let hy = hyByName
+         . jHypothesis
          $ filterAncestry
              (findDconPositionVals jdg dcon pos)
              (WrongBranch pos)
              jdg
       tys = S.fromList $ hi_type <$> M.elems hy
       to_remove =
-        M.filter (flip S.member tys . hi_type) (jHypothesis jdg)
+        M.filter (flip S.member tys . hi_type) (hyByName $ jHypothesis jdg)
           M.\\ hy
    in disallowing Shadowed (M.keys to_remove) jdg
 
@@ -267,7 +270,7 @@ introducingPat scrutinee dc ns jdg
 -- them from 'jHypothesis', but not from 'jEntireHypothesis'.
 disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
 disallowing reason (S.fromList -> ns) =
-  field @"_jHypothesis" %~ (M.mapWithKey $ \name hi ->
+  field @"_jHypothesis" %~ (\z -> Hypothesis . flip M.mapWithKey (hyByName z) $ \name hi ->
     case S.member name ns of
       True -> overProvenance (DisallowedPrv reason) hi
       False -> hi
@@ -277,20 +280,20 @@ disallowing reason (S.fromList -> ns) =
 ------------------------------------------------------------------------------
 -- | The hypothesis, consisting of local terms and the ambient environment
 -- (impors and class methods.) Hides disallowed values.
-jHypothesis :: Judgement' a -> Map OccName (HyInfo a)
-jHypothesis = M.filter (not . isDisallowed . hi_provenance) . jEntireHypothesis
+jHypothesis :: Judgement' a -> Hypothesis a
+jHypothesis = Hypothesis . M.filter (not . isDisallowed . hi_provenance) . hyByName . jEntireHypothesis
 
 
 ------------------------------------------------------------------------------
 -- | The whole hypothesis, including things disallowed.
-jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)
+jEntireHypothesis :: Judgement' a -> Hypothesis a
 jEntireHypothesis = _jHypothesis
 
 
 ------------------------------------------------------------------------------
 -- | Just the local hypothesis.
-jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)
-jLocalHypothesis = M.filter (isLocalHypothesis . hi_provenance) . jHypothesis
+jLocalHypothesis :: Judgement' a -> Hypothesis a
+jLocalHypothesis = Hypothesis . M.filter (isLocalHypothesis . hi_provenance) . hyByName . jHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -304,10 +307,16 @@ unsetIsTopHole :: Judgement' a -> Judgement' a
 unsetIsTopHole = field @"_jIsTopHole" .~ False
 
 
+------------------------------------------------------------------------------
+-- | What names are currently in scope in the hypothesis?
+hyNamesInScope :: Hypothesis a -> [OccName]
+hyNamesInScope = M.keys . hyByName
+
+
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
 jPatHypothesis :: Judgement' a -> Map OccName PatVal
-jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . jHypothesis
+jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . hyByName . jHypothesis
 
 
 getPatVal :: Provenance-> Maybe PatVal
@@ -326,7 +335,7 @@ substJdg subst = fmap $ coerce . substTy subst . coerce
 
 
 mkFirstJudgement
-    :: M.Map OccName (HyInfo CType)
+    :: Hypothesis CType
     -> Bool  -- ^ are we in the top level rhs hole?
     -> Type
     -> Judgement' CType
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
index 9eea51b7ff..ad31293e4e 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
@@ -74,9 +74,11 @@ runTactic ctx jdg t =
                 $ (:) (jGoal jdg)
                 $ fmap hi_type
                 $ toList
+                $ hyByName
                 $ jHypothesis jdg
         unused_topvals = M.keysSet
                        $ M.filter (isTopLevel . hi_provenance)
+                       $ hyByName
                        $ jHypothesis jdg
         tacticState =
           defaultTacticState
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
index f6b054f987..98059bdf1c 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
@@ -75,11 +75,11 @@ mkGoodName in_scope t =
 -- | Like 'mkGoodName' but creates several apart names.
 mkManyGoodNames
   :: (Traversable t, Monad m)
-  => M.Map OccName a
+  => [OccName]
   -> t Type
   -> m (t OccName)
-mkManyGoodNames hy args =
-  flip evalStateT (getInScope hy) $ for args $ \at -> do
+mkManyGoodNames in_scope args =
+  flip evalStateT in_scope $ for args $ \at -> do
     in_scope <- get
     let n = mkGoodName in_scope at
     modify (n :)
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index 60b318c8cc..3c489aa170 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -51,7 +51,7 @@ assumption = attemptOn allNames assume
 assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
-  case M.lookup name $ jHypothesis jdg of
+  case M.lookup name $ hyByName $ jHypothesis jdg of
     Just (hi_type -> ty) -> do
       unify ty $ jGoal jdg
       for_ (M.lookup name $ jPatHypothesis jdg) markStructuralySmallerRecursion
@@ -80,7 +80,7 @@ intros = rule $ \jdg -> do
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
-      vs <- mkManyGoodNames (jEntireHypothesis jdg) as
+      vs <- mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as
       let top_hole = isTopHole ctx jdg
           jdg' = introducingLambda top_hole (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
@@ -99,14 +99,14 @@ intros = rule $ \jdg -> do
 destructAuto :: OccName -> TacticsM ()
 destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
   jdg <- goal
-  case M.lookup name $ jHypothesis jdg of
+  case M.lookup name $ hyByName $ jHypothesis jdg of
     Nothing -> throwError $ NotInScope name
     Just hi ->
       let subtactic = rule $ destruct' (const subgoal) name
       in case isPatternMatch $ hi_provenance hi of
             True ->
               pruning subtactic $ \jdgs ->
-                let getHyTypes = S.fromList . fmap hi_type . M.elems . jHypothesis
+                let getHyTypes = S.fromList . fmap hi_type . M.elems . hyByName . jHypothesis
                     new_hy = foldMap getHyTypes jdgs
                     old_hy = getHyTypes jdg
                 in case S.null $ new_hy S.\\ old_hy of
@@ -153,7 +153,7 @@ apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do
   jdg <- goal
   let hy = jHypothesis jdg
       g  = jGoal jdg
-  case M.lookup func hy of
+  case M.lookup func $ hyByName hy of
     Just (hi_type -> CType ty) -> do
       ty' <- freshTyvars ty
       let (_, _, args, ret) = tacticsSplitFunTy ty'
@@ -270,13 +270,14 @@ auto' n = do
 
 overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
 overFunctions =
-  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis
+  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . hyByName . jHypothesis
 
 overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
   attemptOn $
-    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis
+    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . hyByName . jHypothesis
 
 
 allNames :: Judgement -> [OccName]
-allNames = M.keys . jHypothesis
+allNames = hyNamesInScope . jHypothesis
+
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index 1b5fdf0db4..0b76180604 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -215,6 +215,13 @@ instance Uniquable a => Ord (Uniquely a) where
   compare = nonDetCmpUnique `on` getUnique . getViaUnique
 
 
+newtype Hypothesis a = Hypothesis
+  { hyByName :: Map OccName (HyInfo a)
+  }
+  deriving stock (Functor, Eq, Show, Generic, Ord)
+  deriving (Semigroup, Monoid) via Map OccName (HyInfo a)
+
+
 ------------------------------------------------------------------------------
 -- | The provenance and type of a hypothesis term.
 data HyInfo a = HyInfo
@@ -234,7 +241,7 @@ overProvenance f (HyInfo name prv ty) = HyInfo name (f prv) ty
 ------------------------------------------------------------------------------
 -- | The current bindings and goal for a hole to be filled by refinery.
 data Judgement' a = Judgement
-  { _jHypothesis :: !(Map OccName (HyInfo a))
+  { _jHypothesis :: !(Hypothesis a)
   , _jBlacklistDestruct :: !Bool
   , _jWhitelistSplit :: !Bool
   , _jIsTopHole    :: !Bool

From bac26b3df2bde963f90cdcfe1f07ac93f82f828f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 13:03:23 -0800
Subject: [PATCH 03/12] Use a set for tracking names in scope

---
 .../src/Ide/Plugin/Tactic/Judgements.hs                |  4 ++--
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs | 10 ++++++----
 .../src/Ide/Plugin/Tactic/Tactics.hs                   |  5 +++--
 3 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 5a1c1087aa..31cd4c31dd 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -309,8 +309,8 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False
 
 ------------------------------------------------------------------------------
 -- | What names are currently in scope in the hypothesis?
-hyNamesInScope :: Hypothesis a -> [OccName]
-hyNamesInScope = M.keys . hyByName
+hyNamesInScope :: Hypothesis a -> Set OccName
+hyNamesInScope = M.keysSet . hyByName
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
index 98059bdf1c..4ab1149f82 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
@@ -2,6 +2,8 @@
 
 module Ide.Plugin.Tactic.Naming where
 
+import qualified Data.Set as S
+import Data.Set (Set)
 import           Control.Monad.State.Strict
 import           Data.Bool (bool)
 import           Data.Char
@@ -61,12 +63,12 @@ filterReplace f r = fmap (\a -> bool a r $ f a)
 ------------------------------------------------------------------------------
 -- | Produce a unique, good name for a type.
 mkGoodName
-    :: [OccName]  -- ^ Bindings in scope; used to ensure we don't shadow anything
+    :: Set OccName  -- ^ Bindings in scope; used to ensure we don't shadow anything
     -> Type       -- ^ The type to produce a name for
     -> OccName
 mkGoodName in_scope t =
   let tn = mkTyName t
-   in mkVarOcc $ case elem (mkVarOcc tn) in_scope of
+   in mkVarOcc $ case S.member (mkVarOcc tn) in_scope of
         True -> tn ++ show (length in_scope)
         False -> tn
 
@@ -75,14 +77,14 @@ mkGoodName in_scope t =
 -- | Like 'mkGoodName' but creates several apart names.
 mkManyGoodNames
   :: (Traversable t, Monad m)
-  => [OccName]
+  => Set OccName
   -> t Type
   -> m (t OccName)
 mkManyGoodNames in_scope args =
   flip evalStateT in_scope $ for args $ \at -> do
     in_scope <- get
     let n = mkGoodName in_scope at
-    modify (n :)
+    modify $ S.insert n
     pure n
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index 3c489aa170..7777630fa1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -20,6 +20,7 @@ import           Data.Foldable
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
+import           Data.Set (Set)
 import qualified Data.Set as S
 import           DataCon
 import           Development.IDE.GHC.Compat
@@ -43,7 +44,7 @@ import           Type hiding (Var)
 ------------------------------------------------------------------------------
 -- | Use something in the hypothesis to fill the hole.
 assumption :: TacticsM ()
-assumption = attemptOn allNames assume
+assumption = attemptOn (S.toList . allNames) assume
 
 
 ------------------------------------------------------------------------------
@@ -278,6 +279,6 @@ overAlgebraicTerms =
     M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . hyByName . jHypothesis
 
 
-allNames :: Judgement -> [OccName]
+allNames :: Judgement -> Set OccName
 allNames = hyNamesInScope . jHypothesis
 

From 9d0ef3a95b7ef9b22a883bc4f14242ebd2f04e31 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 13:35:37 -0800
Subject: [PATCH 04/12] Remove the internal Map OccName representation of
 Hypothesis

---
 .../src/Ide/Plugin/Tactic.hs                  |  6 +++---
 .../src/Ide/Plugin/Tactic/Context.hs          |  8 ++++----
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 20 +++++++++++--------
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  5 ++---
 .../src/Ide/Plugin/Tactic/Types.hs            |  4 ++--
 5 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 7ac74aefc3..73956109fb 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -278,7 +278,7 @@ judgementForHole state nfp range = do
         HieFresh ->
           pure ( resulting_range
                , mkFirstJudgement
-                   (local_hy <> Hypothesis cls_hy)
+                   (local_hy <> cls_hy)
                    (isRhsHole rss tcs)
                    goal
                , ctx
@@ -290,8 +290,8 @@ spliceProvenance
     -> Hypothesis a
     -> Hypothesis a
 spliceProvenance provs x =
-  Hypothesis $ flip M.mapWithKey (hyByName x) $ \name hi ->
-    overProvenance (maybe id const $ M.lookup name provs) hi
+  Hypothesis $ flip fmap (unHypothesis x) $ \hi ->
+    overProvenance (maybe id const $ M.lookup (hi_name hi) provs) hi
 
 
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs
index 15150c938e..ad5f937f6f 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs
@@ -35,9 +35,9 @@ mkContext locals tcg = Context
 
 ------------------------------------------------------------------------------
 -- | Find all of the class methods that exist from the givens in the context.
-contextMethodHypothesis :: Context -> Map OccName (HyInfo CType)
+contextMethodHypothesis :: Context -> Hypothesis CType
 contextMethodHypothesis ctx
-  = M.fromList
+  = Hypothesis
   . excludeForbiddenMethods
   . join
   . concatMap
@@ -54,8 +54,8 @@ contextMethodHypothesis ctx
 -- | Many operations are defined in typeclasses for performance reasons, rather
 -- than being a true part of the class. This function filters out those, in
 -- order to keep our hypothesis space small.
-excludeForbiddenMethods :: [(OccName, a)] -> [(OccName, a)]
-excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
+excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
   where
     forbiddenMethods :: Set OccName
     forbiddenMethods = S.map mkVarOcc $ S.fromList
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 31cd4c31dd..cf6d3e2c03 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -27,8 +27,10 @@ module Ide.Plugin.Tactic.Judgements
   , hypothesisFromBindings
   , isTopLevel
   , hyNamesInScope
+  , hyByName
   ) where
 
+import Control.Arrow
 import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char
@@ -58,12 +60,11 @@ hypothesisFromBindings span bs = buildHypothesis $ getLocalScope bs span
 buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
 buildHypothesis
   = Hypothesis
-  . M.fromList
   . mapMaybe go
   where
     go (occName -> occ, t)
       | Just ty <- t
-      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo occ UserPrv $ CType ty)
+      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ UserPrv $ CType ty
       | otherwise = Nothing
 
 
@@ -98,8 +99,8 @@ introducing
     -> Judgement' a
     -> Judgement' a
 introducing f ns =
-  field @"_jHypothesis" <>~ Hypothesis (M.fromList (zip [0..] ns <&>
-    \(pos, (name, ty)) -> (name, HyInfo name (f pos) ty)))
+  field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&>
+    \(pos, (name, ty)) -> HyInfo name (f pos) ty)
 
 
 ------------------------------------------------------------------------------
@@ -270,8 +271,8 @@ introducingPat scrutinee dc ns jdg
 -- them from 'jHypothesis', but not from 'jEntireHypothesis'.
 disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
 disallowing reason (S.fromList -> ns) =
-  field @"_jHypothesis" %~ (\z -> Hypothesis . flip M.mapWithKey (hyByName z) $ \name hi ->
-    case S.member name ns of
+  field @"_jHypothesis" %~ (\z -> Hypothesis . flip fmap (unHypothesis z) $ \hi ->
+    case S.member (hi_name hi) ns of
       True -> overProvenance (DisallowedPrv reason) hi
       False -> hi
                            )
@@ -281,7 +282,7 @@ disallowing reason (S.fromList -> ns) =
 -- | The hypothesis, consisting of local terms and the ambient environment
 -- (impors and class methods.) Hides disallowed values.
 jHypothesis :: Judgement' a -> Hypothesis a
-jHypothesis = Hypothesis . M.filter (not . isDisallowed . hi_provenance) . hyByName . jEntireHypothesis
+jHypothesis = Hypothesis . filter (not . isDisallowed . hi_provenance) . unHypothesis . jEntireHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -293,7 +294,7 @@ jEntireHypothesis = _jHypothesis
 ------------------------------------------------------------------------------
 -- | Just the local hypothesis.
 jLocalHypothesis :: Judgement' a -> Hypothesis a
-jLocalHypothesis = Hypothesis . M.filter (isLocalHypothesis . hi_provenance) . hyByName . jHypothesis
+jLocalHypothesis = Hypothesis . filter (isLocalHypothesis . hi_provenance) . unHypothesis . jHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -312,6 +313,9 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False
 hyNamesInScope :: Hypothesis a -> Set OccName
 hyNamesInScope = M.keysSet . hyByName
 
+hyByName :: Hypothesis a -> Map OccName (HyInfo a)
+hyByName = M.fromList . fmap (hi_name &&& id) . unHypothesis
+
 
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
index ad31293e4e..dd307da2ca 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
@@ -220,7 +220,7 @@ unify goal inst = do
 ------------------------------------------------------------------------------
 -- | Get the class methods of a 'PredType', correctly dealing with
 -- instantiation of quantified class types.
-methodHypothesis :: PredType -> Maybe [(OccName, HyInfo CType)]
+methodHypothesis :: PredType -> Maybe [HyInfo CType]
 methodHypothesis ty = do
   (tc, apps) <- splitTyConApp_maybe ty
   cls <- tyConClass_maybe tc
@@ -232,8 +232,7 @@ methodHypothesis ty = do
               $ classSCTheta cls
   pure $ mappend sc_methods $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
-    in ( occName method
-       , HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
+    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
        )
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
index 0b76180604..ac0ab3dff1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -216,10 +216,10 @@ instance Uniquable a => Ord (Uniquely a) where
 
 
 newtype Hypothesis a = Hypothesis
-  { hyByName :: Map OccName (HyInfo a)
+  { unHypothesis :: [HyInfo a]
   }
   deriving stock (Functor, Eq, Show, Generic, Ord)
-  deriving (Semigroup, Monoid) via Map OccName (HyInfo a)
+  deriving newtype (Semigroup, Monoid)
 
 
 ------------------------------------------------------------------------------

From fb04421b4ee2e5c67e3c2ba26d8a7db8aeb745a1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 13:45:45 -0800
Subject: [PATCH 05/12] Remove most spurious uses of hyByName

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs |  9 +++++----
 .../src/Ide/Plugin/Tactic/CodeGen.hs                |  2 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs             | 11 ++++++++++-
 .../src/Ide/Plugin/Tactic/Tactics.hs                | 13 +++++++++----
 4 files changed, 25 insertions(+), 10 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 73956109fb..9d4c7a5b31 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -216,10 +216,11 @@ filterBindingType
 filterBindingType p tp dflags plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
-   in fmap join $ for (M.toList $ hyByName hy) $ \(occ, hi_type -> CType ty) ->
-        case p (unCType g) ty of
-          True  -> tp occ ty dflags plId uri range jdg
-          False -> pure []
+   in fmap join $ for (unHypothesis hy) $ \hi ->
+        let ty = unCType $ hi_type hi
+         in case p (unCType g) ty of
+              True  -> tp (hi_name hi) ty dflags plId uri range jdg
+              False -> pure []
 
 
 data TacticParams = TacticParams
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
index 6e1a0cc11d..faba039541 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -154,7 +154,7 @@ destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
 destruct' f term jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let hy = jHypothesis jdg
-  case M.lookup term (hyByName hy) of
+  case M.lookup term $ hyByName hy of
     Nothing -> throwError $ UndefinedHypothesis term
     Just (hi_type -> t) -> do
       useOccName jdg term
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index cf6d3e2c03..5fb8040860 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -313,8 +313,17 @@ unsetIsTopHole = field @"_jIsTopHole" .~ False
 hyNamesInScope :: Hypothesis a -> Set OccName
 hyNamesInScope = M.keysSet . hyByName
 
+
+------------------------------------------------------------------------------
+-- | Fold a hypothesis into a single mapping from name to info. This
+-- unavoidably will cause duplicate names (things like methods) to shadow one
+-- another.
 hyByName :: Hypothesis a -> Map OccName (HyInfo a)
-hyByName = M.fromList . fmap (hi_name &&& id) . unHypothesis
+hyByName
+  = M.fromList
+  . fmap (hi_name &&& id)
+  -- . filter (not . isDisallowed . hi_provenance)
+  . unHypothesis
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index 7777630fa1..855d30bc6b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -107,7 +107,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
       in case isPatternMatch $ hi_provenance hi of
             True ->
               pruning subtactic $ \jdgs ->
-                let getHyTypes = S.fromList . fmap hi_type . M.elems . hyByName . jHypothesis
+                let getHyTypes = S.fromList . fmap hi_type . unHypothesis . jHypothesis
                     new_hy = foldMap getHyTypes jdgs
                     old_hy = getHyTypes jdg
                 in case S.null $ new_hy S.\\ old_hy of
@@ -271,12 +271,17 @@ auto' n = do
 
 overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
 overFunctions =
-  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . hyByName . jHypothesis
+  attemptOn $ fmap hi_name
+           . filter (isFunction . unCType . hi_type)
+           . unHypothesis
+           . jHypothesis
 
 overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
-  attemptOn $
-    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . hyByName . jHypothesis
+  attemptOn $ fmap hi_name
+            . filter (isJust . algebraicTyCon . unCType . hi_type)
+            . unHypothesis
+            . jHypothesis
 
 
 allNames :: Judgement -> Set OccName

From c02b016bd0addf9602acb90ae1c3cfb033dbbb9a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 15:56:25 -0800
Subject: [PATCH 06/12] Stop looking up things by name in hyByName; use hi
 directly

---
 .../src/Ide/Plugin/Tactic.hs                  | 15 ++-
 .../src/Ide/Plugin/Tactic/CodeGen.hs          | 29 +++---
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 18 +++-
 .../src/Ide/Plugin/Tactic/Tactics.hs          | 96 +++++++++----------
 4 files changed, 85 insertions(+), 73 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 9d4c7a5b31..d45913cc84 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -61,6 +61,8 @@ import           OccName
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
+import Refinery.Tactic (goal)
+import Control.Monad.Error (MonadError(throwError))
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState
@@ -124,12 +126,21 @@ commandProvider HomomorphismLambdaCase =
 commandTactic :: TacticCommand -> OccName -> TacticsM ()
 commandTactic Auto         = const auto
 commandTactic Intros       = const intros
-commandTactic Destruct     = destruct
-commandTactic Homomorphism = homo
+commandTactic Destruct     = useNameFromHypothesis destruct
+commandTactic Homomorphism = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
 
+useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
+useNameFromHypothesis f name = do
+  hy <- jHypothesis <$> goal
+  case M.lookup name $ hyByName hy of
+    Just hi -> f hi
+    Nothing -> throwError $ NotInScope name
+
+
+
 ------------------------------------------------------------------------------
 -- | We should show homos only when the goal type is the same as the binding
 -- type, and that both are usual algebraic types.
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
index faba039541..1cab232a7a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -150,23 +150,20 @@ dataConInstOrigArgTys' con uniTys =
 -- | Combinator for performing case splitting, and running sub-rules on the
 -- resulting matches.
 
-destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
-destruct' f term jdg = do
+destruct' :: (DataCon -> Judgement -> Rule) -> HyInfo CType -> Judgement -> Rule
+destruct' f hi jdg = do
   when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
-  let hy = jHypothesis jdg
-  case M.lookup term $ hyByName hy of
-    Nothing -> throwError $ UndefinedHypothesis term
-    Just (hi_type -> t) -> do
-      useOccName jdg term
-      (tr, ms)
-          <- destructMatches
-               f
-               (Just term)
-               t
-               $ disallowing AlreadyDestructed [term] jdg
-      pure ( rose ("destruct " <> show term) $ pure tr
-           , noLoc $ case' (var' term) ms
-           )
+  let term = hi_name hi
+  useOccName jdg term
+  (tr, ms)
+      <- destructMatches
+           f
+           (Just term)
+           (hi_type hi)
+           $ disallowing AlreadyDestructed [term] jdg
+  pure ( rose ("destruct " <> show term) $ pure tr
+       , noLoc $ case' (var' term) ms
+       )
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 5fb8040860..533ba74f94 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -282,7 +282,11 @@ disallowing reason (S.fromList -> ns) =
 -- | The hypothesis, consisting of local terms and the ambient environment
 -- (impors and class methods.) Hides disallowed values.
 jHypothesis :: Judgement' a -> Hypothesis a
-jHypothesis = Hypothesis . filter (not . isDisallowed . hi_provenance) . unHypothesis . jEntireHypothesis
+jHypothesis
+  = Hypothesis
+  . filter (not . isDisallowed . hi_provenance)
+  . unHypothesis
+  . jEntireHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -294,7 +298,11 @@ jEntireHypothesis = _jHypothesis
 ------------------------------------------------------------------------------
 -- | Just the local hypothesis.
 jLocalHypothesis :: Judgement' a -> Hypothesis a
-jLocalHypothesis = Hypothesis . filter (isLocalHypothesis . hi_provenance) . unHypothesis . jHypothesis
+jLocalHypothesis
+  = Hypothesis
+  . filter (isLocalHypothesis . hi_provenance)
+  . unHypothesis
+  . jHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -322,14 +330,16 @@ hyByName :: Hypothesis a -> Map OccName (HyInfo a)
 hyByName
   = M.fromList
   . fmap (hi_name &&& id)
-  -- . filter (not . isDisallowed . hi_provenance)
   . unHypothesis
 
 
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
 jPatHypothesis :: Judgement' a -> Map OccName PatVal
-jPatHypothesis = M.mapMaybe (getPatVal . hi_provenance) . hyByName . jHypothesis
+jPatHypothesis
+  = M.mapMaybe (getPatVal . hi_provenance)
+  . hyByName
+  . jHypothesis
 
 
 getPatVal :: Provenance-> Maybe PatVal
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index 855d30bc6b..171f0a8749 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -64,10 +64,10 @@ assume name = rule $ \jdg -> do
 recursion :: TacticsM ()
 recursion = requireConcreteHole $ tracing "recursion" $ do
   defs <- getCurrentDefinitions
-  attemptOn (const $ fmap fst defs) $ \name -> do
+  attemptOn (const defs) $ \(name, ty) -> do
     modify $ pushRecursionStack .  countRecursiveCall
     ensure guardStructurallySmallerRecursion popRecursionStack $ do
-      (localTactic (apply name) $ introducingRecursively defs)
+      (localTactic (apply $ HyInfo name RecursivePrv ty) $ introducingRecursively defs)
         <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
@@ -97,35 +97,33 @@ intros = rule $ \jdg -> do
 
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
-destructAuto :: OccName -> TacticsM ()
-destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
+destructAuto :: HyInfo CType -> TacticsM ()
+destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do
+  let name = hi_name hi
   jdg <- goal
-  case M.lookup name $ hyByName $ jHypothesis jdg of
-    Nothing -> throwError $ NotInScope name
-    Just hi ->
-      let subtactic = rule $ destruct' (const subgoal) name
-      in case isPatternMatch $ hi_provenance hi of
-            True ->
-              pruning subtactic $ \jdgs ->
-                let getHyTypes = S.fromList . fmap hi_type . unHypothesis . jHypothesis
-                    new_hy = foldMap getHyTypes jdgs
-                    old_hy = getHyTypes jdg
-                in case S.null $ new_hy S.\\ old_hy of
-                      True  -> Just $ UnhelpfulDestruct name
-                      False -> Nothing
-            False -> subtactic
+  let subtactic = rule $ destruct' (const subgoal) hi
+  case isPatternMatch $ hi_provenance hi of
+    True ->
+      pruning subtactic $ \jdgs ->
+        let getHyTypes = S.fromList . fmap hi_type . unHypothesis . jHypothesis
+            new_hy = foldMap getHyTypes jdgs
+            old_hy = getHyTypes jdg
+        in case S.null $ new_hy S.\\ old_hy of
+              True  -> Just $ UnhelpfulDestruct name
+              False -> Nothing
+    False -> subtactic
 
 
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
-destruct :: OccName -> TacticsM ()
-destruct name = requireConcreteHole $ tracing "destruct(user)" $
-  rule $ destruct' (const subgoal) name
+destruct :: HyInfo CType -> TacticsM ()
+destruct hi = requireConcreteHole $ tracing "destruct(user)" $
+  rule $ destruct' (const subgoal) hi
 
 
 ------------------------------------------------------------------------------
 -- | Case split, using the same data constructor in the matches.
-homo :: OccName -> TacticsM ()
+homo :: HyInfo CType -> TacticsM ()
 homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
@@ -149,32 +147,30 @@ homoLambdaCase =
         $ jGoal jdg
 
 
-apply :: OccName -> TacticsM ()
-apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do
+apply :: HyInfo CType -> TacticsM ()
+apply hi = requireConcreteHole $ tracing ("apply' " <> show (hi_name hi)) $ do
   jdg <- goal
   let hy = jHypothesis jdg
       g  = jGoal jdg
-  case M.lookup func $ hyByName hy of
-    Just (hi_type -> CType ty) -> do
-      ty' <- freshTyvars ty
-      let (_, _, args, ret) = tacticsSplitFunTy ty'
-      requireNewHoles $ rule $ \jdg -> do
-        unify g (CType ret)
-        useOccName jdg func
-        (tr, sgs)
-            <- fmap unzipTrace
-            $ traverse ( newSubgoal
-                        . blacklistingDestruct
-                        . flip withNewGoal jdg
-                        . CType
-                        ) args
-        pure
-          . (tr, )
-          . noLoc
-          . foldl' (@@) (var' func)
-          $ fmap unLoc sgs
-    Nothing -> do
-      throwError $ GoalMismatch "apply" g
+      ty = unCType $ hi_type hi
+      func = hi_name hi
+  ty' <- freshTyvars ty
+  let (_, _, args, ret) = tacticsSplitFunTy ty'
+  requireNewHoles $ rule $ \jdg -> do
+    unify g (CType ret)
+    useOccName jdg func
+    (tr, sgs)
+        <- fmap unzipTrace
+        $ traverse ( newSubgoal
+                    . blacklistingDestruct
+                    . flip withNewGoal jdg
+                    . CType
+                    ) args
+    pure
+      . (tr, )
+      . noLoc
+      . foldl' (@@) (var' func)
+      $ fmap unLoc sgs
 
 
 ------------------------------------------------------------------------------
@@ -269,17 +265,15 @@ auto' n = do
     , recursion
     ]
 
-overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
+overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overFunctions =
-  attemptOn $ fmap hi_name
-           . filter (isFunction . unCType . hi_type)
+  attemptOn $ filter (isFunction . unCType . hi_type)
            . unHypothesis
            . jHypothesis
 
-overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
+overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
-  attemptOn $ fmap hi_name
-            . filter (isJust . algebraicTyCon . unCType . hi_type)
+  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)
             . unHypothesis
             . jHypothesis
 

From da9e9f3cfb9e6d79e8c3cf518925b469f8934b0f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 17:13:39 -0800
Subject: [PATCH 07/12] Cleanup imports

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index d45913cc84..4695d19652 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -17,6 +17,7 @@ module Ide.Plugin.Tactic
 
 import           Control.Arrow
 import           Control.Monad
+import           Control.Monad.Error.Class (MonadError(throwError))
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
@@ -38,6 +39,7 @@ import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (useWithStale, IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.Error (realSrcSpanToRange)
+import           Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource)
 import           Development.IDE.Spans.LocalBindings (getDefiningBindings)
 import           Development.Shake (Action)
 import           DynFlags (xopt)
@@ -53,16 +55,14 @@ import           Ide.Plugin.Tactic.Tactics
 import           Ide.Plugin.Tactic.TestTypes
 import           Ide.Plugin.Tactic.Types
 import           Ide.PluginUtils
-import Development.IDE.GHC.ExactPrint (graft, transform, useAnnotatedSource)
 import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           Refinery.Tactic (goal)
 import           SrcLoc (containsSpan)
 import           System.Timeout
 import           TcRnTypes (tcg_binds)
-import Refinery.Tactic (goal)
-import Control.Monad.Error (MonadError(throwError))
 
 
 descriptor :: PluginId -> PluginDescriptor IdeState

From ca6ff0e02caa38c455a399ff26c04a724687440e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 17:13:44 -0800
Subject: [PATCH 08/12] Add test for invoking methods at different types

---
 test/functional/Tactic.hs                 | 1 +
 test/testdata/tactic/FmapBoth.hs          | 3 +++
 test/testdata/tactic/FmapBoth.hs.expected | 4 ++++
 3 files changed, 8 insertions(+)
 create mode 100644 test/testdata/tactic/FmapBoth.hs
 create mode 100644 test/testdata/tactic/FmapBoth.hs.expected

diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index 5a3bbed4d6..6e33a96a90 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -116,6 +116,7 @@ tests = testGroup
   , goldenTest "GoldenSafeHead.hs"          2 12 Auto ""
   , expectFail "GoldenFish.hs"              5 18 Auto ""
   , goldenTest "GoldenArbitrary.hs"         25 13 Auto ""
+  , goldenTest "FmapBoth.hs"                2 12 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/FmapBoth.hs b/test/testdata/tactic/FmapBoth.hs
new file mode 100644
index 0000000000..29d8ea62b2
--- /dev/null
+++ b/test/testdata/tactic/FmapBoth.hs
@@ -0,0 +1,3 @@
+fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)
+fmapBoth = _
+
diff --git a/test/testdata/tactic/FmapBoth.hs.expected b/test/testdata/tactic/FmapBoth.hs.expected
new file mode 100644
index 0000000000..13b7e13604
--- /dev/null
+++ b/test/testdata/tactic/FmapBoth.hs.expected
@@ -0,0 +1,4 @@
+fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)
+fmapBoth = (\ fab p_xx
+   -> case p_xx of { (x, x5) -> (fmap fab x, fmap fab x5) })
+

From 9d974ee004cf82a2a75782d2df694c7404703bdd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 17:23:14 -0800
Subject: [PATCH 09/12] Improve generated names for tyvar applications

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs | 3 +++
 test/testdata/tactic/FmapBoth.hs.expected                  | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
index 4ab1149f82..8c81bc9f80 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
@@ -29,6 +29,9 @@ mkTyName (tcSplitFunTys -> (_:_, b))
 -- eg. mkTyName (Either A B) = "eab"
 mkTyName (splitTyConApp_maybe -> Just (c, args))
   = mkTyConName c ++ foldMap mkTyName args
+-- eg. mkTyName (f a) = "fa"
+mkTyName (tcSplitAppTys -> (t, args@(_:_)))
+  = mkTyName t ++ foldMap mkTyName args
 -- eg. mkTyName a = "a"
 mkTyName (getTyVar_maybe -> Just tv)
   = occNameString $ occName tv
diff --git a/test/testdata/tactic/FmapBoth.hs.expected b/test/testdata/tactic/FmapBoth.hs.expected
index 13b7e13604..a513b35a42 100644
--- a/test/testdata/tactic/FmapBoth.hs.expected
+++ b/test/testdata/tactic/FmapBoth.hs.expected
@@ -1,4 +1,4 @@
 fmapBoth :: (Functor f, Functor g) => (a -> b) -> (f a, g a) -> (f b, g b)
-fmapBoth = (\ fab p_xx
-   -> case p_xx of { (x, x5) -> (fmap fab x, fmap fab x5) })
+fmapBoth = (\ fab p_faga
+   -> case p_faga of { (fa, ga) -> (fmap fab fa, fmap fab ga) })
 

From cc3fb52b283c9dbc9ac3bf53ce6ebffbf8379d3b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 17:28:03 -0800
Subject: [PATCH 10/12] Minor formatting and haddocks

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs         | 3 +++
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs  | 4 ++--
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs | 3 +--
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 4695d19652..5182161f25 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -132,6 +132,9 @@ commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 
 
+------------------------------------------------------------------------------
+-- | Lift a function over 'HyInfo's to one that takes an 'OccName' and tries to
+-- look it up in the hypothesis.
 useNameFromHypothesis :: (HyInfo CType -> TacticsM a) -> OccName -> TacticsM a
 useNameFromHypothesis f name = do
   hy <- jHypothesis <$> goal
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
index 8c81bc9f80..fbc72dd7be 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
@@ -2,13 +2,13 @@
 
 module Ide.Plugin.Tactic.Naming where
 
-import qualified Data.Set as S
-import Data.Set (Set)
 import           Control.Monad.State.Strict
 import           Data.Bool (bool)
 import           Data.Char
 import           Data.Map (Map)
 import qualified Data.Map as M
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Data.Traversable
 import           Name
 import           TcType
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index 171f0a8749..2274d8f513 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -99,7 +99,6 @@ intros = rule $ \jdg -> do
 -- | Case split, and leave holes in the matches.
 destructAuto :: HyInfo CType -> TacticsM ()
 destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do
-  let name = hi_name hi
   jdg <- goal
   let subtactic = rule $ destruct' (const subgoal) hi
   case isPatternMatch $ hi_provenance hi of
@@ -109,7 +108,7 @@ destructAuto hi = requireConcreteHole $ tracing "destruct(auto)" $ do
             new_hy = foldMap getHyTypes jdgs
             old_hy = getHyTypes jdg
         in case S.null $ new_hy S.\\ old_hy of
-              True  -> Just $ UnhelpfulDestruct name
+              True  -> Just $ UnhelpfulDestruct $ hi_name hi
               False -> Nothing
     False -> subtactic
 

From 69b3ac321b3a097423a5ef8181865293b054973e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 17:36:21 -0800
Subject: [PATCH 11/12] Minor styling

---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
index 533ba74f94..d29229f1ed 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -30,7 +30,7 @@ module Ide.Plugin.Tactic.Judgements
   , hyByName
   ) where
 
-import Control.Arrow
+import           Control.Arrow
 import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char

From bc086bb3deaa2927ba0eb2d3f756b94664f15ad9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 10 Feb 2021 19:37:26 -0800
Subject: [PATCH 12/12] Fix test

---
 plugins/hls-tactics-plugin/test/AutoTupleSpec.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
index 94125c06c4..d1e9a6ce5f 100644
--- a/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
+++ b/plugins/hls-tactics-plugin/test/AutoTupleSpec.hs
@@ -42,7 +42,7 @@ spec = describe "auto for tuple" $ do
           runTactic
             emptyContext
             (mkFirstJudgement
-              (M.singleton (mkVarOcc "x") $ HyInfo UserPrv $ CType in_type)
+              (Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)
               True
               out_type)
             (auto' $ n * 2) `shouldSatisfy` isRight