diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 494865d6ac..5182161f25 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,11 +55,11 @@ 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)
@@ -124,12 +126,24 @@ 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
 
 
+------------------------------------------------------------------------------
+-- | 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
+  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.
@@ -216,10 +230,11 @@ 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) ->
-        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
@@ -287,11 +302,11 @@ judgementForHole state nfp range = do
 
 spliceProvenance
     :: Map OccName Provenance
-    -> Map OccName (HyInfo a)
-    -> Map OccName (HyInfo a)
-spliceProvenance provs =
-  M.mapWithKey $ \name hi ->
-    overProvenance (maybe id const $ M.lookup name provs) hi
+    -> Hypothesis a
+    -> Hypothesis a
+spliceProvenance provs x =
+  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/CodeGen.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/CodeGen.hs
index 0c1633d379..1cab232a7a 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
@@ -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 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/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 75321a170c..d29229f1ed 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements.hs
@@ -26,8 +26,11 @@ module Ide.Plugin.Tactic.Judgements
   , mkFirstJudgement
   , hypothesisFromBindings
   , isTopLevel
+  , hyNamesInScope
+  , hyByName
   ) where
 
+import           Control.Arrow
 import           Control.Lens hiding (Context)
 import           Data.Bool
 import           Data.Char
@@ -48,20 +51,20 @@ 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
   . mapMaybe go
   where
     go (occName -> occ, t)
       | Just ty <- t
-      , isAlpha . head . occNameString $ occ = Just (occ, HyInfo UserPrv $ CType ty)
+      , isAlpha . head . occNameString $ occ = Just $ HyInfo occ UserPrv $ CType ty
       | otherwise = Nothing
 
 
@@ -96,8 +99,8 @@ introducing
     -> Judgement' a
     -> Judgement' a
 introducing f ns =
-  field @"_jHypothesis" <>~ M.fromList (zip [0..] ns <&>
-    \(pos, (name, ty)) -> (name, HyInfo (f pos) ty))
+  field @"_jHypothesis" <>~ (Hypothesis $ zip [0..] ns <&>
+    \(pos, (name, ty)) -> HyInfo name (f pos) ty)
 
 
 ------------------------------------------------------------------------------
@@ -149,7 +152,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 +175,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 +191,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 +206,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,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" %~ (M.mapWithKey $ \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
                            )
@@ -277,20 +281,28 @@ 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
+  . filter (not . isDisallowed . hi_provenance)
+  . unHypothesis
+  . 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
+  . filter (isLocalHypothesis . hi_provenance)
+  . unHypothesis
+  . jHypothesis
 
 
 ------------------------------------------------------------------------------
@@ -304,10 +316,30 @@ unsetIsTopHole :: Judgement' a -> Judgement' a
 unsetIsTopHole = field @"_jIsTopHole" .~ False
 
 
+------------------------------------------------------------------------------
+-- | What names are currently in scope in the hypothesis?
+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
+
+
 ------------------------------------------------------------------------------
 -- | 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 +358,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 559d983e31..dd307da2ca 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
@@ -218,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
@@ -230,8 +232,7 @@ methodHypothesis ty = do
               $ classSCTheta cls
   pure $ mappend sc_methods $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
-    in ( occName method
-       , HyInfo (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/Naming.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
index f6b054f987..fbc72dd7be 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Naming.hs
@@ -7,6 +7,8 @@ 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
@@ -27,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
@@ -61,12 +66,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 +80,14 @@ mkGoodName in_scope t =
 -- | Like 'mkGoodName' but creates several apart names.
 mkManyGoodNames
   :: (Traversable t, Monad m)
-  => M.Map OccName a
+  => Set 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 :)
+    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 60b318c8cc..2274d8f513 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
 
 
 ------------------------------------------------------------------------------
@@ -51,7 +52,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
@@ -63,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..]
 
 
@@ -80,7 +81,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
@@ -96,35 +97,32 @@ 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
   jdg <- goal
-  case M.lookup name $ 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
-                    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 $ hi_name hi
+              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)
 
@@ -148,32 +146,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 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
 
 
 ------------------------------------------------------------------------------
@@ -268,15 +264,19 @@ auto' n = do
     , recursion
     ]
 
-overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
+overFunctions :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overFunctions =
-  attemptOn $ M.keys . M.filter (isFunction . unCType . hi_type) . jHypothesis
+  attemptOn $ filter (isFunction . unCType . hi_type)
+           . unHypothesis
+           . jHypothesis
 
-overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
+overAlgebraicTerms :: (HyInfo CType -> TacticsM ()) -> TacticsM ()
 overAlgebraicTerms =
-  attemptOn $
-    M.keys . M.filter (isJust . algebraicTyCon . unCType . hi_type) . jHypothesis
+  attemptOn $ filter (isJust . algebraicTyCon . unCType . hi_type)
+            . unHypothesis
+            . jHypothesis
 
 
-allNames :: Judgement -> [OccName]
-allNames = M.keys . jHypothesis
+allNames :: Judgement -> Set OccName
+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 c9d1bdd514..ac0ab3dff1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs
@@ -215,10 +215,18 @@ instance Uniquable a => Ord (Uniquely a) where
   compare = nonDetCmpUnique `on` getUnique . getViaUnique
 
 
+newtype Hypothesis a = Hypothesis
+  { unHypothesis :: [HyInfo a]
+  }
+  deriving stock (Functor, Eq, Show, Generic, Ord)
+  deriving newtype (Semigroup, Monoid)
+
+
 ------------------------------------------------------------------------------
 -- | 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,13 +235,13 @@ 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
 
 
 ------------------------------------------------------------------------------
 -- | 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
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
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..a513b35a42
--- /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_faga
+   -> case p_faga of { (fa, ga) -> (fmap fab fa, fmap fab ga) })
+