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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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 36de8112c009f93d6fee888b32f787ea97150f09 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 25 Oct 2020 12:07:49 -0700
Subject: [PATCH 13/13] Only allow assumption in unconstrained polymorphic
 holes

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 13 +++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 29 ++++++++++---------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  3 ++
 test/functional/Tactic.hs                     |  1 +
 test/testdata/tactic/GoldenApplicativeThen.hs |  2 ++
 .../tactic/GoldenApplicativeThen.hs.expected  |  2 ++
 6 files changed, 36 insertions(+), 14 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenApplicativeThen.hs
 create mode 100644 test/testdata/tactic/GoldenApplicativeThen.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 75fa4c49b3..94850fa4e0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -208,3 +208,16 @@ methodHypothesis ty = do
     let (_, _, ty) = tcSplitSigmaTy $ idType method
     in (occName method,  CType $ substTy subst ty)
 
+
+------------------------------------------------------------------------------
+-- | Run the given tactic iff the current hole contains no univars. Skolems and
+-- already decided univars are OK though.
+requireConcreteHole :: TacticsM a -> TacticsM a
+requireConcreteHole m = do
+  jdg     <- goal
+  skolems <- gets $ S.fromList . ts_skolems
+  let vars = S.fromList $ tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
+  case S.size $ vars S.\\ skolems of
+    0 -> m
+    _ -> throwError TooPolymorphic
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 9bb5be4282..4a6389ec9f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -65,7 +65,7 @@ assume name = rule $ \jdg -> do
 
 
 recursion :: TacticsM ()
-recursion = tracing "recursion" $ do
+recursion = requireConcreteHole $ tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
@@ -106,7 +106,7 @@ intros = rule $ \jdg -> do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destructAuto :: OccName -> TacticsM ()
-destructAuto name = tracing "destruct(auto)" $ do
+destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -126,7 +126,7 @@ destructAuto name = tracing "destruct(auto)" $ do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: OccName -> TacticsM ()
-destruct name = tracing "destruct(user)" $ do
+destruct name = requireConcreteHole $ tracing "destruct(user)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -136,7 +136,7 @@ destruct name = tracing "destruct(user)" $ do
 ------------------------------------------------------------------------------
 -- | Case split, using the same data constructor in the matches.
 homo :: OccName -> TacticsM ()
-homo = tracing "homo" . rule . destruct' (\dc jdg ->
+homo = requireConcreteHole . tracing "homo" . rule . destruct' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
@@ -160,7 +160,7 @@ homoLambdaCase =
 
 
 apply :: OccName -> TacticsM ()
-apply func = tracing ("apply' " <> show func) $ do
+apply func = requireConcreteHole $ tracing ("apply' " <> show func) $ do
   jdg <- goal
   let hy = jHypothesis jdg
       g  = jGoal jdg
@@ -205,7 +205,7 @@ split = tracing "split(user)" $ do
 -- 'split' because it won't split a data con if it doesn't result in any new
 -- goals.
 splitAuto :: TacticsM ()
-splitAuto = tracing "split(auto)" $ do
+splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
@@ -234,14 +234,15 @@ requireNewHoles m = do
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
 splitDataCon :: DataCon -> TacticsM ()
-splitDataCon dc = tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
-  let g = jGoal jdg
-  case splitTyConApp_maybe $ unCType g of
-    Just (tc, apps) -> do
-      case elem dc $ tyConDataCons tc of
-        True -> buildDataCon (unwhitelistingSplit jdg) dc apps
-        False -> throwError $ IncorrectDataCon dc
-    Nothing -> throwError $ GoalMismatch "splitDataCon" g
+splitDataCon dc =
+  requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
+    let g = jGoal jdg
+    case splitTyConApp_maybe $ unCType g of
+      Just (tc, apps) -> do
+        case elem dc $ tyConDataCons tc of
+          True -> buildDataCon (unwhitelistingSplit jdg) dc apps
+          False -> throwError $ IncorrectDataCon dc
+      Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index bf3aa020ae..2d7299a380 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -177,6 +177,7 @@ data TacticError
   | RecursionOnWrongParam OccName Int OccName
   | UnhelpfulDestruct OccName
   | UnhelpfulSplit OccName
+  | TooPolymorphic
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -213,6 +214,8 @@ instance Show TacticError where
       "Destructing patval " <> show n <> " leads to no new types"
     show (UnhelpfulSplit n) =
       "Splitting constructor " <> show n <> " leads to no new goals"
+    show TooPolymorphic =
+      "The tactic isn't applicable because the goal is too polymorphic"
 
 
 ------------------------------------------------------------------------------
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index c386570c10..c265719eb3 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -106,6 +106,7 @@ tests = testGroup
   , goldenTest "GoldenShowCompose.hs"       2 15 Auto ""
   , goldenTest "GoldenShowMapChar.hs"       2 8  Auto ""
   , goldenTest "GoldenSuperclass.hs"        7 8  Auto ""
+  , goldenTest "GoldenApplicativeThen.hs"   2 11 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenApplicativeThen.hs b/test/testdata/tactic/GoldenApplicativeThen.hs
new file mode 100644
index 0000000000..29ce9f5132
--- /dev/null
+++ b/test/testdata/tactic/GoldenApplicativeThen.hs
@@ -0,0 +1,2 @@
+useThen :: Applicative f => f Int -> f a -> f a
+useThen = _
diff --git a/test/testdata/tactic/GoldenApplicativeThen.hs.expected b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
new file mode 100644
index 0000000000..fc7816581b
--- /dev/null
+++ b/test/testdata/tactic/GoldenApplicativeThen.hs.expected
@@ -0,0 +1,2 @@
+useThen :: Applicative f => f Int -> f a -> f a
+useThen = (\ x x8 -> (*>) x x8)