From 4ed815b6b24430e6a0f4d6b9bfe18e3b683dd937 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 22 Oct 2020 22:58:12 -0700
Subject: [PATCH 01/20] Fix skolem-aware unification

---
 plugins/tactics/hls-tactics-plugin.cabal      |  1 +
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 40 ++++++------
 plugins/tactics/test/UnificationSpec.hs       | 64 +++++++++++++++++++
 3 files changed, 83 insertions(+), 22 deletions(-)
 create mode 100644 plugins/tactics/test/UnificationSpec.hs

diff --git a/plugins/tactics/hls-tactics-plugin.cabal b/plugins/tactics/hls-tactics-plugin.cabal
index 7fecc860c4..b95140fe49 100644
--- a/plugins/tactics/hls-tactics-plugin.cabal
+++ b/plugins/tactics/hls-tactics-plugin.cabal
@@ -84,6 +84,7 @@ test-suite tests
   main-is: Main.hs
   other-modules:
     AutoTupleSpec
+    UnificationSpec
   hs-source-dirs:
       test
   ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index f34aff5abd..1936185830 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -144,22 +144,18 @@ newtype Reward a = Reward a
 
 
 
-------------------------------------------------------------------------------
--- | We need to make sure that we don't try to unify any skolems.
--- To see why, consider the case:
---
--- uhh :: (Int -> Int) -> a
--- uhh f = _
---
--- If we were to apply 'f', then we would try to unify 'Int' and 'a'.
--- This is fine from the perspective of 'tcUnifyTy', but will cause obvious
--- type errors in our use case. Therefore, we need to ensure that our
--- 'TCvSubst' doesn't try to unify skolems.
-checkSkolemUnification :: CType -> CType -> TCvSubst -> RuleM ()
-checkSkolemUnification t1 t2 subst = do
-    skolems <- gets ts_skolems
-    unless (all (flip notElemTCvSubst subst) skolems) $
-      throwError (UnificationError t1 t2)
+tryUnifyUnivarsButNotSkolems :: [TyVar] -> CType -> CType -> Maybe TCvSubst
+tryUnifyUnivarsButNotSkolems skolems goal inst =
+  case tcUnifyTysFG (skolemsOf skolems) [unCType inst] [unCType goal] of
+    Unifiable subst -> pure subst
+    _ -> Nothing
+
+
+skolemsOf :: [TyVar] -> TyVar -> BindFlag
+skolemsOf tvs tv =
+  case elem tv tvs of
+    True  -> Skolem
+    False -> BindMe
 
 
 ------------------------------------------------------------------------------
@@ -167,10 +163,10 @@ checkSkolemUnification t1 t2 subst = do
 unify :: CType -- ^ The goal type
       -> CType -- ^ The type we are trying unify the goal type with
       -> RuleM ()
-unify goal inst =
-    case tcUnifyTy (unCType inst) (unCType goal) of
-      Just subst -> do
-          checkSkolemUnification inst goal subst
-          modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })
-      Nothing -> throwError (UnificationError inst goal)
+unify goal inst = do
+  skolems <- gets ts_skolems
+  case tryUnifyUnivarsButNotSkolems skolems goal inst of
+    Just subst ->
+      modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })
+    Nothing -> throwError (UnificationError inst goal)
 
diff --git a/plugins/tactics/test/UnificationSpec.hs b/plugins/tactics/test/UnificationSpec.hs
new file mode 100644
index 0000000000..15091f33d1
--- /dev/null
+++ b/plugins/tactics/test/UnificationSpec.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module UnificationSpec where
+
+import           Control.Arrow
+import           Data.Bool (bool)
+import           Data.Functor ((<&>))
+import           Data.Traversable
+import           Data.Tuple (swap)
+import           Ide.Plugin.Tactic.Debug
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Types
+import           TcType (tcGetTyVar_maybe, substTy)
+import           Test.Hspec
+import           Test.QuickCheck
+import           Type (mkTyVarTy)
+import           TysPrim (alphaTyVars)
+import           TysWiredIn (mkBoxedTupleTy)
+import Data.Maybe (mapMaybe)
+
+
+instance Show Type where
+  show = unsafeRender
+
+
+spec :: Spec
+spec = describe "unification" $ do
+  it "should be able to unify univars with skolems on either side of the equality" $ do
+    property $ do
+      -- Pick some number of unification vars and skolem
+      n <- choose (1, 1)
+      let (skolems, take n -> univars) = splitAt n $ fmap mkTyVarTy alphaTyVars
+      -- Randomly pair them
+      skolem_uni_pairs <-
+        for (zip skolems univars) randomSwap
+      let (lhs, rhs)
+            = mkBoxedTupleTy *** mkBoxedTupleTy
+            $ unzip skolem_uni_pairs
+      pure $
+        counterexample (show skolems) $
+        counterexample (show lhs) $
+        counterexample (show rhs) $
+          case tryUnifyUnivarsButNotSkolems
+                 (mapMaybe tcGetTyVar_maybe skolems)
+                 (CType lhs)
+                 (CType rhs) of
+            Just subst ->
+              -- For each pair, running the unification over the univar should
+              -- result in the skolem
+              conjoin $ zip univars skolems <&> \(uni, skolem) ->
+                let substd = substTy subst uni
+                 in counterexample (show substd) $
+                    counterexample (show skolem) $
+                      CType substd === CType skolem
+            Nothing -> True === False
+
+
+randomSwap :: (a, a) -> Gen (a, a)
+randomSwap ab = do
+  which <- arbitrary
+  pure $ bool swap id which ab
+
+

From b4cec967de3991fa1a16ab36778e65a71ad7eb2c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 22 Oct 2020 23:12:27 -0700
Subject: [PATCH 02/20] apply' on rank-n functions

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 11 +++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 19 +++++++++----------
 2 files changed, 18 insertions(+), 12 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 7f89e4c0c9..2c8511eec6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -43,8 +43,15 @@ cloneTyVar t =
 ------------------------------------------------------------------------------
 -- | Is this a function type?
 isFunction :: Type -> Bool
-isFunction (tcSplitFunTys -> ((_:_), _)) = True
-isFunction _ = False
+isFunction (tacticsSplitFunTy -> (_, _, [], _)) = False
+isFunction _ = True
+
+
+tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
+tacticsSplitFunTy t
+  = let (vars, theta, t') = tcSplitSigmaTy t
+        (args, res) = tcSplitFunTys t'
+     in (vars, theta, args, res)
 
 ------------------------------------------------------------------------------
 -- | Is this an algebraic type?
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index f00a1087cb..e39c924c95 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -54,15 +54,13 @@ assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
   case M.lookup name $ jHypothesis jdg of
-    Just ty ->
-      case ty == jGoal jdg of
-        True  -> do
-          case M.member name (jPatHypothesis jdg) of
-            True  -> setRecursionFrameData True
-            False -> pure ()
-          useOccName jdg name
-          pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name
-        False -> throwError $ GoalMismatch "assume" g
+    Just ty -> do
+      unify ty $ jGoal jdg
+      case M.member name (jPatHypothesis jdg) of
+        True  -> setRecursionFrameData True
+        False -> pure ()
+      useOccName jdg name
+      pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name
     Nothing -> throwError $ UndefinedHypothesis name
 
 
@@ -167,7 +165,8 @@ apply' f func = tracing ("apply' " <> show func) $ do
         g  = jGoal jdg
     case M.lookup func hy of
       Just (CType ty) -> do
-          let (args, ret) = splitFunTys ty
+          let (_tvs, _, args, ret) = tacticsSplitFunTy ty
+          -- Instantiate fresh univars for _tvs
           unify g (CType ret)
           useOccName jdg func
           (tr, sgs)

From a62bac20ecb38f3c4761ed5ebab69456a8a34275 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 11:39:42 -0700
Subject: [PATCH 03/20] Freshen tyvars when instantianting polymorphic funcs

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 48 ++++++++++++++-----
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  1 +
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 44 ++++++++---------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 29 ++++++++++-
 4 files changed, 84 insertions(+), 38 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 2c8511eec6..816bd7e3e9 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,18 +1,25 @@
-{-# LANGUAGE CPP             #-}
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE ViewPatterns    #-}
+{-# LANGUAGE CPP              #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PatternSynonyms  #-}
+{-# LANGUAGE ViewPatterns     #-}
 
 module Ide.Plugin.Tactic.GHC where
 
-import Data.Maybe (isJust)
-import Development.IDE.GHC.Compat
-import OccName
-import TcType
-import TyCoRep
-import Type
-import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
-import Unique
-import Var
+import           Control.Monad.State
+import           Data.Map (Map)
+import qualified Data.Map as M
+import           Data.Maybe (isJust)
+import           Data.Traversable
+import           Development.IDE.GHC.Compat
+import           Generics.SYB (mkT, everywhere)
+import           Ide.Plugin.Tactic.Types
+import           OccName
+import           TcType
+import           TyCoRep
+import           Type
+import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
+import           Unique
+import           Var
 
 
 tcTyVar_maybe :: Type -> Maybe Var
@@ -53,6 +60,23 @@ tacticsSplitFunTy t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
+
+freshTyvars :: MonadState TacticState m => Type -> m Type
+freshTyvars t = do
+  let (tvs, _, _, _) = tacticsSplitFunTy t
+  reps <- fmap M.fromList
+        $ for tvs $ \tv -> do
+            uniq <- freshUnique
+            pure $ (tv, setTyVarUnique tv uniq)
+  pure $
+    everywhere
+      (mkT $ \tv ->
+        case M.lookup tv reps of
+          Just tv' -> tv'
+          Nothing -> tv
+      ) t
+
+
 ------------------------------------------------------------------------------
 -- | Is this an algebraic type?
 algebraicTyCon :: Type -> Maybe TyCon
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1936185830..3160b2b21f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -170,3 +170,4 @@ unify goal inst = do
       modify (\s -> s { ts_unifier = unionTCvSubst subst (ts_unifier s) })
     Nothing -> throwError (UnificationError inst goal)
 
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e39c924c95..653eb578d7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -64,14 +64,13 @@ assume name = rule $ \jdg -> do
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-
 recursion :: TacticsM ()
 recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
     ensure recursiveCleanup (withRecursionStack tail) $ do
-      (localTactic (apply' (const id) name) $ introducing defs)
+      (localTactic (apply name) $ introducing defs)
         <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
@@ -155,34 +154,29 @@ homoLambdaCase = tracing "homoLambdaCase" $ rule $ destructLambdaCase' (\dc jdg
 
 
 apply :: OccName -> TacticsM ()
-apply = apply' (const id)
-
-
-apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
-apply' f func = tracing ("apply' " <> show func) $ do
+apply func = tracing ("apply' " <> show func) $ do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg
     case M.lookup func hy of
       Just (CType ty) -> do
-          let (_tvs, _, args, ret) = tacticsSplitFunTy ty
-          -- Instantiate fresh univars for _tvs
-          unify g (CType ret)
-          useOccName jdg func
-          (tr, sgs)
-              <- fmap unzipTrace
-               $ traverse ( \(i, t) ->
-                            newSubgoal
-                          . f i
-                          . blacklistingDestruct
-                          . flip withNewGoal jdg
-                          $ CType t
-                          ) $ zip [0..] args
-          pure
-            . (tr, )
-            . noLoc
-            . foldl' (@@) (var' func)
-            $ fmap unLoc sgs
+        ty' <- freshTyvars ty
+        let (_, _, args, ret) = tacticsSplitFunTy ty'
+        unify g (CType ret)
+        useOccName jdg func
+        (tr, sgs)
+            <- fmap unzipTrace
+             $ traverse ( \(i, t) ->
+                          newSubgoal
+                        . blacklistingDestruct
+                        . flip withNewGoal jdg
+                        $ CType t
+                        ) $ zip [0..] args
+        pure
+          . (tr, )
+          . noLoc
+          . foldl' (@@) (var' func)
+          $ fmap unLoc sgs
       Nothing -> do
         throwError $ GoalMismatch "apply" g
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 4d1b802697..e8e725a67f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveFunctor              #-}
@@ -35,6 +36,10 @@ import Refinery.Tactic
 import Type
 import Data.Tree
 import Data.Coerce
+import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
+import System.IO.Unsafe (unsafePerformIO)
+import Control.Monad.State
+import Unique (Unique)
 
 
 ------------------------------------------------------------------------------
@@ -73,12 +78,34 @@ data TacticState = TacticState
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
     , ts_recursion_stack :: ![Bool]
+    , ts_unique_gen :: !UniqSupply
     } deriving stock (Show, Generic)
 
+instance Show UniqSupply where
+  show _ = "<uniqsupply>"
+
+unsafeDefaultUniqueSupply :: UniqSupply
+unsafeDefaultUniqueSupply =
+  unsafePerformIO $ mkSplitUniqSupply '🚒'
+{-# NOINLINE unsafeDefaultUniqueSupply #-}
 
 defaultTacticState :: TacticState
 defaultTacticState =
-  TacticState mempty emptyTCvSubst mempty mempty mempty
+  TacticState
+    { ts_skolems         = mempty
+    , ts_unifier         = emptyTCvSubst
+    , ts_used_vals       = mempty
+    , ts_intro_vals      = mempty
+    , ts_recursion_stack = mempty
+    , ts_unique_gen      = unsafeDefaultUniqueSupply
+    }
+
+
+freshUnique :: MonadState TacticState m => m Unique
+freshUnique = do
+  (uniq, supply) <- gets $ takeUniqFromSupply . ts_unique_gen
+  modify' $! field @"ts_unique_gen" .~ supply
+  pure uniq
 
 
 withRecursionStack

From 4f445858bfe2bc547d7c5662389a1127caac47cf Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 12:27:14 -0700
Subject: [PATCH 04/20] first step towards method invocation

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  1 +
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  | 36 +++++++++++++++----
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  |  4 ++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 22 ++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  4 +++
 5 files changed, 59 insertions(+), 8 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 5750835ef7..e34b9ddc78 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -265,6 +265,7 @@ judgementForHole state nfp range = do
                 $ getDefiningBindings binds rss)
               tcg
       hyps = hypothesisFromBindings rss binds
+          <> M.fromList (contextMethodHypothesis ctx)
   pure ( resulting_range
        , mkFirstJudgement
            hyps
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index 2c8b48227a..0ef95ad3c1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -10,16 +10,38 @@ import Development.IDE.GHC.Compat
 import Ide.Plugin.Tactic.Types
 import OccName
 import TcRnTypes
+import Ide.Plugin.Tactic.GHC (tacticsThetaTy)
+import Ide.Plugin.Tactic.Machinery (methodHypothesis)
+import Data.Maybe (mapMaybe)
 
 
 mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
-mkContext locals
-  = Context locals
-  . fmap splitId
-  . (getFunBindId =<<)
-  . fmap unLoc
-  . bagToList
-  . tcg_binds
+mkContext locals tcg = Context
+  { ctxDefiningFuncs = locals
+  , ctxModuleFuncs = fmap splitId
+                   . (getFunBindId =<<)
+                   . fmap unLoc
+                   . bagToList
+                   $ tcg_binds tcg
+  }
+
+
+contextMethodHypothesis :: Context -> [(OccName, CType)]
+contextMethodHypothesis
+  = join
+  . concatMap
+      ( mapMaybe methodHypothesis
+      . fmap unCType
+      . traceIdX "tacticsTheta"
+      . fmap CType
+      . tacticsThetaTy
+      . unCType
+      . traceIdX "method hypothesis"
+      -- TODO(sandy): unify the poly type with the defined type
+      . snd
+      )
+  -- TODO(sandy): use the defining funcs to find the poly type in module funcs
+  . ctxModuleFuncs
 
 
 splitId :: Id -> (OccName, CType)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 816bd7e3e9..4880e99987 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -6,7 +6,6 @@
 module Ide.Plugin.Tactic.GHC where
 
 import           Control.Monad.State
-import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
@@ -60,6 +59,9 @@ tacticsSplitFunTy t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
+tacticsThetaTy :: Type -> ThetaType
+tacticsThetaTy (tacticsSplitFunTy -> (_, theta, _, _)) = theta
+
 
 freshTyvars :: MonadState TacticState m => Type -> m Type
 freshTyvars t = do
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 3160b2b21f..ec64a70fd8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -17,6 +17,8 @@ module Ide.Plugin.Tactic.Machinery
   ( module Ide.Plugin.Tactic.Machinery
   ) where
 
+import qualified Data.Map as M
+import Data.Map (Map)
 import           Control.Arrow
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
@@ -37,6 +39,11 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import Data.Maybe (mapMaybe)
+import Data.Tuple (swap)
+import Class (Class(classTyVars))
+import Data.Functor ((<&>))
+import OccName (HasOccName(occName))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -171,3 +178,18 @@ unify goal inst = do
     Nothing -> throwError (UnificationError inst goal)
 
 
+methodHypothesis :: PredType -> Maybe [(OccName, CType)]
+methodHypothesis ty = do
+  traceMX "pred ty " $ unsafeRender ty
+  (tc, apps) <- splitTyConApp_maybe ty
+  traceMX "got a tycon" $ unsafeRender tc
+  cls <- tyConClass_maybe tc
+  traceMX "got a cls" $ unsafeRender cls
+  let methods = classMethods cls
+      tvs = classTyVars cls
+      subst = zipTvSubst tvs apps
+  -- TODO(sandy): strip out the theta type from the result
+  traceMX "methods" $ unsafeRender methods
+  pure $ methods <&> \method ->
+    (occName method,  CType $ substTy subst $ idType method)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index e8e725a67f..16804833d7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -225,6 +225,10 @@ data Context = Context
   deriving stock (Eq, Ord)
 
 
+emptyContext :: Context
+emptyContext  = Context mempty mempty
+
+
 newtype Rose a = Rose (Tree a)
   deriving stock (Eq, Functor, Generic)
 

From d98a4712ac757865a5d9fbe06175ff7975e7d2d4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 17:25:53 -0700
Subject: [PATCH 05/20] Cleanup poly and thetatypes for class methods

---
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  | 30 +++++++++++++------
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 11 +++----
 2 files changed, 25 insertions(+), 16 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index 0ef95ad3c1..a9a56d290d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -13,6 +13,9 @@ import TcRnTypes
 import Ide.Plugin.Tactic.GHC (tacticsThetaTy)
 import Ide.Plugin.Tactic.Machinery (methodHypothesis)
 import Data.Maybe (mapMaybe)
+import Data.List
+import TcType (substTy, tcSplitSigmaTy)
+import Unify (tcUnifyTy)
 
 
 mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
@@ -26,22 +29,31 @@ mkContext locals tcg = Context
   }
 
 
+------------------------------------------------------------------------------
+-- | Find all of the class methods that exist from the givens in the context.
 contextMethodHypothesis :: Context -> [(OccName, CType)]
-contextMethodHypothesis
+contextMethodHypothesis ctx
   = join
   . concatMap
       ( mapMaybe methodHypothesis
-      . fmap unCType
-      . traceIdX "tacticsTheta"
-      . fmap CType
       . tacticsThetaTy
       . unCType
-      . traceIdX "method hypothesis"
-      -- TODO(sandy): unify the poly type with the defined type
-      . snd
       )
-  -- TODO(sandy): use the defining funcs to find the poly type in module funcs
-  . ctxModuleFuncs
+  . mapMaybe (definedThetaType ctx)
+  . fmap fst
+  $ ctxDefiningFuncs ctx
+
+
+------------------------------------------------------------------------------
+-- | Given the name of a function that exists in 'ctxDefiningFuncs', get its
+-- theta type.
+definedThetaType :: Context -> OccName -> Maybe CType
+definedThetaType ctx name = do
+  (_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx
+  (_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx
+  let (_, _, poly') = tcSplitSigmaTy poly
+  subst <- tcUnifyTy poly' mono
+  pure $ CType $ substTy subst $ snd $ splitForAllTys poly
 
 
 splitId :: Id -> (OccName, CType)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index ec64a70fd8..42dd8fab02 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -180,16 +180,13 @@ unify goal inst = do
 
 methodHypothesis :: PredType -> Maybe [(OccName, CType)]
 methodHypothesis ty = do
-  traceMX "pred ty " $ unsafeRender ty
   (tc, apps) <- splitTyConApp_maybe ty
-  traceMX "got a tycon" $ unsafeRender tc
   cls <- tyConClass_maybe tc
-  traceMX "got a cls" $ unsafeRender cls
   let methods = classMethods cls
-      tvs = classTyVars cls
-      subst = zipTvSubst tvs apps
-  -- TODO(sandy): strip out the theta type from the result
+      tvs     = classTyVars cls
+      subst   = zipTvSubst tvs apps
   traceMX "methods" $ unsafeRender methods
   pure $ methods <&> \method ->
-    (occName method,  CType $ substTy subst $ idType method)
+    let (_, _, ty) = tcSplitSigmaTy $ idType method
+    in (occName method,  CType $ substTy subst ty)
 

From 68800f664588e48eb1ea92c4c5e1a417959f2e6e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 17:37:22 -0700
Subject: [PATCH 06/20] penalize big extracts

---
 .../tactics/src/Ide/Plugin/Tactic/Machinery.hs  | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 42dd8fab02..d8fbd42aa1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveFunctor         #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE DerivingStrategies    #-}
@@ -44,6 +45,7 @@ import Data.Tuple (swap)
 import Class (Class(classTyVars))
 import Data.Functor ((<&>))
 import OccName (HasOccName(occName))
+import Data.Generics (mkQ, everything, gcount)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -81,7 +83,8 @@ runTactic ctx jdg t =
       (errs, []) -> Left $ take 50 $ errs
       (_, fmap assoc23 -> solns) -> do
         let sorted =
-              sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
+              flip sortBy solns $ comparing $ \((_, ext), (jdg, holes)) ->
+                Down $ scoreSolution ext jdg holes
         case sorted of
           (((tr, ext), _) : _) ->
             Right
@@ -128,21 +131,29 @@ setRecursionFrameData b = do
 
 
 scoreSolution
-    :: TacticState
+    :: LHsExpr GhcPs
+    -> TacticState
     -> [Judgement]
     -> ( Penalize Int  -- number of holes
        , Reward Bool   -- all bindings used
        , Penalize Int  -- number of introduced bindings
        , Reward Int    -- number used bindings
+       , Penalize Int  -- size of extract
        )
-scoreSolution TacticState{..} holes
+scoreSolution ext TacticState{..} holes
   = ( Penalize $ length holes
     , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
     , Penalize $ S.size ts_intro_vals
     , Reward $ S.size ts_used_vals
+    , Penalize $ solutionSize ext
     )
 
 
+solutionSize :: LHsExpr GhcPs -> Int
+solutionSize = everything (+) $ gcount $ mkQ False $ \case
+  (_ :: LHsExpr GhcPs) -> True
+
+
 newtype Penalize a = Penalize a
   deriving (Eq, Ord, Show) via (Down a)
 

From c3ff637fc775a1c23d2487bff569984bac1982b9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 17:49:32 -0700
Subject: [PATCH 07/20] Don't award points for using the ambient hypothesis

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs            |  3 ++-
 plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs    |  3 ++-
 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 11 ++++++++---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs  |  5 ++---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs    |  6 +++---
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs      |  3 +++
 6 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index e34b9ddc78..25874bf242 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -265,10 +265,11 @@ judgementForHole state nfp range = do
                 $ getDefiningBindings binds rss)
               tcg
       hyps = hypothesisFromBindings rss binds
-          <> M.fromList (contextMethodHypothesis ctx)
+      ambient = M.fromList $ contextMethodHypothesis ctx
   pure ( resulting_range
        , mkFirstJudgement
            hyps
+           ambient
            (isRhsHole rss tcs)
            (maybe
               mempty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 89947e1443..28a3bf8274 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -29,7 +29,8 @@ import           Type hiding (Var)
 
 useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
 useOccName jdg name =
-  case M.lookup name $ jHypothesis jdg of
+  -- Only score points if this is in the local hypothesis
+  case M.lookup name $ jLocalHypothesis jdg of
     Just{}  -> modify $ withUsedVals $ S.insert name
     Nothing -> pure ()
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 32ad70bc2e..0666274c88 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -163,7 +163,10 @@ disallowing ns =
 
 
 jHypothesis :: Judgement' a -> Map OccName a
-jHypothesis = _jHypothesis
+jHypothesis = _jHypothesis <> _jAmbientHypothesis
+
+jLocalHypothesis :: Judgement' a -> Map OccName a
+jLocalHypothesis = _jHypothesis
 
 
 isPatVal :: Judgement' a -> OccName -> Bool
@@ -191,13 +194,15 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement
-    :: M.Map OccName CType
+    :: M.Map OccName CType  -- ^ local hypothesis
+    -> M.Map OccName CType  -- ^ ambient hypothesis
     -> Bool  -- ^ are we in the top level rhs hole?
     -> M.Map OccName [[OccName]]  -- ^ existing pos vals
     -> Type
     -> Judgement' CType
-mkFirstJudgement hy top posvals goal = Judgement
+mkFirstJudgement hy ambient top posvals goal = Judgement
   { _jHypothesis        = hy
+  , _jAmbientHypothesis = ambient
   , _jDestructed        = mempty
   , _jPatternVals       = mempty
   , _jBlacklistDestruct = False
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index d8fbd42aa1..cfe74433d1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -142,9 +142,9 @@ scoreSolution
        )
 scoreSolution ext TacticState{..} holes
   = ( Penalize $ length holes
-    , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
+    , Reward   $ S.null $ ts_intro_vals S.\\ ts_used_vals
     , Penalize $ S.size ts_intro_vals
-    , Reward $ S.size ts_used_vals
+    , Reward   $ S.size ts_used_vals
     , Penalize $ solutionSize ext
     )
 
@@ -196,7 +196,6 @@ methodHypothesis ty = do
   let methods = classMethods cls
       tvs     = classTyVars cls
       subst   = zipTvSubst tvs apps
-  traceMX "methods" $ unsafeRender methods
   pure $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in (occName method,  CType $ substTy subst ty)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 653eb578d7..7383d6923c 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -14,6 +14,7 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
+import           Control.Monad (when)
 import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
@@ -56,9 +57,8 @@ assume name = rule $ \jdg -> do
   case M.lookup name $ jHypothesis jdg of
     Just ty -> do
       unify ty $ jGoal jdg
-      case M.member name (jPatHypothesis jdg) of
-        True  -> setRecursionFrameData True
-        False -> pure ()
+      when (M.member name $ jPatHypothesis jdg) $
+        setRecursionFrameData True
       useOccName jdg name
       pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name
     Nothing -> throwError $ UndefinedHypothesis name
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 16804833d7..cfaa32c0fa 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -129,6 +129,9 @@ withIntroducedVals f =
 -- | The current bindings and goal for a hole to be filled by refinery.
 data Judgement' a = Judgement
   { _jHypothesis :: !(Map OccName a)
+  , _jAmbientHypothesis :: !(Map OccName a)
+    -- ^ Things in the hypothesis that were imported. Solutions don't get
+    -- points for using the ambient hypothesis.
   , _jDestructed :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jPatternVals :: !(Set OccName)

From 3254d178155063ef88ad9a2025fb3307baa08693 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 17:52:12 -0700
Subject: [PATCH 08/20] Fix property tests

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

diff --git a/plugins/tactics/test/AutoTupleSpec.hs b/plugins/tactics/test/AutoTupleSpec.hs
index efe37bf09a..9b73c7c2f9 100644
--- a/plugins/tactics/test/AutoTupleSpec.hs
+++ b/plugins/tactics/test/AutoTupleSpec.hs
@@ -43,6 +43,7 @@ spec = describe "auto for tuple" $ do
             (Context [] [])
             (mkFirstJudgement
               (M.singleton (mkVarOcc "x") $ CType in_type)
+              mempty
               True
               mempty
               out_type)

From 435f4edf4ce8d3a4c295427f177b1392fbad63a3 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 17:58:35 -0700
Subject: [PATCH 09/20] Add show tests

---
 test/functional/Tactic.hs                          | 3 +++
 test/testdata/tactic/GoldenShow.hs                 | 2 ++
 test/testdata/tactic/GoldenShow.hs.expected        | 2 ++
 test/testdata/tactic/GoldenShowCompose.hs          | 2 ++
 test/testdata/tactic/GoldenShowCompose.hs.expected | 2 ++
 test/testdata/tactic/GoldenShowMapChar.hs          | 2 ++
 test/testdata/tactic/GoldenShowMapChar.hs.expected | 2 ++
 7 files changed, 15 insertions(+)
 create mode 100644 test/testdata/tactic/GoldenShow.hs
 create mode 100644 test/testdata/tactic/GoldenShow.hs.expected
 create mode 100644 test/testdata/tactic/GoldenShowCompose.hs
 create mode 100644 test/testdata/tactic/GoldenShowCompose.hs.expected
 create mode 100644 test/testdata/tactic/GoldenShowMapChar.hs
 create mode 100644 test/testdata/tactic/GoldenShowMapChar.hs.expected

diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index 275e1b68fe..896f5ccbfe 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -102,6 +102,9 @@ tests = testGroup
   , goldenTest "GoldenGADTAuto.hs"          7 13 Auto ""
   , goldenTest "GoldenSwapMany.hs"          2 12 Auto ""
   , goldenTest "GoldenBigTuple.hs"          4 12 Auto ""
+  , goldenTest "GoldenShow.hs"              2 10 Auto ""
+  , goldenTest "GoldenShowCompose.hs"       2 15 Auto ""
+  , goldenTest "GoldenShowMapChar.hs"       2 8  Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenShow.hs b/test/testdata/tactic/GoldenShow.hs
new file mode 100644
index 0000000000..9ec5e27bcf
--- /dev/null
+++ b/test/testdata/tactic/GoldenShow.hs
@@ -0,0 +1,2 @@
+showMe :: Show a => a -> String
+showMe = _
diff --git a/test/testdata/tactic/GoldenShow.hs.expected b/test/testdata/tactic/GoldenShow.hs.expected
new file mode 100644
index 0000000000..05ba83e9fe
--- /dev/null
+++ b/test/testdata/tactic/GoldenShow.hs.expected
@@ -0,0 +1,2 @@
+showMe :: Show a => a -> String
+showMe = show
diff --git a/test/testdata/tactic/GoldenShowCompose.hs b/test/testdata/tactic/GoldenShowCompose.hs
new file mode 100644
index 0000000000..c99768e4e5
--- /dev/null
+++ b/test/testdata/tactic/GoldenShowCompose.hs
@@ -0,0 +1,2 @@
+showCompose :: Show a => (b -> a) -> b -> String
+showCompose = _
diff --git a/test/testdata/tactic/GoldenShowCompose.hs.expected b/test/testdata/tactic/GoldenShowCompose.hs.expected
new file mode 100644
index 0000000000..373ea6af91
--- /dev/null
+++ b/test/testdata/tactic/GoldenShowCompose.hs.expected
@@ -0,0 +1,2 @@
+showCompose :: Show a => (b -> a) -> b -> String
+showCompose = (\ fba b -> show (fba b))
diff --git a/test/testdata/tactic/GoldenShowMapChar.hs b/test/testdata/tactic/GoldenShowMapChar.hs
new file mode 100644
index 0000000000..8e6e5eae6b
--- /dev/null
+++ b/test/testdata/tactic/GoldenShowMapChar.hs
@@ -0,0 +1,2 @@
+test :: Show a => a -> (String -> b) -> b
+test = _
diff --git a/test/testdata/tactic/GoldenShowMapChar.hs.expected b/test/testdata/tactic/GoldenShowMapChar.hs.expected
new file mode 100644
index 0000000000..8750e4e1f4
--- /dev/null
+++ b/test/testdata/tactic/GoldenShowMapChar.hs.expected
@@ -0,0 +1,2 @@
+test :: Show a => a -> (String -> b) -> b
+test = (\ a fl_cb -> fl_cb (show a))

From 86702957dd5ac8dd08387b4ac8977bc434b66b46 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 18:14:08 -0700
Subject: [PATCH 10/20] Cleanup and haddock

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 11 +++++++-
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  6 ++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 25 ++++++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 18 ++++++++----
 plugins/tactics/test/UnificationSpec.hs       | 28 +++++++++----------
 5 files changed, 58 insertions(+), 30 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 4880e99987..3b66956257 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -53,16 +53,25 @@ isFunction (tacticsSplitFunTy -> (_, _, [], _)) = False
 isFunction _ = True
 
 
+------------------------------------------------------------------------------
+-- | Split a function, also splitting out its quantified variables and theta
+-- context.
 tacticsSplitFunTy :: Type -> ([TyVar], ThetaType, [Type], Type)
 tacticsSplitFunTy t
   = let (vars, theta, t') = tcSplitSigmaTy t
         (args, res) = tcSplitFunTys t'
      in (vars, theta, args, res)
 
+
+------------------------------------------------------------------------------
+-- | Rip the theta context out of a regular type.
 tacticsThetaTy :: Type -> ThetaType
-tacticsThetaTy (tacticsSplitFunTy -> (_, theta, _, _)) = theta
+tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 
 
+------------------------------------------------------------------------------
+-- | Instantiate all of the quantified type variables in a type with fresh
+-- skolems.
 freshTyvars :: MonadState TacticState m => Type -> m Type
 freshTyvars t = do
   let (tvs, _, _, _) = tacticsSplitFunTy t
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 0666274c88..743448dc64 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -162,9 +162,15 @@ disallowing ns =
   field @"_jHypothesis" %~ flip M.withoutKeys (S.fromList ns)
 
 
+------------------------------------------------------------------------------
+-- | The hypothesis, consisting of local terms and the ambient environment
+-- (includes and class methods.)
 jHypothesis :: Judgement' a -> Map OccName a
 jHypothesis = _jHypothesis <> _jAmbientHypothesis
 
+
+------------------------------------------------------------------------------
+-- | Just the local hypothesis.
 jLocalHypothesis :: Judgement' a -> Map OccName a
 jLocalHypothesis = _jHypothesis
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index cfe74433d1..1ba309c0bc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,8 +18,7 @@ module Ide.Plugin.Tactic.Machinery
   ( module Ide.Plugin.Tactic.Machinery
   ) where
 
-import qualified Data.Map as M
-import Data.Map (Map)
+import           Class (Class(classTyVars))
 import           Control.Arrow
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
@@ -28,24 +27,21 @@ import           Control.Monad.State.Class (gets, modify)
 import           Control.Monad.State.Strict (StateT (..))
 import           Data.Coerce
 import           Data.Either
-import           Data.List (intercalate, sortBy)
+import           Data.Functor ((<&>))
+import           Data.Generics (mkQ, everything, gcount)
+import           Data.List (sortBy)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Types
+import           OccName (HasOccName(occName))
 import           Refinery.ProofState
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
-import Data.Maybe (mapMaybe)
-import Data.Tuple (swap)
-import Class (Class(classTyVars))
-import Data.Functor ((<&>))
-import OccName (HasOccName(occName))
-import Data.Generics (mkQ, everything, gcount)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -149,6 +145,9 @@ scoreSolution ext TacticState{..} holes
     )
 
 
+------------------------------------------------------------------------------
+-- | Compute the number of 'LHsExpr' nodes; used as a rough metric for code
+-- size.
 solutionSize :: LHsExpr GhcPs -> Int
 solutionSize = everything (+) $ gcount $ mkQ False $ \case
   (_ :: LHsExpr GhcPs) -> True
@@ -161,7 +160,8 @@ newtype Reward a = Reward a
   deriving (Eq, Ord, Show) via a
 
 
-
+------------------------------------------------------------------------------
+-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
 tryUnifyUnivarsButNotSkolems :: [TyVar] -> CType -> CType -> Maybe TCvSubst
 tryUnifyUnivarsButNotSkolems skolems goal inst =
   case tcUnifyTysFG (skolemsOf skolems) [unCType inst] [unCType goal] of
@@ -169,6 +169,8 @@ tryUnifyUnivarsButNotSkolems skolems goal inst =
     _ -> Nothing
 
 
+------------------------------------------------------------------------------
+-- | Helper method for 'tryUnifyUnivarsButNotSkolems'
 skolemsOf :: [TyVar] -> TyVar -> BindFlag
 skolemsOf tvs tv =
   case elem tv tvs of
@@ -189,6 +191,9 @@ unify goal inst = do
     Nothing -> throwError (UnificationError inst goal)
 
 
+------------------------------------------------------------------------------
+-- | Get the class methods of a 'PredType', correctly dealing with
+-- instantiation of quantified class types.
 methodHypothesis :: PredType -> Maybe [(OccName, CType)]
 methodHypothesis ty = do
   (tc, apps) <- splitTyConApp_maybe ty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index cfaa32c0fa..bf3aa020ae 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -22,23 +22,23 @@ module Ide.Plugin.Tactic.Types
   ) where
 
 import Control.Lens hiding (Context)
-import Data.Generics.Product (field)
 import Control.Monad.Reader
+import Control.Monad.State
+import Data.Coerce
 import Data.Function
+import Data.Generics.Product (field)
 import Data.Map (Map)
 import Data.Set (Set)
+import Data.Tree
 import Development.IDE.GHC.Compat hiding (Node)
 import Development.IDE.Types.Location
 import GHC.Generics
 import Ide.Plugin.Tactic.Debug
 import OccName
 import Refinery.Tactic
+import System.IO.Unsafe (unsafePerformIO)
 import Type
-import Data.Tree
-import Data.Coerce
 import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
-import System.IO.Unsafe (unsafePerformIO)
-import Control.Monad.State
 import Unique (Unique)
 
 
@@ -84,11 +84,15 @@ data TacticState = TacticState
 instance Show UniqSupply where
   show _ = "<uniqsupply>"
 
+
+------------------------------------------------------------------------------
+-- | A 'UniqSupply' to use in 'defaultTacticState'
 unsafeDefaultUniqueSupply :: UniqSupply
 unsafeDefaultUniqueSupply =
   unsafePerformIO $ mkSplitUniqSupply '🚒'
 {-# NOINLINE unsafeDefaultUniqueSupply #-}
 
+
 defaultTacticState :: TacticState
 defaultTacticState =
   TacticState
@@ -101,6 +105,8 @@ defaultTacticState =
     }
 
 
+------------------------------------------------------------------------------
+-- | Generate a new 'Unique'
 freshUnique :: MonadState TacticState m => m Unique
 freshUnique = do
   (uniq, supply) <- gets $ takeUniqFromSupply . ts_unique_gen
@@ -228,6 +234,8 @@ data Context = Context
   deriving stock (Eq, Ord)
 
 
+------------------------------------------------------------------------------
+-- | An empty context
 emptyContext :: Context
 emptyContext  = Context mempty mempty
 
diff --git a/plugins/tactics/test/UnificationSpec.hs b/plugins/tactics/test/UnificationSpec.hs
index 15091f33d1..9351725036 100644
--- a/plugins/tactics/test/UnificationSpec.hs
+++ b/plugins/tactics/test/UnificationSpec.hs
@@ -3,21 +3,21 @@
 
 module UnificationSpec where
 
-import           Control.Arrow
-import           Data.Bool (bool)
-import           Data.Functor ((<&>))
-import           Data.Traversable
-import           Data.Tuple (swap)
-import           Ide.Plugin.Tactic.Debug
-import           Ide.Plugin.Tactic.Machinery
-import           Ide.Plugin.Tactic.Types
-import           TcType (tcGetTyVar_maybe, substTy)
-import           Test.Hspec
-import           Test.QuickCheck
-import           Type (mkTyVarTy)
-import           TysPrim (alphaTyVars)
-import           TysWiredIn (mkBoxedTupleTy)
+import Control.Arrow
+import Data.Bool (bool)
+import Data.Functor ((<&>))
 import Data.Maybe (mapMaybe)
+import Data.Traversable
+import Data.Tuple (swap)
+import Ide.Plugin.Tactic.Debug
+import Ide.Plugin.Tactic.Machinery
+import Ide.Plugin.Tactic.Types
+import TcType (tcGetTyVar_maybe, substTy)
+import Test.Hspec
+import Test.QuickCheck
+import Type (mkTyVarTy)
+import TysPrim (alphaTyVars)
+import TysWiredIn (mkBoxedTupleTy)
 
 
 instance Show Type where

From 92eb184e3f46e980536d74de93997c24bf98019e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 21:35:53 -0700
Subject: [PATCH 11/20] Require apply to introduce new holes

---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 56 ++++++++++++-------
 1 file changed, 36 insertions(+), 20 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7383d6923c..9bb5be4282 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -36,7 +36,7 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (nameOccName, occNameString)
+import           Name (occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -149,36 +149,42 @@ destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (
 ------------------------------------------------------------------------------
 -- | LambdaCase split, using the same data constructor in the matches.
 homoLambdaCase :: TacticsM ()
-homoLambdaCase = tracing "homoLambdaCase" $ rule $ destructLambdaCase' (\dc jdg ->
-  buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
+homoLambdaCase =
+  tracing "homoLambdaCase" $
+    rule $ destructLambdaCase' $ \dc jdg ->
+      buildDataCon jdg dc
+        . snd
+        . splitAppTys
+        . unCType
+        $ jGoal jdg
 
 
 apply :: OccName -> TacticsM ()
 apply func = tracing ("apply' " <> show func) $ do
-  rule $ \jdg -> do
-    let hy = jHypothesis jdg
-        g  = jGoal jdg
-    case M.lookup func hy of
-      Just (CType ty) -> do
-        ty' <- freshTyvars ty
-        let (_, _, args, ret) = tacticsSplitFunTy ty'
+  jdg <- goal
+  let hy = jHypothesis jdg
+      g  = jGoal jdg
+  case M.lookup func hy of
+    Just (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 ( \(i, t) ->
-                          newSubgoal
+            $ traverse ( newSubgoal
                         . blacklistingDestruct
                         . flip withNewGoal jdg
-                        $ CType t
-                        ) $ zip [0..] args
+                        . CType
+                        ) args
         pure
           . (tr, )
           . noLoc
           . foldl' (@@) (var' func)
           $ fmap unLoc sgs
-      Nothing -> do
-        throwError $ GoalMismatch "apply" g
+    Nothing -> do
+      throwError $ GoalMismatch "apply" g
 
 
 ------------------------------------------------------------------------------
@@ -209,10 +215,20 @@ splitAuto = tracing "split(auto)" $ do
       case isSplitWhitelisted jdg of
         True -> choice $ fmap splitDataCon dcs
         False -> do
-          choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-            case null jdgs || any (/= jGoal jdg) (fmap jGoal jdgs) of
-              True  -> Nothing
-              False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+          choice $ flip fmap dcs $ \dc -> requireNewHoles $
+            splitDataCon dc
+
+
+------------------------------------------------------------------------------
+-- | Allow the given tactic to proceed if and only if it introduces holes that
+-- have a different goal than current goal.
+requireNewHoles :: TacticsM () -> TacticsM ()
+requireNewHoles m = do
+  jdg <- goal
+  pruning m $ \jdgs ->
+    case null jdgs || any (/= jGoal jdg) (fmap jGoal jdgs) of
+      True  -> Nothing
+      False -> Just NoProgress
 
 
 ------------------------------------------------------------------------------

From 13c3fccdf55e98d27c1be62ea529a4cfdf692bd5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 23 Oct 2020 21:51:03 -0700
Subject: [PATCH 12/20] Discover superclass methods

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 5 ++++-
 test/functional/Tactic.hs                          | 1 +
 test/testdata/tactic/GoldenSuperclass.hs           | 8 ++++++++
 test/testdata/tactic/GoldenSuperclass.hs.expected  | 8 ++++++++
 4 files changed, 21 insertions(+), 1 deletion(-)
 create mode 100644 test/testdata/tactic/GoldenSuperclass.hs
 create mode 100644 test/testdata/tactic/GoldenSuperclass.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1ba309c0bc..75fa4c49b3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -201,7 +201,10 @@ methodHypothesis ty = do
   let methods = classMethods cls
       tvs     = classTyVars cls
       subst   = zipTvSubst tvs apps
-  pure $ methods <&> \method ->
+  sc_methods <- fmap join
+              $ traverse (methodHypothesis . substTy subst)
+              $ classSCTheta cls
+  pure $ mappend sc_methods $ methods <&> \method ->
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in (occName method,  CType $ substTy subst ty)
 
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index 896f5ccbfe..c386570c10 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -105,6 +105,7 @@ tests = testGroup
   , goldenTest "GoldenShow.hs"              2 10 Auto ""
   , goldenTest "GoldenShowCompose.hs"       2 15 Auto ""
   , goldenTest "GoldenShowMapChar.hs"       2 8  Auto ""
+  , goldenTest "GoldenSuperclass.hs"        7 8  Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenSuperclass.hs b/test/testdata/tactic/GoldenSuperclass.hs
new file mode 100644
index 0000000000..86a9fed7bc
--- /dev/null
+++ b/test/testdata/tactic/GoldenSuperclass.hs
@@ -0,0 +1,8 @@
+class Super a where
+    super :: a
+
+class Super a => Sub a
+
+blah :: Sub a => a
+blah = _
+
diff --git a/test/testdata/tactic/GoldenSuperclass.hs.expected b/test/testdata/tactic/GoldenSuperclass.hs.expected
new file mode 100644
index 0000000000..e0a5dbb565
--- /dev/null
+++ b/test/testdata/tactic/GoldenSuperclass.hs.expected
@@ -0,0 +1,8 @@
+class Super a where
+    super :: a
+
+class Super a => Sub a
+
+blah :: Sub a => a
+blah = super
+

From c11e2455d015840ce36e079e1d5f4a26cad38c17 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 24 Oct 2020 13:48:21 -0700
Subject: [PATCH 13/20] Idiom brackets

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 17 +++++--
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  |  2 +
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  7 +++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 26 ++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 51 +++++++++++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  7 ++-
 7 files changed, 103 insertions(+), 9 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 25874bf242..dcd387a295 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -289,7 +289,7 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e8 $
+        x <- lift $ timeout 2e6 $
           case runTactic ctx jdg
                 $ tac
                 $ mkVarOcc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 28a3bf8274..6c004e3e7d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -1,6 +1,7 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE TupleSections    #-}
-{-# LANGUAGE ViewPatterns     #-}
+{-# LANGUAGE FlexibleContexts  #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TupleSections     #-}
+{-# LANGUAGE ViewPatterns      #-}
 
 module Ide.Plugin.Tactic.CodeGen where
 
@@ -192,6 +193,16 @@ coerceName :: HasOccName a => a -> RdrNameStr
 coerceName = fromString . occNameString . occName
 
 
+------------------------------------------------------------------------------
+-- | Converts a function application into applicative form
+idiomize :: LHsExpr GhcPs -> LHsExpr GhcPs
+idiomize x = noLoc $ case unLoc x of
+   HsApp _ (L _ (HsVar _ (L _ x))) gshgp3 ->
+     op (bvar' $ occName x) "<$>" (unLoc gshgp3)
+   HsApp _ gsigp gshgp3 ->
+     op (unLoc $ idiomize gsigp) "<*>" (unLoc gshgp3)
+   y -> y
+
 
 ------------------------------------------------------------------------------
 -- | Like 'var', but works over standard GHC 'OccName's.
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index a9a56d290d..d9c9058af6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -26,6 +26,8 @@ mkContext locals tcg = Context
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
+  , ctxTypeEnv = tcg_type_env tcg
+  , ctxInstEnv = tcg_inst_env tcg
   }
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 743448dc64..05b03a9314 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -70,6 +70,13 @@ withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
 
+------------------------------------------------------------------------------
+-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing
+-- it.
+withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
+withModifiedGoal f = field @"_jGoal" %~ f
+
+
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 75fa4c49b3..bb32ed5d91 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -33,8 +33,11 @@ import           Data.List (sortBy)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
+import           HscTypes (lookupTypeEnv)
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Types
+import           InstEnv (emptyInstEnv, lookupInstEnv, InstEnvs(InstEnvs))
+import           Module (emptyModuleSet)
 import           OccName (HasOccName(occName))
 import           Refinery.ProofState
 import           Refinery.Tactic
@@ -208,3 +211,26 @@ methodHypothesis ty = do
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in (occName method,  CType $ substTy subst ty)
 
+
+------------------------------------------------------------------------------
+-- | Lookup the given class.
+lookupClass :: MonadReader Context m => Name -> m (Maybe Class)
+lookupClass nm = do
+  tenv <- asks ctxTypeEnv
+  pure $ case lookupTypeEnv tenv nm of
+    Just (ATyCon tc) -> tyConClass_maybe tc
+    Just x -> traceX "found some class" (unsafeRender x) Nothing
+    Nothing          -> trace "NOTHING" Nothing
+
+
+------------------------------------------------------------------------------
+-- | Check if the types have a MPTC instance for the given clas name.;
+hasInstance :: MonadReader Context m => Name -> [Type] -> m Bool
+hasInstance nm tys = do
+  insts <- asks ctxInstEnv
+  lookupClass nm >>= \case
+    Just cls ->
+      case lookupInstEnv False (InstEnvs insts emptyInstEnv emptyModuleSet) cls tys of
+        (matches, _, _) -> pure $ not $ null matches
+    Nothing  -> error $ "hasInstance: CANT FIND CLASS " <> show (occName nm)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 9bb5be4282..1a6df05f41 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -14,11 +14,14 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
+import           Control.Applicative (Alternative((<|>)))
+import           Control.Arrow
 import           Control.Monad (when)
 import           Control.Monad.Except (throwError)
+import           Control.Monad.Extra (unlessM)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
-import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Control.Monad.State.Strict (execStateT, StateT(..), runStateT)
 import           Data.Bool (bool)
 import           Data.List
 import qualified Data.Map as M
@@ -37,6 +40,7 @@ import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
 import           Name (occNameString)
+import           PrelNames (applicativeClassName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -261,6 +265,45 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
+------------------------------------------------------------------------------
+-- | Attempt to run the given tactic in "idiom bracket" mode. For example, if
+-- the current goal is
+--
+--    (_ :: [r])
+--
+-- then @idiom apply@ will remove the applicative context, resulting in a hole:
+--
+--    (_ :: r)
+--
+-- and then use @apply@ to solve it. Let's say this results in:
+--
+--    (f (_ :: a) (_ :: b))
+--
+-- Finally, @idiom@ lifts this back into the original applicative:
+--
+--    (f <$> (_ :: [a]) <*> (_ :: [b]))
+--
+-- Idiom will fail fast if the current goal doesn't have an applicative
+-- instance.
+idiom :: TacticsM () -> TacticsM ()
+idiom m = do
+  jdg <- goal
+  case splitAppTy_maybe $ unCType $ jGoal jdg of
+    Just (applic, ty) -> do
+      -- TODO(sandy): make sure this check works
+      -- unlessM (hasInstance applicativeClassName [applic]) $
+      --   throwError $ GoalMismatch "idiom" $ CType applic
+      rule $ fmap (second idiomize) . flip subgoalWith m . withNewGoal (CType ty)
+      rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType)
+    Nothing -> throwError $ GoalMismatch "idiom" $ jGoal jdg
+
+
+
+
+subgoalWith :: Judgement -> TacticsM () -> RuleM (Trace, LHsExpr GhcPs)
+subgoalWith jdg t = RuleT $ flip execStateT jdg $ unTacticT t
+
+
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
@@ -268,12 +311,14 @@ auto' n = do
   try intros
   choice
     [ overFunctions $ \fname -> do
-        apply fname
+        idiom (apply fname) <|> apply fname
         loop
     , overAlgebraicTerms $ \aname -> do
         destructAuto aname
         loop
-    , splitAuto >> loop
+    , do
+        idiom splitAuto <|> splitAuto
+        loop
     , assumption >> loop
     , recursion
     ]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index bf3aa020ae..33bcca8dae 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -40,6 +40,8 @@ import System.IO.Unsafe (unsafePerformIO)
 import Type
 import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
 import Unique (Unique)
+import InstEnv (emptyInstEnv, InstEnv)
+import HscTypes (emptyTypeEnv, TypeEnv)
 
 
 ------------------------------------------------------------------------------
@@ -230,14 +232,15 @@ data Context = Context
     -- ^ The functions currently being defined
   , ctxModuleFuncs :: [(OccName, CType)]
     -- ^ Everything defined in the current module
+  , ctxTypeEnv :: TypeEnv
+  , ctxInstEnv :: InstEnv
   }
-  deriving stock (Eq, Ord)
 
 
 ------------------------------------------------------------------------------
 -- | An empty context
 emptyContext :: Context
-emptyContext  = Context mempty mempty
+emptyContext  = Context mempty mempty emptyTypeEnv emptyInstEnv
 
 
 newtype Rose a = Rose (Tree a)

From 9d69311aeb689cfbe0d27052971b8f67c4bf094e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 24 Oct 2020 14:14:13 -0700
Subject: [PATCH 14/20] Fix test

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

diff --git a/plugins/tactics/test/AutoTupleSpec.hs b/plugins/tactics/test/AutoTupleSpec.hs
index 9b73c7c2f9..8c7bc17c34 100644
--- a/plugins/tactics/test/AutoTupleSpec.hs
+++ b/plugins/tactics/test/AutoTupleSpec.hs
@@ -40,7 +40,7 @@ spec = describe "auto for tuple" $ do
       pure $
           -- We should always be able to find a solution
           runTactic
-            (Context [] [])
+            emptyContext
             (mkFirstJudgement
               (M.singleton (mkVarOcc "x") $ CType in_type)
               mempty

From 360c81231eb0137de67a9276e94673237ee4c2e5 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Oct 2020 16:08:49 -0700
Subject: [PATCH 15/20] Only idiomize on HsApp

---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 6 +++++-
 test/testdata/tactic/GoldenListFmap.hs.expected  | 5 +----
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 6b09347526..e8571b6076 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -294,7 +294,11 @@ idiom m = do
       -- TODO(sandy): make sure this check works
       -- unlessM (hasInstance applicativeClassName [applic]) $
       --   throwError $ GoalMismatch "idiom" $ CType applic
-      rule $ fmap (second idiomize) . flip subgoalWith m . withNewGoal (CType ty)
+      rule $ \jdg -> do
+        (tr, expr) <- subgoalWith (withNewGoal (CType ty) jdg) m
+        case unLoc expr of
+          HsApp{} -> pure (tr, idiomize expr)
+          _       -> throwError $ GoalMismatch "idiom" $ jGoal jdg
       rule $ newSubgoal . withModifiedGoal (CType . mkAppTy applic . unCType)
     Nothing -> throwError $ GoalMismatch "idiom" $ jGoal jdg
 
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
index 6d183a9578..bc70bec5e2 100644
--- a/test/testdata/tactic/GoldenListFmap.hs.expected
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -1,5 +1,2 @@
 fmapList :: (a -> b) -> [a] -> [b]
-fmapList = (\ fab l_a
-   -> case l_a of
-        [] -> []
-        (a : l_a3) -> fab a : fmapList fab l_a3)
+fmapList = (\ fab l_a -> fab <$> l_a)

From a8549589bb2c4660ec4757dc03100656da996a02 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Oct 2020 23:40:56 -0700
Subject: [PATCH 16/20] Disallow idiom brackets when defining ap and fmap

---
 .../tactics/src/Ide/Plugin/Tactic/Machinery.hs  | 17 ++++++++++++++++-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs    |  2 +-
 test/functional/Tactic.hs                       |  2 +-
 test/testdata/tactic/GoldenListFmap.hs          |  4 ++--
 test/testdata/tactic/GoldenListFmap.hs.expected |  7 +++++--
 5 files changed, 25 insertions(+), 7 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 31b05c7258..009b40782b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -31,6 +31,7 @@ import           Data.Functor ((<&>))
 import           Data.Generics (mkQ, everything, gcount)
 import           Data.List (sortBy)
 import           Data.Ord (comparing, Down(..))
+import           Data.Set (Set)
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
 import           HscTypes (lookupTypeEnv)
@@ -38,7 +39,7 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Types
 import           InstEnv (emptyInstEnv, lookupInstEnv, InstEnvs(InstEnvs))
 import           Module (emptyModuleSet)
-import           OccName (HasOccName(occName))
+import           OccName (mkVarOcc, HasOccName(occName))
 import           Refinery.ProofState
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
@@ -247,3 +248,17 @@ requireConcreteHole m = do
     0 -> m
     _ -> throwError TooPolymorphic
 
+
+------------------------------------------------------------------------------
+-- | Prevent the tactic from running when deriving a function with a name in
+-- the given set. Useful for preventing bottoms.
+disallowWhenDeriving
+    :: Set String
+    -> TacticsM a
+    -> TacticsM a
+disallowWhenDeriving what m = do
+  defs <- asks $ S.fromList . fmap fst . ctxDefiningFuncs
+  case S.null $ defs S.\\ S.map mkVarOcc what of
+    True  -> m
+    False -> throwError NoProgress
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e8571b6076..dcea53ccf1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -287,7 +287,7 @@ localTactic t f = do
 -- Idiom will fail fast if the current goal doesn't have an applicative
 -- instance.
 idiom :: TacticsM () -> TacticsM ()
-idiom m = do
+idiom m = disallowWhenDeriving (S.fromList ["fmap", "<*>", "liftA2"]) $ do
   jdg <- goal
   case splitAppTy_maybe $ unCType $ jGoal jdg of
     Just (applic, ty) -> do
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index b722646336..607ff9fab8 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -93,7 +93,7 @@ tests = testGroup
   , goldenTest "GoldenEitherHomomorphic.hs" 2 15 Auto ""
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
-  , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
+  , goldenTest "GoldenListFmap.hs"          2 8  Auto ""
   , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
   , goldenTest "GoldenFoldr.hs"             2 10 Auto ""
   , goldenTest "GoldenSwap.hs"              2 8  Auto ""
diff --git a/test/testdata/tactic/GoldenListFmap.hs b/test/testdata/tactic/GoldenListFmap.hs
index 85293daaf4..4dbfb72199 100644
--- a/test/testdata/tactic/GoldenListFmap.hs
+++ b/test/testdata/tactic/GoldenListFmap.hs
@@ -1,2 +1,2 @@
-fmapList :: (a -> b) -> [a] -> [b]
-fmapList = _
+fmap :: (a -> b) -> [a] -> [b]
+fmap = _
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
index bc70bec5e2..aa562b96b3 100644
--- a/test/testdata/tactic/GoldenListFmap.hs.expected
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -1,2 +1,5 @@
-fmapList :: (a -> b) -> [a] -> [b]
-fmapList = (\ fab l_a -> fab <$> l_a)
+fmap :: (a -> b) -> [a] -> [b]
+fmap = (\ fab l_a
+   -> case l_a of
+        [] -> []
+        (a : l_a3) -> fab a : fmap fab l_a3)

From c2e2fd1178ecc37337010de85d9d6b2da8ee79cb Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Oct 2020 12:31:34 -0700
Subject: [PATCH 17/20] Support towards resolving instances

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 14 ++++--
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  | 13 ++++--
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 39 +++++++++++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 46 +++++++++----------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  5 +-
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 32 ++++++++++---
 6 files changed, 103 insertions(+), 46 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index dcd387a295..75363f7e2e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -31,6 +31,7 @@ import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
+import           Development.IDE (HscEnvEq(hscEnv))
 import           Development.IDE.Core.PositionMapping
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Service (runAction)
@@ -258,11 +259,13 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  (hsc, _) <- MaybeT $ runIde state $ useWithStale GhcSession nfp
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
+              (hscEnv hsc)
               tcg
       hyps = hypothesisFromBindings rss binds
       ambient = M.fromList $ contextMethodHypothesis ctx
@@ -289,11 +292,12 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e6 $
-          case runTactic ctx jdg
-                $ tac
-                $ mkVarOcc
-                $ T.unpack var_name of
+        x <- lift $ timeout 2e6 $ do
+          res <- runTactic ctx jdg
+               $ tac
+               $ mkVarOcc
+               $ T.unpack var_name
+          case res of
             Left err ->
               pure $ (, Nothing)
                 $ Left
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index d9c9058af6..936a8173f3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -16,21 +16,26 @@ import Data.Maybe (mapMaybe)
 import Data.List
 import TcType (substTy, tcSplitSigmaTy)
 import Unify (tcUnifyTy)
+import TcRnMonad (initTcWithGbl)
+import SrcLoc
+import FastString (fsLit)
 
 
-mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
-mkContext locals tcg = Context
+mkContext :: [(OccName, CType)] -> HscEnv -> TcGblEnv -> Context
+mkContext locals env tcg = Context
   { ctxDefiningFuncs = locals
   , ctxModuleFuncs = fmap splitId
                    . (getFunBindId =<<)
                    . fmap unLoc
                    . bagToList
                    $ tcg_binds tcg
-  , ctxTypeEnv = tcg_type_env tcg
-  , ctxInstEnv = tcg_inst_env tcg
+  , ctxRunTcM = \tcr -> do
+      let loc = mkRealSrcLoc (fsLit "generated") 0 0
+      fmap snd $ initTcWithGbl env tcg (mkRealSrcSpan loc loc) tcr
   }
 
 
+
 ------------------------------------------------------------------------------
 -- | Find all of the class methods that exist from the givens in the context.
 contextMethodHypothesis :: Context -> [(OccName, CType)]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 3b66956257..870035e727 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -5,6 +5,7 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import Control.Arrow
 import           Control.Monad.State
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
@@ -16,9 +17,15 @@ import           OccName
 import           TcType
 import           TyCoRep
 import           Type
-import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
+import           TysWiredIn (unitTy, intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
+import TcRnMonad
+import TcEvidence (TcEvBinds (..), evBindMapBinds, TcEvBinds(TcEvBinds))
+import TcEnv (tcLookupTyCon)
+import Id (mkVanillaGlobal)
+import TcSMonad (runTcS)
+import TcSimplify (solveWanteds)
 
 
 tcTyVar_maybe :: Type -> Maybe Var
@@ -148,3 +155,33 @@ getPatName (fromPatCompat -> p0) =
 #endif
     _             -> Nothing
 
+
+-- Generates the evidence for `Show ()`.
+generateDictionary :: Name -> [Type] -> TcM (Var, TcEvBinds)
+generateDictionary cls tys = do
+  traceMX "generating a dict for" $ unsafeRender (cls, tys)
+  showTyCon <- tcLookupTyCon cls
+  dictName <- newName $ mkDictOcc $ mkVarOcc "magic"
+  let dict_ty  = mkTyConApp showTyCon tys
+      dict_var = mkVanillaGlobal dictName dict_ty
+  traceMX "looking for a dict: " $ CType dict_ty
+  ev <- getDictionaryBindings dict_var
+  return (dict_var, ev)
+
+
+-- Pass in a variable `x` which has type `Show ()` (for example) to generate
+-- evidence for `Show ()` which will be bound to `x`.
+getDictionaryBindings :: Var -> TcM TcEvBinds
+getDictionaryBindings dict_var = do
+    loc <- getCtLocM (GivenOrigin UnkSkol) Nothing
+    let nonC = mkNonCanonical CtWanted
+            { ctev_pred = varType dict_var
+            , ctev_nosh = WDeriv
+            , ctev_dest = EvVarDest dict_var
+            , ctev_loc = loc
+            }
+        wCs = mkSimpleWC [cc_ev nonC]
+    traceMX "looking for a wanted: " $ unsafeRender wCs
+    (_, evBinds) <- second evBindMapBinds <$> runTcS (solveWanteds wCs)
+    return (EvBinds evBinds)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 009b40782b..f5aa5d1e3c 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -46,6 +46,10 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import TcEnv (tcLookupGlobal)
+import Ide.Plugin.Tactic.GHC (generateDictionary)
+import TcEvidence (TcEvBinds(EvBinds))
+import Bag (isEmptyBag)
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -72,14 +76,14 @@ runTactic
     :: Context
     -> Judgement
     -> TacticsM ()       -- ^ Tactic to use
-    -> Either [TacticError] RunTacticResults
-runTactic ctx jdg t =
+    -> IO (Either [TacticError] RunTacticResults)
+runTactic ctx jdg t = do
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
         tacticState = defaultTacticState { ts_skolems = skolems }
-    in case partitionEithers
-          . flip runReader ctx
+    res <- flip runReaderT ctx
           . unExtractM
-          $ runTacticT t jdg tacticState of
+          $ runTacticT t jdg tacticState
+    pure $ case partitionEithers res of
       (errs, []) -> Left $ take 50 $ errs
       (_, fmap assoc23 -> solns) -> do
         let sorted =
@@ -213,27 +217,20 @@ methodHypothesis ty = do
     in (occName method,  CType $ substTy subst ty)
 
 
-------------------------------------------------------------------------------
--- | Lookup the given class.
-lookupClass :: MonadReader Context m => Name -> m (Maybe Class)
-lookupClass nm = do
-  tenv <- asks ctxTypeEnv
-  pure $ case lookupTypeEnv tenv nm of
-    Just (ATyCon tc) -> tyConClass_maybe tc
-    Just x -> traceX "found some class" (unsafeRender x) Nothing
-    Nothing          -> trace "NOTHING" Nothing
-
-
 ------------------------------------------------------------------------------
 -- | Check if the types have a MPTC instance for the given clas name.;
-hasInstance :: MonadReader Context m => Name -> [Type] -> m Bool
+hasInstance :: MonadTc m => Name -> [Type] -> m Bool
 hasInstance nm tys = do
-  insts <- asks ctxInstEnv
-  lookupClass nm >>= \case
-    Just cls ->
-      case lookupInstEnv False (InstEnvs insts emptyInstEnv emptyModuleSet) cls tys of
-        (matches, _, _) -> pure $ not $ null matches
-    Nothing  -> error $ "hasInstance: CANT FIND CLASS " <> show (occName nm)
+  traceMX "looking for an instance" $ unsafeRender (nm, tys)
+  liftTc (generateDictionary nm tys) >>= \case
+    Just (_, ev) -> do
+      case ev of
+        EvBinds bag -> do
+          pure $ not $ isEmptyBag bag
+        _ -> pure False
+    Nothing -> do
+      traceMX "no instance" $ unsafeRender nm
+      pure False
 
 
 --------------------------------------------------------------------------------
@@ -258,7 +255,6 @@ disallowWhenDeriving
     -> TacticsM a
 disallowWhenDeriving what m = do
   defs <- asks $ S.fromList . fmap fst . ctxDefiningFuncs
-  case S.null $ defs S.\\ S.map mkVarOcc what of
+  case S.null $ S.intersection defs $ S.map mkVarOcc what of
     True  -> m
     False -> throwError NoProgress
-
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index dcea53ccf1..7e899b97ca 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -287,11 +287,10 @@ localTactic t f = do
 -- Idiom will fail fast if the current goal doesn't have an applicative
 -- instance.
 idiom :: TacticsM () -> TacticsM ()
-idiom m = disallowWhenDeriving (S.fromList ["fmap", "<*>", "liftA2"]) $ do
+idiom m = do -- disallowWhenDeriving (S.fromList ["fmap", "<*>", "liftA2"]) $ do
   jdg <- goal
   case splitAppTy_maybe $ unCType $ jGoal jdg of
     Just (applic, ty) -> do
-      -- TODO(sandy): make sure this check works
       -- unlessM (hasInstance applicativeClassName [applic]) $
       --   throwError $ GoalMismatch "idiom" $ CType applic
       rule $ \jdg -> do
@@ -303,8 +302,6 @@ idiom m = disallowWhenDeriving (S.fromList ["fmap", "<*>", "liftA2"]) $ do
     Nothing -> throwError $ GoalMismatch "idiom" $ jGoal jdg
 
 
-
-
 subgoalWith :: Judgement -> TacticsM () -> RuleM (Trace, LHsExpr GhcPs)
 subgoalWith jdg t = RuleT $ flip execStateT jdg $ unTacticT t
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 6780c9e083..1086b93a06 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,12 +1,13 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE TypeApplications           #-}
 {-# LANGUAGE TypeSynonymInstances       #-}
 {-# OPTIONS_GHC -fno-warn-orphans       #-}
 
@@ -42,6 +43,7 @@ import System.IO.Unsafe (unsafePerformIO)
 import Type
 import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
 import Unique (Unique)
+import TcRnMonad (TcM)
 
 
 ------------------------------------------------------------------------------
@@ -156,7 +158,7 @@ data Judgement' a = Judgement
 type Judgement = Judgement' CType
 
 
-newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
+newtype ExtractM a = ExtractM { unExtractM :: ReaderT Context IO a }
     deriving (Functor, Applicative, Monad, MonadReader Context)
 
 ------------------------------------------------------------------------------
@@ -235,15 +237,31 @@ data Context = Context
     -- ^ The functions currently being defined
   , ctxModuleFuncs :: [(OccName, CType)]
     -- ^ Everything defined in the current module
-  , ctxTypeEnv :: TypeEnv
-  , ctxInstEnv :: InstEnv
+  , ctxRunTcM  :: forall x. TcM x -> IO (Maybe x)
   }
 
 
+------------------------------------------------------------------------------
+-- | Allows us to run TcM without directly exposing MonadIO.
+class Monad m => MonadTc m where
+  liftTc :: TcM a -> m (Maybe a)
+
+instance MonadTc ExtractM where
+  liftTc tcm = do
+    runtc <- asks ctxRunTcM
+    ExtractM $ liftIO $ runtc tcm
+
+instance MonadTc RuleM where
+  liftTc = lift . liftTc
+
+instance MonadTc TacticsM where
+  liftTc = lift . liftTc
+
+
 ------------------------------------------------------------------------------
 -- | An empty context
 emptyContext :: Context
-emptyContext  = Context mempty mempty emptyTypeEnv emptyInstEnv
+emptyContext  = Context mempty mempty (error "can't runTcM")
 
 
 newtype Rose a = Rose (Tree a)

From 81ba3c743145fbbd6e2d79364f8be82f85664fa7 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 26 Oct 2020 23:09:52 -0700
Subject: [PATCH 18/20] Aggressive branch pruning for idioms and class methods

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  | 43 ++++++++++++++++++-
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  |  2 -
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 -
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 25 +++++++----
 .../tactic/GoldenApplicativeThen.hs.expected  |  2 +-
 6 files changed, 60 insertions(+), 16 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 75363f7e2e..54b0ad9028 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -292,7 +292,7 @@ tacticCmd tac lf state (TacticParams uri range var_name)
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range
         let span = rangeToRealSrcSpan (fromNormalizedFilePath nfp) range'
         pm <- MaybeT $ useAnnotatedSource "tacticsCmd" state nfp
-        x <- lift $ timeout 2e6 $ do
+        x <- lift $ timeout 2e8 $ do
           res <- runTactic ctx jdg
                $ tac
                $ mkVarOcc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index 936a8173f3..8286aa7560 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -3,6 +3,8 @@
 
 module Ide.Plugin.Tactic.Context where
 
+import qualified Data.Set as S
+import Data.Set (Set)
 import Bag
 import Control.Arrow
 import Control.Monad.Reader
@@ -40,7 +42,8 @@ mkContext locals env tcg = Context
 -- | Find all of the class methods that exist from the givens in the context.
 contextMethodHypothesis :: Context -> [(OccName, CType)]
 contextMethodHypothesis ctx
-  = join
+  = excludeForbiddenMethods
+  . join
   . concatMap
       ( mapMaybe methodHypothesis
       . tacticsThetaTy
@@ -51,6 +54,44 @@ contextMethodHypothesis ctx
   $ ctxDefiningFuncs 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, CType)] -> [(OccName, CType)]
+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
+  where
+    forbiddenMethods :: Set OccName
+    forbiddenMethods = S.map mkVarOcc $ S.fromList
+      [ -- applicative methods
+        "<*"
+      , "<$"
+        -- monad methods
+      , ">>"
+      , "return"
+        -- foldable methods
+      , "foldMap'"
+      , "foldr"
+      , "foldl"
+      , "foldr'"
+      , "foldl'"
+      , "foldr1"
+      , "foldl1"
+      , "maximum"
+      , "minimum"
+      , "sum"
+      , "product"
+      , "elem"
+      , "null"
+      , "mapM"
+        -- traversable methods
+      , "sequence"
+      , "pass"
+      , "censor"
+      , "state"
+      ]
+
+
 ------------------------------------------------------------------------------
 -- | Given the name of a function that exists in 'ctxDefiningFuncs', get its
 -- theta type.
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 870035e727..462e17e75b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -159,12 +159,10 @@ getPatName (fromPatCompat -> p0) =
 -- Generates the evidence for `Show ()`.
 generateDictionary :: Name -> [Type] -> TcM (Var, TcEvBinds)
 generateDictionary cls tys = do
-  traceMX "generating a dict for" $ unsafeRender (cls, tys)
   showTyCon <- tcLookupTyCon cls
   dictName <- newName $ mkDictOcc $ mkVarOcc "magic"
   let dict_ty  = mkTyConApp showTyCon tys
       dict_var = mkVanillaGlobal dictName dict_ty
-  traceMX "looking for a dict: " $ CType dict_ty
   ev <- getDictionaryBindings dict_var
   return (dict_var, ev)
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index f5aa5d1e3c..03afe6ec3b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -221,7 +221,6 @@ methodHypothesis ty = do
 -- | Check if the types have a MPTC instance for the given clas name.;
 hasInstance :: MonadTc m => Name -> [Type] -> m Bool
 hasInstance nm tys = do
-  traceMX "looking for an instance" $ unsafeRender (nm, tys)
   liftTc (generateDictionary nm tys) >>= \case
     Just (_, ev) -> do
       case ev of
@@ -229,7 +228,6 @@ hasInstance nm tys = do
           pure $ not $ isEmptyBag bag
         _ -> pure False
     Nothing -> do
-      traceMX "no instance" $ unsafeRender nm
       pure False
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7e899b97ca..2cb7a5db5e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -115,7 +115,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
     False ->
-      let subtactic = rule $ destruct' (const subgoal) name
+      let subtactic = rule $ destruct' (const $ newSubgoal . disallowing [name]) name
        in case isPatVal jdg name of
             True ->
               pruning subtactic $ \jdgs ->
@@ -134,7 +134,7 @@ destruct name = requireConcreteHole $ tracing "destruct(user)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
-    False -> rule $ \jdg -> destruct' (const subgoal) name jdg
+    False -> rule $ \jdg -> destruct' (const newSubgoal) name jdg
 
 
 ------------------------------------------------------------------------------
@@ -289,10 +289,13 @@ localTactic t f = do
 idiom :: TacticsM () -> TacticsM ()
 idiom m = do -- disallowWhenDeriving (S.fromList ["fmap", "<*>", "liftA2"]) $ do
   jdg <- goal
-  case splitAppTy_maybe $ unCType $ jGoal jdg of
+  let hole = unCType $ jGoal jdg
+  when (isFunction hole) $
+    throwError $ GoalMismatch "idiom" $ jGoal jdg
+  case splitAppTy_maybe hole of
     Just (applic, ty) -> do
-      -- unlessM (hasInstance applicativeClassName [applic]) $
-      --   throwError $ GoalMismatch "idiom" $ CType applic
+      unlessM (hasInstance applicativeClassName [applic]) $
+        throwError $ GoalMismatch "idiom" $ CType applic
       rule $ \jdg -> do
         (tr, expr) <- subgoalWith (withNewGoal (CType ty) jdg) m
         case unLoc expr of
@@ -313,14 +316,18 @@ auto' n = do
   try intros
   choice
     [ overFunctions $ \fname -> do
-        idiom (apply fname) <|> apply fname
-        loop
+        choice
+          [ idiom (apply fname) >> assumption
+          , apply fname >> loop
+          ]
     , overAlgebraicTerms $ \aname -> do
         destructAuto aname
         loop
     , do
-        idiom splitAuto <|> splitAuto
-        loop
+        choice
+          [ idiom splitAuto >> assumption
+          , splitAuto >> loop
+          ]
     , assumption >> loop
     , recursion
     ]
diff --git a/test/testdata/tactic/GoldenApplicativeThen.hs.expected b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
index fc7816581b..de6616d50c 100644
--- a/test/testdata/tactic/GoldenApplicativeThen.hs.expected
+++ b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
@@ -1,2 +1,2 @@
 useThen :: Applicative f => f Int -> f a -> f a
-useThen = (\ x x8 -> (*>) x x8)
+useThen = (\ x x6 -> (*>) x x6)

From caf05be4f9ae73123f4a064883c6d88ff6236263 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Oct 2020 09:46:01 -0700
Subject: [PATCH 19/20] Fix broken test

---
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  6 ++++-
 plugins/tactics/test/AutoTupleSpec.hs         | 25 +++++++++++--------
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 1086b93a06..cfbd430bf9 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -261,7 +261,11 @@ instance MonadTc TacticsM where
 ------------------------------------------------------------------------------
 -- | An empty context
 emptyContext :: Context
-emptyContext  = Context mempty mempty (error "can't runTcM")
+emptyContext
+  = Context mempty mempty
+  $ trace "using empty context; TcM operations will always fail"
+  $ const
+  $ pure Nothing
 
 
 newtype Rose a = Rose (Tree a)
diff --git a/plugins/tactics/test/AutoTupleSpec.hs b/plugins/tactics/test/AutoTupleSpec.hs
index 8c7bc17c34..ff546ed864 100644
--- a/plugins/tactics/test/AutoTupleSpec.hs
+++ b/plugins/tactics/test/AutoTupleSpec.hs
@@ -2,6 +2,7 @@
 
 module AutoTupleSpec where
 
+import           Control.Monad.IO.Class (MonadIO(liftIO))
 import           Data.Either (isRight)
 import qualified Data.Map as M
 import           Ide.Plugin.Tactic.Debug
@@ -37,17 +38,19 @@ spec = describe "auto for tuple" $ do
       out_type <- mkBoxedTupleTy
                 . fmap mkBoxedTupleTy
               <$> randomGroups vars
-      pure $
-          -- We should always be able to find a solution
-          runTactic
-            emptyContext
-            (mkFirstJudgement
-              (M.singleton (mkVarOcc "x") $ CType in_type)
-              mempty
-              True
-              mempty
-              out_type)
-            (auto' $ n * 2) `shouldSatisfy` isRight
+      pure $ do
+        -- We should always be able to find a solution
+        res <- liftIO
+            $ runTactic
+                emptyContext
+                (mkFirstJudgement
+                  (M.singleton (mkVarOcc "x") $ CType in_type)
+                  mempty
+                  True
+                  mempty
+                  out_type)
+                (auto' $ n * 2)
+        res `shouldSatisfy` isRight
 
 
 randomGroups :: [a] -> Gen [[a]]

From ff3be761f4a6b6741ac8ecff4fe4e88967946b00 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 27 Oct 2020 09:56:25 -0700
Subject: [PATCH 20/20] Conditionally import CtWanted

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs  | 20 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  4 +---
 2 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 462e17e75b..9ba69623c5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -5,27 +5,31 @@
 
 module Ide.Plugin.Tactic.GHC where
 
-import Control.Arrow
+import           Control.Arrow
 import           Control.Monad.State
 import qualified Data.Map as M
 import           Data.Maybe (isJust)
 import           Data.Traversable
 import           Development.IDE.GHC.Compat
 import           Generics.SYB (mkT, everywhere)
+import           Id (mkVanillaGlobal)
 import           Ide.Plugin.Tactic.Types
 import           OccName
+import           TcEnv (tcLookupTyCon)
+import           TcEvidence (TcEvBinds (..), evBindMapBinds)
+import           TcRnMonad
+import           TcSMonad (runTcS)
+import           TcSimplify (solveWanteds)
 import           TcType
 import           TyCoRep
 import           Type
-import           TysWiredIn (unitTy, intTyCon, floatTyCon, doubleTyCon, charTyCon)
+import           TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import           Unique
 import           Var
-import TcRnMonad
-import TcEvidence (TcEvBinds (..), evBindMapBinds, TcEvBinds(TcEvBinds))
-import TcEnv (tcLookupTyCon)
-import Id (mkVanillaGlobal)
-import TcSMonad (runTcS)
-import TcSimplify (solveWanteds)
+
+#if __GLASGOW_HASKELL__ >= 810
+import Constraint
+#endif
 
 
 tcTyVar_maybe :: Type -> Maybe Var
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index cfbd430bf9..b768ae273c 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -34,16 +34,14 @@ import Data.Tree
 import Development.IDE.GHC.Compat hiding (Node)
 import Development.IDE.Types.Location
 import GHC.Generics
-import HscTypes (emptyTypeEnv, TypeEnv)
 import Ide.Plugin.Tactic.Debug
-import InstEnv (emptyInstEnv, InstEnv)
 import OccName
 import Refinery.Tactic
 import System.IO.Unsafe (unsafePerformIO)
+import TcRnMonad (TcM)
 import Type
 import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
 import Unique (Unique)
-import TcRnMonad (TcM)
 
 
 ------------------------------------------------------------------------------