diff --git a/ghcide/src/Development/IDE/Core/UseStale.hs b/ghcide/src/Development/IDE/Core/UseStale.hs
index 04c1755817..c9f3df3aec 100644
--- a/ghcide/src/Development/IDE/Core/UseStale.hs
+++ b/ghcide/src/Development/IDE/Core/UseStale.hs
@@ -9,6 +9,7 @@ module Development.IDE.Core.UseStale
   , unTrack
   , PositionMap
   , TrackedStale (..)
+  , untrackedStaleValue
   , unsafeMkStale
   , unsafeMkCurrent
   , unsafeCopyAge
@@ -85,6 +86,10 @@ instance Functor TrackedStale where
   fmap f (TrackedStale t pm) = TrackedStale (fmap f t) pm
 
 
+untrackedStaleValue :: TrackedStale a -> a
+untrackedStaleValue (TrackedStale ta _) = coerce ta
+
+
 ------------------------------------------------------------------------------
 -- | A class for which 'Tracked' values can be run across a 'PositionMapping'
 -- to change their ages.
diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
index e1f051f652..1c2f1e399b 100644
--- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
+++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal
@@ -142,6 +142,8 @@ test-suite tests
     , lens
     , mtl
     , text
+    , deepseq
+    , tasty-hunit
   build-tool-depends:
       hspec-discover:hspec-discover
   default-language: Haskell2010
diff --git a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
index 632f6e12e7..f0e8e09ab5 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs
@@ -16,7 +16,6 @@ import           Control.Monad.State
 import           Data.Bool (bool)
 import           Data.Generics.Labels ()
 import           Data.List
-import           Data.Maybe (mapMaybe)
 import           Data.Monoid (Endo(..))
 import qualified Data.Set as S
 import           Data.Traversable
@@ -58,7 +57,7 @@ destructMatches f scrut t jdg = do
         [] -> throwError $ GoalMismatch "destruct" g
         _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let con = RealDataCon dc
-              ev = mapMaybe mkEvidence $ dataConInstArgTys dc apps
+              ev = concatMap mkEvidence $ dataConInstArgTys dc apps
               -- We explicitly do not need to add the method hypothesis to
               -- #syn_scoped
               method_hy = foldMap evidenceToHypothesis ev
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Context.hs b/plugins/hls-tactics-plugin/src/Wingman/Context.hs
index e148fcd1b8..ef133d12ad 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Context.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Context.hs
@@ -1,17 +1,32 @@
 module Wingman.Context where
 
-import Bag
-import Control.Arrow
-import Control.Monad.Reader
-import Development.IDE.GHC.Compat
-import OccName
-import TcRnTypes
-import Wingman.FeatureSet (FeatureSet)
-import Wingman.Types
-
-
-mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
-mkContext features locals tcg = Context
+import           Bag
+import           Control.Arrow
+import           Control.Monad.Reader
+import           Data.Foldable.Extra (allM)
+import           Data.Maybe (fromMaybe, isJust)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
+import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
+import           OccName
+import           TcRnTypes
+import           TcType (tcSplitTyConApp, tcSplitPhiTy)
+import           TysPrim (alphaTys)
+import           Wingman.FeatureSet (FeatureSet)
+import           Wingman.Judgements.Theta
+import           Wingman.Types
+
+
+mkContext
+    :: FeatureSet
+    -> [(OccName, CType)]
+    -> TcGblEnv
+    -> ExternalPackageState
+    -> KnownThings
+    -> [Evidence]
+    -> Context
+mkContext features locals tcg eps kt ev = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
@@ -19,6 +34,13 @@ mkContext features locals tcg = Context
                    . bagToList
                    $ tcg_binds tcg
   , ctxFeatureSet = features
+  , ctxInstEnvs =
+      InstEnvs
+        (eps_inst_env eps)
+        (tcg_inst_env tcg)
+        (tcVisibleOrphanMods tcg)
+  , ctxKnownThings = kt
+  , ctxTheta = evidenceToThetaType ev
   }
 
 
@@ -37,3 +59,55 @@ getFunBindId _ = []
 getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
 getCurrentDefinitions = asks ctxDefiningFuncs
 
+
+------------------------------------------------------------------------------
+-- | Extract something from 'KnownThings'.
+getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a
+getKnownThing f = asks $ f . ctxKnownThings
+
+
+------------------------------------------------------------------------------
+-- | Like 'getInstance', but uses a class from the 'KnownThings'.
+getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))
+getKnownInstance f tys = do
+  cls <- getKnownThing f
+  getInstance cls tys
+
+
+------------------------------------------------------------------------------
+-- | Determine if there is an instance that exists for the given 'Class' at the
+-- specified types. Deeply checks contexts to ensure the instance is actually
+-- real.
+--
+-- If so, this returns a 'PredType' that corresponds to the type of the
+-- dictionary.
+getInstance :: MonadReader Context m => Class -> [Type] -> m (Maybe (Class, PredType))
+getInstance cls tys = do
+  env <- asks ctxInstEnvs
+  let (mres, _, _) = lookupInstEnv False env cls tys
+  case mres of
+    ((inst, mapps) : _) -> do
+      -- Get the instantiated type of the dictionary
+      let df = piResultTys (idType $ is_dfun inst) $ zipWith fromMaybe alphaTys mapps
+      -- pull off its resulting arguments
+      let (theta, df') = tcSplitPhiTy df
+      allM hasClassInstance theta >>= \case
+        True -> pure $ Just (cls, df')
+        False -> pure Nothing
+    _ -> pure Nothing
+
+
+------------------------------------------------------------------------------
+-- | Like 'getInstance', but only returns whether or not it succeeded. Can fail
+-- fast, and uses a cached Theta from the context.
+hasClassInstance :: MonadReader Context m => PredType -> m Bool
+hasClassInstance predty = do
+  theta <- asks ctxTheta
+  case S.member (CType predty) theta of
+    True -> pure True
+    False -> do
+      let (con, apps) = tcSplitTyConApp predty
+      case tyConClass_maybe con of
+        Nothing -> pure False
+        Just cls -> fmap isJust $ getInstance cls apps
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
index a36f2da49a..962e8e5645 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/FeatureSet.hs
@@ -24,6 +24,7 @@ data Feature
   = FeatureDestructAll
   | FeatureUseDataCon
   | FeatureRefineHole
+  | FeatureKnownMonoid
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
index eeead45836..c8b198dc23 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/GHC.hs
@@ -4,7 +4,9 @@
 module Wingman.GHC where
 
 import           ConLike
+import           Control.Applicative (empty)
 import           Control.Monad.State
+import           Control.Monad.Trans.Maybe (MaybeT(..))
 import           Data.Function (on)
 import           Data.Functor ((<&>))
 import           Data.List (isPrefixOf)
@@ -14,10 +16,14 @@ import           Data.Set (Set)
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
+import           Development.IDE (HscEnvEq (hscEnv))
+import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat
 import           GHC.SourceGen (case', lambda, match)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
+import           GhcPlugins (extractModule, GlobalRdrElt (gre_name))
 import           OccName
+import           TcRnMonad
 import           TcType
 import           TyCoRep
 import           Type
@@ -294,3 +300,40 @@ unXPat (XPat (L _ pat)) = unXPat pat
 #endif
 unXPat pat              = pat
 
+
+------------------------------------------------------------------------------
+-- | Build a 'KnownThings'.
+knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings
+knownThings tcg hscenv= do
+  let cls = knownClass tcg hscenv
+  KnownThings
+    <$> cls (mkClsOcc "Semigroup")
+    <*> cls (mkClsOcc "Monoid")
+
+
+------------------------------------------------------------------------------
+-- | Like 'knownThing' but specialized to classes.
+knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class
+knownClass = knownThing $ \case
+  ATyCon tc -> tyConClass_maybe tc
+  _         -> Nothing
+
+
+------------------------------------------------------------------------------
+-- | Helper function for defining 'knownThings'.
+knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a
+knownThing f tcg hscenv occ = do
+  let modul = extractModule tcg
+      rdrenv = tcg_rdr_env tcg
+
+  case lookupOccEnv rdrenv occ of
+    Nothing -> empty
+    Just elts -> do
+      mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts
+      case mvar of
+        Just tt -> liftMaybe $ f tt
+        _ -> empty
+
+liftMaybe :: Monad m => Maybe a -> MaybeT m a
+liftMaybe a = MaybeT $ pure a
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
index 40328c09cf..3d9d89896d 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs
@@ -7,15 +7,18 @@ module Wingman.Judgements.Theta
   , mkEvidence
   , evidenceToSubst
   , evidenceToHypothesis
+  , evidenceToThetaType
   ) where
 
-import           Data.Maybe (fromMaybe, mapMaybe)
+import           Class (classTyVars)
+import           Control.Applicative (empty)
+import           Data.Maybe (fromMaybe, mapMaybe, maybeToList)
 import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.Core.UseStale
 import           Development.IDE.GHC.Compat
-import           Generics.SYB hiding (tyConName)
-import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe)
+import           Generics.SYB hiding (tyConName, empty)
+import           GhcPlugins (mkVarOcc, splitTyConApp_maybe, getTyVar_maybe, zipTvSubst)
 #if __GLASGOW_HASKELL__ > 806
 import           GhcPlugins (eqTyCon)
 #else
@@ -23,6 +26,7 @@ import           GhcPlugins (nameRdrName, tyConName)
 import           PrelNames (eqTyCon_RDR)
 #endif
 import           TcEvidence
+import           TcType (substTy)
 import           TcType (tcTyConAppTyCon_maybe)
 import           TysPrim (eqPrimTyCon)
 import           Wingman.Machinery
@@ -41,19 +45,31 @@ data Evidence
 
 ------------------------------------------------------------------------------
 -- | Given a 'PredType', pull an 'Evidence' out of it.
-mkEvidence :: PredType -> Maybe Evidence
+mkEvidence :: PredType -> [Evidence]
 mkEvidence (getEqualityTheta -> Just (a, b))
-  = Just $ EqualityOfTypes a b
-mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (isClassTyCon -> True))
-  = Just $ HasInstance inst
-mkEvidence _ = Nothing
+  = pure $ EqualityOfTypes a b
+mkEvidence inst@(tcTyConAppTyCon_maybe -> Just (tyConClass_maybe -> Just cls)) = do
+  (_, apps) <- maybeToList $ splitTyConApp_maybe inst
+  let tvs     = classTyVars cls
+      subst   = zipTvSubst tvs apps
+  sc_ev <- traverse (mkEvidence . substTy subst) $ classSCTheta cls
+  HasInstance inst : sc_ev
+mkEvidence _ = empty
+
+
+------------------------------------------------------------------------------
+-- | Build a set of 'PredType's from the evidence.
+evidenceToThetaType :: [Evidence] -> Set CType
+evidenceToThetaType evs = S.fromList $ do
+  HasInstance t <- evs
+  pure $ CType t
 
 
 ------------------------------------------------------------------------------
 -- | Compute all the 'Evidence' implicitly bound at the given 'SrcSpan'.
 getEvidenceAtHole :: Tracked age SrcSpan -> Tracked age (LHsBinds GhcTc) -> [Evidence]
 getEvidenceAtHole (unTrack -> dst)
-  = mapMaybe mkEvidence
+  = concatMap mkEvidence
   . (everything (<>) $
         mkQ mempty (absBinds dst) `extQ` wrapperBinds dst `extQ` matchBinds dst)
   . unTrack
@@ -113,6 +129,8 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name
         -- show
       , "showsPrec"
       , "showList"
+        -- monad
+      , "return"
       ]
 
 
diff --git a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
index 21eb5b3359..0cd72bd62e 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs
@@ -3,20 +3,38 @@ module Wingman.KnownStrategies where
 import Control.Monad.Error.Class
 import OccName (mkVarOcc)
 import Refinery.Tactic
-import Wingman.Context (getCurrentDefinitions)
+import Wingman.Context (getCurrentDefinitions, getKnownInstance)
 import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
 import Wingman.Machinery (tracing)
 import Wingman.Tactics
 import Wingman.Types
+import Wingman.Judgements (jGoal)
+import Data.Foldable (for_)
+import Wingman.FeatureSet
+import Control.Applicative (empty)
+import Control.Monad.Reader.Class (asks)
 
 
 knownStrategies :: TacticsM ()
 knownStrategies = choice
   [ known "fmap" deriveFmap
+  , known "mempty" deriveMempty
   , known "arbitrary" deriveArbitrary
+  , featureGuard FeatureKnownMonoid $ known "<>" deriveMappend
+  , featureGuard FeatureKnownMonoid $ known "mappend" deriveMappend
   ]
 
 
+------------------------------------------------------------------------------
+-- | Guard a tactic behind a feature.
+featureGuard :: Feature -> TacticsM a -> TacticsM a
+featureGuard feat t = do
+  fs <- asks ctxFeatureSet
+  case hasFeature feat fs of
+    True -> t
+    False -> empty
+
+
 known :: String -> TacticsM () -> TacticsM ()
 known name t = do
   getCurrentDefinitions >>= \case
@@ -35,3 +53,45 @@ deriveFmap = do
     , recursion
     ]
 
+
+------------------------------------------------------------------------------
+-- | We derive mappend by binding the arguments, introducing the constructor,
+-- and then calling mappend recursively. At each recursive call, we filter away
+-- any binding that isn't in an analogous position.
+--
+-- The recursive call first attempts to use an instace in scope. If that fails,
+-- it fals back to trying a theta method from the hypothesis with the correct
+-- name.
+deriveMappend :: TacticsM ()
+deriveMappend = do
+  try intros
+  destructAll
+  split
+  g <- goal
+  minst <- getKnownInstance kt_semigroup
+         . pure
+         . unCType
+         $ jGoal g
+  for_ minst $ \(cls, df) -> do
+    restrictPositionForApplication
+      (applyMethod cls df $ mkVarOcc "<>")
+      assumption
+  try $
+    restrictPositionForApplication
+      (applyByName $ mkVarOcc "<>")
+      assumption
+
+
+------------------------------------------------------------------------------
+-- | We derive mempty by introducing the constructor, and then trying to
+-- 'mempty' everywhere. This smaller 'mempty' might come from an instance in
+-- scope, or it might come from the hypothesis theta.
+deriveMempty :: TacticsM ()
+deriveMempty = do
+  split
+  g <- goal
+  minst <- getKnownInstance kt_monoid [unCType $ jGoal g]
+  for_ minst $ \(cls, df) -> do
+    applyMethod cls df $ mkVarOcc "mempty"
+  try assumption
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
index 7f02483734..57ecb60904 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs
@@ -12,12 +12,14 @@ import           Data.Coerce
 import           Data.Functor ((<&>))
 import           Data.Generics.Aliases (mkQ)
 import           Data.Generics.Schemes (everything)
+import           Data.IORef (readIORef)
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Set  as S
 import qualified Data.Text as T
 import           Data.Traversable
+import           Development.IDE (hscEnv)
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Service (runAction)
 import           Development.IDE.Core.Shake (IdeState (..), use)
@@ -29,7 +31,7 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import           Development.Shake (Action, RuleResult)
 import           Development.Shake.Classes (Typeable, Binary, Hashable, NFData)
 import qualified FastString
-import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope)
+import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), liftIO)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
 import           Ide.PluginUtils (usePropertyLsp)
@@ -156,12 +158,21 @@ judgementForHole state nfp range features = do
     HAR _ (unsafeCopyAge asts -> hf) _ _ HieFresh -> do
       range' <- liftMaybe $ mapAgeFrom amapping range
       binds <- runStaleIde state nfp GetBindings
-      tcmod <- fmap (fmap tmrTypechecked)
-             $ runStaleIde state nfp TypeCheck
+      tcg <- fmap (fmap tmrTypechecked)
+           $ runStaleIde state nfp TypeCheck
+      hscenv <- runStaleIde state nfp GhcSessionDeps
 
       (rss, g) <- liftMaybe $ getSpanAndTypeAtHole range' hf
       new_rss <- liftMaybe $ mapAgeTo amapping rss
-      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcmod
+
+      -- KnownThings is just the instances in scope. There are no ranges
+      -- involved, so it's not crucial to track ages.
+      let henv = untrackedStaleValue $ hscenv
+      eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
+      kt <- knownThings (untrackedStaleValue tcg) henv
+
+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext features g binds new_rss tcg eps kt
+
       dflags <- getIdeDynflags state nfp
       pure (fmap realSrcSpanToRange new_rss, jdg, ctx, dflags)
 
@@ -172,8 +183,10 @@ mkJudgementAndContext
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
+    -> ExternalPackageState
+    -> KnownThings
     -> Maybe (Judgement, Context)
-mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) = do
+mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
@@ -183,6 +196,9 @@ mkJudgementAndContext features g (TrackedStale binds bmap) rss (TrackedStale tcg
                 $ unTrack
                 $ getDefiningBindings <$> binds <*> binds_rss)
               (unTrack tcg)
+              eps
+              kt
+              evidence
       top_provs = getRhsPosVals tcg_rss tcs
       local_hy = spliceProvenance top_provs
                $ hypothesisFromBindings binds_rss binds
@@ -216,9 +232,6 @@ getSpanAndTypeAtHole r@(unTrack -> range) (unTrack -> hf) = do
         pure (unsafeCopyAge r $ nodeSpan ast', ty)
 
 
-liftMaybe :: Monad m => Maybe a -> MaybeT m a
-liftMaybe a = MaybeT $ pure a
-
 
 ------------------------------------------------------------------------------
 -- | Combine two (possibly-overlapping) hypotheses; using the provenance from
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
index 1fa209c4ce..34dcb449c6 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Machinery.hs
@@ -243,10 +243,7 @@ methodHypothesis ty = do
   let methods = classMethods cls
       tvs     = classTyVars cls
       subst   = zipTvSubst tvs apps
-  sc_methods <- fmap join
-              $ traverse (methodHypothesis . substTy subst)
-              $ classSCTheta cls
-  pure $ mappend sc_methods $ methods <&> \method ->
+  pure $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
        )
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
index 3f91497e95..f477a2a323 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Tactics.hs
@@ -11,6 +11,7 @@ import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader (ask))
 import           Control.Monad.State.Strict (StateT(..), runStateT)
 import           Data.Foldable
+import           Data.Functor ((<&>))
 import           Data.Generics.Labels ()
 import           Data.List
 import qualified Data.Map as M
@@ -80,6 +81,16 @@ recursion = requireConcreteHole $ tracing "recursion" $ do
       <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
+restrictPositionForApplication :: TacticsM () -> TacticsM () -> TacticsM ()
+restrictPositionForApplication f app = do
+  -- NOTE(sandy): Safe use of head; context is guaranteed to have a defining
+  -- binding
+  name <- head . fmap fst <$> getCurrentDefinitions
+  f <@>
+    fmap
+      (localTactic app . filterPosition name) [0..]
+
+
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
@@ -364,3 +375,23 @@ overAlgebraicTerms =
 allNames :: Judgement -> Set OccName
 allNames = hyNamesInScope . jHypothesis
 
+
+applyMethod :: Class -> PredType -> OccName -> TacticsM ()
+applyMethod cls df method_name = do
+  case find ((== method_name) . occName) $ classMethods cls of
+    Just method -> do
+      let (_, apps) = splitAppTys df
+      let ty = piResultTys (idType method) apps
+      apply $ HyInfo method_name (ClassMethodPrv $ Uniquely cls) $ CType ty
+    Nothing -> throwError $ NotInScope method_name
+
+
+applyByName :: OccName -> TacticsM ()
+applyByName name = do
+  g <- goal
+  choice $ (unHypothesis (jHypothesis g)) <&> \hi ->
+    case hi_name hi == name of
+      True  -> apply hi
+      False -> empty
+
+
diff --git a/plugins/hls-tactics-plugin/src/Wingman/Types.hs b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
index 4db95dd5e1..3077e6d1b3 100644
--- a/plugins/hls-tactics-plugin/src/Wingman/Types.hs
+++ b/plugins/hls-tactics-plugin/src/Wingman/Types.hs
@@ -30,6 +30,7 @@ import           Development.IDE.GHC.Compat hiding (Node)
 import           Development.IDE.GHC.Orphans ()
 import           GHC.Generics
 import           GHC.SourceGen (var)
+import           InstEnv (InstEnvs(..))
 import           OccName
 import           Refinery.Tactic
 import           System.IO.Unsafe (unsafePerformIO)
@@ -392,14 +393,41 @@ data Context = Context
   , ctxModuleFuncs   :: [(OccName, CType)]
     -- ^ Everything defined in the current module
   , ctxFeatureSet    :: FeatureSet
+  , ctxKnownThings   :: KnownThings
+  , ctxInstEnvs      :: InstEnvs
+  , ctxTheta         :: Set CType
+  }
+
+instance Show Context where
+  show (Context {..}) = mconcat
+    [ "Context "
+    , showsPrec 10 ctxDefiningFuncs ""
+    , showsPrec 10 ctxModuleFuncs ""
+    , showsPrec 10 ctxFeatureSet ""
+    , showsPrec 10 ctxTheta ""
+    ]
+
+
+------------------------------------------------------------------------------
+-- | Things we'd like to look up, that don't exist in TysWiredIn.
+data KnownThings = KnownThings
+  { kt_semigroup :: Class
+  , kt_monoid    :: Class
   }
-  deriving stock (Eq, Ord, Show)
 
 
 ------------------------------------------------------------------------------
 -- | An empty context
 emptyContext :: Context
-emptyContext  = Context mempty mempty mempty
+emptyContext
+  = Context
+      { ctxDefiningFuncs = mempty
+      , ctxModuleFuncs = mempty
+      , ctxFeatureSet = mempty
+      , ctxKnownThings = error "empty known things from emptyContext"
+      , ctxInstEnvs = InstEnvs mempty mempty mempty
+      , ctxTheta = mempty
+      }
 
 
 newtype Rose a = Rose (Tree a)
diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
index 2b12243f6c..e4da91f3c0 100644
--- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
+++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs
@@ -16,6 +16,7 @@ import Wingman.FeatureSet (allFeatures)
 spec :: Spec
 spec = do
   let autoTest = goldenTest Auto ""
+      autoTestNoWhitespace = goldenTestNoWhitespace Auto ""
 
   describe "golden" $ do
     autoTest 11  8 "AutoSplitGADT.hs"
@@ -39,7 +40,6 @@ spec = do
     autoTest  2  8 "GoldenShowMapChar.hs"
     autoTest  7  8 "GoldenSuperclass.hs"
     autoTest  2 12 "GoldenSafeHead.hs"
-    autoTest 25 13 "GoldenArbitrary.hs"
     autoTest  2 12 "FmapBoth.hs"
     autoTest  7  8 "RecordCon.hs"
     autoTest  6  8 "NewtypeRecord.hs"
@@ -68,6 +68,19 @@ spec = do
     autoTest  6 10 "AutoThetaRefl.hs"
     autoTest  6  8 "AutoThetaReflDestruct.hs"
 
+  describe "known" $ do
+    autoTest 25 13 "GoldenArbitrary.hs"
+    autoTestNoWhitespace
+              6 10 "KnownBigSemigroup.hs"
+    autoTest  4 10 "KnownThetaSemigroup.hs"
+    autoTest  6 10 "KnownCounterfactualSemigroup.hs"
+    autoTest 10 10 "KnownModuleInstanceSemigroup.hs"
+    autoTest  4 22 "KnownDestructedSemigroup.hs"
+    autoTest  4 10 "KnownMissingSemigroup.hs"
+    autoTest  7 12 "KnownMonoid.hs"
+    autoTest  7 12 "KnownPolyMonoid.hs"
+    autoTest  7 12 "KnownMissingMonoid.hs"
+
 
   describe "messages" $ do
     mkShowMessageTest allFeatures Auto "" 2 8 "MessageForallA.hs" TacticErrors
diff --git a/plugins/hls-tactics-plugin/test/Utils.hs b/plugins/hls-tactics-plugin/test/Utils.hs
index a985b78e7c..37f93e16e2 100644
--- a/plugins/hls-tactics-plugin/test/Utils.hs
+++ b/plugins/hls-tactics-plugin/test/Utils.hs
@@ -7,25 +7,32 @@
 
 module Utils where
 
+import           Control.DeepSeq (deepseq)
+import qualified Control.Exception as E
 import           Control.Lens hiding (failing, (<.>), (.=))
 import           Control.Monad (unless)
 import           Control.Monad.IO.Class
 import           Data.Aeson
 import           Data.Foldable
+import           Data.Function (on)
 import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Text (Text)
+import qualified Data.Text as T
 import qualified Data.Text.IO as T
 import qualified Ide.Plugin.Config as Plugin
-import           Wingman.FeatureSet (FeatureSet, allFeatures, prettyFeatureSet)
-import           Wingman.LanguageServer (mkShowMessageParams)
-import           Wingman.Types
+import           Ide.Plugin.Tactic as Tactic
+import           Language.LSP.Types
 import           Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title)
 import           System.Directory (doesFileExist)
 import           System.FilePath
-import           Test.Hspec
 import           Test.Hls
-import           Ide.Plugin.Tactic as Tactic
+import           Test.Hspec
+import           Test.Hspec.Formatters (FailureReason(ExpectedButGot))
+import           Test.Tasty.HUnit (Assertion, HUnitFailure(..))
+import           Wingman.FeatureSet (FeatureSet, allFeatures, prettyFeatureSet)
+import           Wingman.LanguageServer (mkShowMessageParams)
+import           Wingman.Types
 
 plugin :: PluginDescriptor IdeState
 plugin = Tactic.descriptor "tactics"
@@ -92,14 +99,15 @@ setFeatureSet features = do
 
 
 mkGoldenTest
-    :: FeatureSet
+    :: (Text -> Text -> Assertion)
+    -> FeatureSet
     -> TacticCommand
     -> Text
     -> Int
     -> Int
     -> FilePath
     -> SpecWith ()
-mkGoldenTest features tc occ line col input =
+mkGoldenTest eq features tc occ line col input =
   it (input <> " (golden)") $ do
     runSessionWithServer plugin tacticPath $ do
       setFeatureSet features
@@ -116,7 +124,7 @@ mkGoldenTest features tc occ line col input =
       liftIO $ (doesFileExist expected_name >>=) $ flip unless $ do
         T.writeFile expected_name edited
       expected <- liftIO $ T.readFile expected_name
-      liftIO $ edited `shouldBe` expected
+      liftIO $ edited `eq` expected
 
 mkShowMessageTest
     :: FeatureSet
@@ -142,7 +150,40 @@ mkShowMessageTest features tc occ line col input ufm =
 
 
 goldenTest :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()
-goldenTest = mkGoldenTest allFeatures
+goldenTest = mkGoldenTest shouldBe allFeatures
+
+goldenTestNoWhitespace :: TacticCommand -> Text -> Int -> Int -> FilePath -> SpecWith ()
+goldenTestNoWhitespace = mkGoldenTest shouldBeIgnoringSpaces allFeatures
+
+
+shouldBeIgnoringSpaces :: Text -> Text -> Assertion
+shouldBeIgnoringSpaces = assertFun f ""
+  where
+    f = (==) `on` T.unwords . T.words
+
+
+assertFun
+    :: Show a
+    => (a -> a -> Bool)
+    -> String -- ^ The message prefix
+    -> a      -- ^ The expected value
+    -> a      -- ^ The actual value
+    -> Assertion
+assertFun eq preface expected actual =
+  unless (eq actual expected) $ do
+    (prefaceMsg
+      `deepseq` expectedMsg
+      `deepseq` actualMsg
+      `deepseq`
+        E.throwIO
+          (HUnitFailure Nothing $ show $ ExpectedButGot prefaceMsg expectedMsg actualMsg))
+  where
+    prefaceMsg
+      | null preface = Nothing
+      | otherwise = Just preface
+    expectedMsg = show expected
+    actualMsg = show actual
+
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs
new file mode 100644
index 0000000000..49ea10b8b4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs
@@ -0,0 +1,7 @@
+import Data.Monoid
+
+data Big a = Big [Bool] (Sum Int) String (Endo a) Any
+
+instance Semigroup (Big a) where
+  (<>) = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs.expected
new file mode 100644
index 0000000000..995c5b0f42
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownBigSemigroup.hs.expected
@@ -0,0 +1,13 @@
+import Data.Monoid
+
+data Big a = Big [Bool] (Sum Int) String (Endo a) Any
+
+instance Semigroup (Big a) where
+  (<>) (Big l_b7 si8 l_c9 ea10 a11) (Big l_b si l_c ea a)
+    = Big
+        ((<>) l_b7 l_b)
+        ((<>) si8 si)
+        ((<>) l_c9 l_c)
+        ((<>) ea10 ea)
+        ((<>) a11 a)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs
new file mode 100644
index 0000000000..11e53f4191
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+data Semi = Semi [String] Int
+
+instance Semigroup Int => Semigroup Semi where
+  (<>) = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs.expected
new file mode 100644
index 0000000000..beb49829f1
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownCounterfactualSemigroup.hs.expected
@@ -0,0 +1,8 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+data Semi = Semi [String] Int
+
+instance Semigroup Int => Semigroup Semi where
+  (<>) (Semi l_l_c7 i8) (Semi l_l_c i)
+    = Semi ((<>) l_l_c7 l_l_c) ((<>) i8 i)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs
new file mode 100644
index 0000000000..ed4182c6d9
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs
@@ -0,0 +1,5 @@
+data Test a = Test [a]
+
+instance Semigroup (Test a) where
+  Test a <> Test c = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs.expected
new file mode 100644
index 0000000000..9515b7fd84
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownDestructedSemigroup.hs.expected
@@ -0,0 +1,5 @@
+data Test a = Test [a]
+
+instance Semigroup (Test a) where
+  (<>) (Test a) (Test c) = Test ((<>) a c)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs
new file mode 100644
index 0000000000..7c6bfc5ccd
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs
@@ -0,0 +1,8 @@
+data Mono a = Monoid [String] a
+
+instance Semigroup (Mono a) where
+  (<>) = undefined
+
+instance Monoid (Mono a) where
+  mempty = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs.expected
new file mode 100644
index 0000000000..430db91cba
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingMonoid.hs.expected
@@ -0,0 +1,8 @@
+data Mono a = Monoid [String] a
+
+instance Semigroup (Mono a) where
+  (<>) = undefined
+
+instance Monoid (Mono a) where
+  mempty = Monoid mempty _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs
new file mode 100644
index 0000000000..1193c14a3b
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs
@@ -0,0 +1,5 @@
+data Semi = Semi [String] Int
+
+instance Semigroup Semi where
+  (<>) = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs.expected
new file mode 100644
index 0000000000..07d9a235ec
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMissingSemigroup.hs.expected
@@ -0,0 +1,5 @@
+data Semi = Semi [String] Int
+
+instance Semigroup Semi where
+  (<>) (Semi l_l_c4 i5) (Semi l_l_c i) = Semi ((<>) l_l_c4 l_l_c) _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs
new file mode 100644
index 0000000000..8a03a029af
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs
@@ -0,0 +1,11 @@
+data Foo = Foo
+
+instance Semigroup Foo where
+  (<>) _ _ = Foo
+
+
+data Bar = Bar Foo Foo
+
+instance Semigroup Bar where
+  (<>) = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs.expected
new file mode 100644
index 0000000000..498cca1a04
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownModuleInstanceSemigroup.hs.expected
@@ -0,0 +1,11 @@
+data Foo = Foo
+
+instance Semigroup Foo where
+  (<>) _ _ = Foo
+
+
+data Bar = Bar Foo Foo
+
+instance Semigroup Bar where
+  (<>) (Bar f4 f5) (Bar f f3) = Bar ((<>) f4 f) ((<>) f5 f3)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs b/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs
new file mode 100644
index 0000000000..0667bee28c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs
@@ -0,0 +1,8 @@
+data Mono = Monoid [String]
+
+instance Semigroup Mono where
+  (<>) = undefined
+
+instance Monoid Mono where
+  mempty = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs.expected
new file mode 100644
index 0000000000..6ad1e2bf92
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownMonoid.hs.expected
@@ -0,0 +1,8 @@
+data Mono = Monoid [String]
+
+instance Semigroup Mono where
+  (<>) = undefined
+
+instance Monoid Mono where
+  mempty = Monoid mempty
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs b/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs
new file mode 100644
index 0000000000..8ba7bc6d98
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs
@@ -0,0 +1,8 @@
+data Mono a = Monoid [String] a
+
+instance Semigroup (Mono a) where
+  (<>) = undefined
+
+instance Monoid a => Monoid (Mono a) where
+  mempty = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs.expected
new file mode 100644
index 0000000000..317f2e770b
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownPolyMonoid.hs.expected
@@ -0,0 +1,8 @@
+data Mono a = Monoid [String] a
+
+instance Semigroup (Mono a) where
+  (<>) = undefined
+
+instance Monoid a => Monoid (Mono a) where
+  mempty = Monoid mempty mempty
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs b/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs
new file mode 100644
index 0000000000..f5e38276fe
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs
@@ -0,0 +1,5 @@
+data Semi a = Semi a
+
+instance Semigroup a => Semigroup (Semi a) where
+  (<>) = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs.expected b/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs.expected
new file mode 100644
index 0000000000..9ed929c47c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/KnownThetaSemigroup.hs.expected
@@ -0,0 +1,5 @@
+data Semi a = Semi a
+
+instance Semigroup a => Semigroup (Semi a) where
+  (<>) (Semi a6) (Semi a) = Semi ((<>) a6 a)
+