From 3527cd21b35cbb8c00ea7680f597225cfe2e6154 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sat, 3 Oct 2020 11:20:44 -0700
Subject: [PATCH 01/50] WIP recursion

This changes the heuristics so we get a reasonable fmap @[], but breaks
note.
---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 35 +++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Context.hs  |  4 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  5 ++
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 48 ++++++++++++++-----
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 32 +++++++++----
 6 files changed, 86 insertions(+), 40 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 1f1f3ea449..09c64c325d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -1,22 +1,24 @@
 {-# LANGUAGE FlexibleContexts #-}
 module Ide.Plugin.Tactic.CodeGen where
 
-import Control.Monad.Except
-import Data.List
-import Data.Traversable
-import DataCon
-import Development.IDE.GHC.Compat
-import GHC.Exts
-import GHC.SourceGen.Binds
-import GHC.SourceGen.Expr
-import GHC.SourceGen.Overloaded
-import GHC.SourceGen.Pat
-import Ide.Plugin.Tactic.Judgements
-import Ide.Plugin.Tactic.Machinery
-import Ide.Plugin.Tactic.Naming
-import Ide.Plugin.Tactic.Types
-import Name
-import Type hiding (Var)
+import           Control.Monad.Except
+import           Control.Monad.State.Class (modify)
+import           Data.List
+import qualified Data.Set as S
+import           Data.Traversable
+import           DataCon
+import           Development.IDE.GHC.Compat
+import           GHC.Exts
+import           GHC.SourceGen.Binds
+import           GHC.SourceGen.Expr
+import           GHC.SourceGen.Overloaded
+import           GHC.SourceGen.Pat
+import           Ide.Plugin.Tactic.Judgements
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Naming
+import           Ide.Plugin.Tactic.Types
+import           Name
+import           Type hiding (Var)
 
 
 destructMatches
@@ -48,6 +50,7 @@ destructMatches f f2 t jdg = do
                 $ introducingPat (zip names $ coerce args)
                 $ withNewGoal g jdg
           sg <- f dc j
+          modify $ withIntroducedVals $ mappend $ S.fromList names
           pure $ match [pat] $ unLoc sg
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
index f1cccae928..2c8b48227a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs
@@ -34,8 +34,8 @@ getFunBindId (AbsBinds _ _ _ abes _ _ _)
 getFunBindId _ = []
 
 
-getCurrentDefinitions :: MonadReader Context m => m [OccName]
-getCurrentDefinitions = asks $ fmap fst . ctxDefiningFuncs
+getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
+getCurrentDefinitions = asks $ ctxDefiningFuncs
 
 getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
 getModuleHypothesis = asks ctxModuleFuncs
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 51c1cef988..19b040877d 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -52,6 +52,11 @@ introducing ns jdg@Judgement{..} = jdg
   { _jHypothesis = M.fromList ns <> _jHypothesis
   }
 
+withHypothesis :: (Map OccName a -> Map OccName a) -> Judgement' a -> Judgement' a
+withHypothesis f jdg@Judgement{..} = jdg
+  { _jHypothesis = f _jHypothesis
+  }
+
 ------------------------------------------------------------------------------
 -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals.
 introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 65885324c0..2ddc06944f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -79,7 +79,7 @@ runTactic ctx jdg t =
 scoreSolution :: TacticState -> [Judgement] -> Int
 scoreSolution TacticState{..} holes
   -- TODO(sandy): should this be linear?
-  = S.size ts_used_vals - length holes * 5
+  = negate (traceShowId $ S.size (ts_intro_vals S.\\ ts_used_vals)) - length holes * 5
 
 
 runTacticTWithState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 89cb181275..b4f2498ca8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -39,14 +39,8 @@ import           Type hiding (Var)
 
 ------------------------------------------------------------------------------
 -- | Use something in the hypothesis to fill the hole.
--- TODO(sandy): deprecate this
 assumption :: TacticsM ()
-assumption = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case find ((== g) . snd) $ toList hy of
-    Just (v, _) -> pure $ noLoc $ var' v
-    Nothing -> throwError $ GoalMismatch "assumption" g
+assumption = attemptOn allNames assume
 
 
 ------------------------------------------------------------------------------
@@ -71,6 +65,27 @@ useOccName jdg name =
     Nothing -> pure ()
 
 
+------------------------------------------------------------------------------
+-- | Restrict a tactic to looking only at pattern vals and functions
+simpler :: TacticsM () -> TacticsM ()
+simpler t = do
+  jdg <- goal
+  let funcs = M.filter (isFunction . unCType) $ jHypothesis jdg
+      hy' = jPatHypothesis jdg <> funcs
+  traceM $ mappend "!!! yo: " $ show hy'
+  localTactic t $ withHypothesis $ const hy'
+
+
+recursion :: TacticsM ()
+recursion = do
+  defs <- getCurrentDefinitions
+  traceM $ mappend "!!! recursion: " $ show defs
+  attemptOn (const $ fmap fst defs) $ \name -> do
+    traceM $ mappend "!!! recursing: " $ show name
+    localTactic (apply' name) (introducing defs)
+    simpler assumption
+
+
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
 intro :: TacticsM ()
@@ -81,6 +96,7 @@ intro = rule $ \jdg -> do
     Just (a, b) -> do
       v <- pure $ mkGoodName (getInScope hy) a
       let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg
+      modify $ withIntroducedVals $ mappend $ S.singleton v
       sg <- newSubgoal jdg'
       pure $ noLoc $ lambda [bvar' v] $ unLoc sg
     _ -> throwError $ GoalMismatch "intro" g
@@ -97,6 +113,7 @@ intros = rule $ \jdg -> do
     (as, b) -> do
       vs <- mkManyGoodNames hy as
       let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg
+      modify $ withIntroducedVals $ mappend $ S.fromList vs
       sg <- newSubgoal jdg'
       pure
         . noLoc
@@ -142,6 +159,7 @@ apply' func = rule $ \jdg -> do
     Just (CType ty) -> do
         let (args, ret) = splitFunTys ty
         unify g (CType ret)
+        useOccName jdg func
         sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
         pure . noLoc
              . foldl' (@@) (var' func)
@@ -186,13 +204,20 @@ attemptOn :: (Judgement -> [a]) -> (a -> TacticsM ()) -> TacticsM ()
 attemptOn getNames tac = matching (choice . fmap (\s -> tac s) . getNames)
 
 
+localTactic :: TacticsM a -> (Judgement -> Judgement) -> TacticsM a
+localTactic t f = do
+  TacticT $ StateT $ \jdg ->
+    runStateT (unTacticT t) $ f jdg
+
+
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
 auto = do
   current <- getCurrentDefinitions
-  TacticT $ StateT $ \jdg ->
-    runStateT (unTacticT $ auto' 5) $ disallowing current jdg
+  traceM $ mappend "!!!auto defs:" $ show current
+  localTactic (auto' 4) $ disallowing $ fmap fst current
+
 
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
@@ -207,9 +232,8 @@ auto' n = do
         progress ((==) `on` jGoal) NoProgress (destruct aname)
         loop
     , split >> loop
-    , attemptOn allNames $ \name -> do
-        assume name
-        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 291d732fad..1cb3e35db7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,10 +1,11 @@
-{-# LANGUAGE DeriveFunctor                  #-}
-{-# LANGUAGE DeriveGeneric                  #-}
-{-# LANGUAGE DerivingStrategies             #-}
-{-# LANGUAGE FlexibleInstances              #-}
-{-# LANGUAGE GeneralizedNewtypeDeriving     #-}
-{-# LANGUAGE MultiParamTypeClasses          #-}
-{-# LANGUAGE TypeSynonymInstances           #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE TypeSynonymInstances       #-}
+{-# OPTIONS_GHC -fno-warn-orphans       #-}
 
 module Ide.Plugin.Tactic.Types
   ( module Ide.Plugin.Tactic.Types
@@ -40,23 +41,31 @@ instance Eq CType where
 instance Ord CType where
   compare = nonDetCmpType `on` unCType
 
+instance Show CType where
+  show  = unsafeRender . unCType
+
+instance Show OccName where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
     { ts_skolems   :: !([TyVar])
     , ts_unifier   :: !(TCvSubst)
     , ts_used_vals :: !(Set OccName)
+    , ts_intro_vals :: !(Set OccName)
     }
 
 instance Semigroup TacticState where
-  TacticState a1 b1 c1 <> TacticState a2 b2 c2
+  TacticState a1 b1 c1 d1 <> TacticState a2 b2 c2 d2
     = TacticState
         (a1 <> a2)
         (unionTCvSubst b1 b2)
         (c1 <> c2)
+        (d1 <> d2)
 
 instance Monoid TacticState where
-  mempty = TacticState mempty emptyTCvSubst mempty
+  mempty = TacticState mempty emptyTCvSubst mempty mempty
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
@@ -64,6 +73,11 @@ withUsedVals f ts = ts
   { ts_used_vals = f $ ts_used_vals ts
   }
 
+withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
+withIntroducedVals f ts = ts
+  { ts_intro_vals = f $ ts_intro_vals ts
+  }
+
 
 ------------------------------------------------------------------------------
 -- | The current bindings and goal for a hole to be filled by refinery.

From da2d7296d5dde6717869fd2ec92616fb026796c9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:12:41 -0700
Subject: [PATCH 02/50] Better scoring heuristic

I was forgetting to count destruct as usage
---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 12 ++++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 25 ++++++++++++++++---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  6 -----
 test/functional/Tactic.hs                     |  1 +
 test/testdata/tactic/GoldenListFmap.hs        |  2 ++
 .../tactic/GoldenListFmap.hs.expected         |  5 ++++
 6 files changed, 41 insertions(+), 10 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenListFmap.hs
 create mode 100644 test/testdata/tactic/GoldenListFmap.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 09c64c325d..c868028a1b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -2,8 +2,10 @@
 module Ide.Plugin.Tactic.CodeGen where
 
 import           Control.Monad.Except
+import           Control.Monad.State (MonadState)
 import           Control.Monad.State.Class (modify)
 import           Data.List
+import qualified Data.Map as M
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
@@ -21,6 +23,13 @@ import           Name
 import           Type hiding (Var)
 
 
+useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
+useOccName jdg name =
+  case M.lookup name $ jHypothesis jdg of
+    Just{}  -> modify $ withUsedVals $ S.insert name
+    Nothing -> pure ()
+
+
 destructMatches
     :: (DataCon -> Judgement -> Rule)
        -- ^ How to construct each match
@@ -62,7 +71,8 @@ destruct' f term jdg = do
   let hy = jHypothesis jdg
   case find ((== term) . fst) $ toList hy of
     Nothing -> throwError $ UndefinedHypothesis term
-    Just (_, t) ->
+    Just (_, t) -> do
+      useOccName jdg term
       fmap noLoc $ case' (var' term) <$>
         destructMatches f (destructing term) t jdg
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 2ddc06944f..4d560f78b7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveFunctor         #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE DerivingStrategies    #-}
+{-# LANGUAGE DerivingVia           #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE LambdaCase            #-}
@@ -76,10 +77,28 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
-scoreSolution :: TacticState -> [Judgement] -> Int
+scoreSolution
+    :: TacticState
+    -> [Judgement]
+    -> ( Penalize Int  -- number of holes
+       , Reward Bool  -- all bindings used
+       , Reward Int   -- number used bindings
+       , Penalize Int   -- number used bindings
+       )
 scoreSolution TacticState{..} holes
-  -- TODO(sandy): should this be linear?
-  = negate (traceShowId $ S.size (ts_intro_vals S.\\ ts_used_vals)) - length holes * 5
+  = traceShowId
+    ( Penalize $ length holes
+    , Reward $ S.null $ traceShowId $ ts_intro_vals S.\\ ts_used_vals
+    , Reward $ S.size ts_used_vals
+    , Penalize $ S.size ts_intro_vals
+    )
+
+
+newtype Penalize a = Penalize a
+  deriving (Eq, Ord, Show) via (Down a)
+
+newtype Reward a = Reward a
+  deriving (Eq, Ord, Show) via a
 
 
 runTacticTWithState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index b4f2498ca8..f5856fc8dc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -58,12 +58,6 @@ assume name = rule $ \jdg -> do
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-useOccName :: MonadState TacticState m => Judgement -> OccName -> m ()
-useOccName jdg name =
-  case M.lookup name $ jHypothesis jdg of
-    Just{}  -> modify $ withUsedVals $ S.insert name
-    Nothing -> pure ()
-
 
 ------------------------------------------------------------------------------
 -- | Restrict a tactic to looking only at pattern vals and functions
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index e770ad8a41..ae4379a9fb 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -93,6 +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 ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenListFmap.hs b/test/testdata/tactic/GoldenListFmap.hs
new file mode 100644
index 0000000000..85293daaf4
--- /dev/null
+++ b/test/testdata/tactic/GoldenListFmap.hs
@@ -0,0 +1,2 @@
+fmapList :: (a -> b) -> [a] -> [b]
+fmapList = _
diff --git a/test/testdata/tactic/GoldenListFmap.hs.expected b/test/testdata/tactic/GoldenListFmap.hs.expected
new file mode 100644
index 0000000000..26766d57c3
--- /dev/null
+++ b/test/testdata/tactic/GoldenListFmap.hs.expected
@@ -0,0 +1,5 @@
+fmapList :: (a -> b) -> [a] -> [b]
+fmapList = (\ fab l_a
+   -> case l_a of
+        [] -> []
+        ((:) a l_a3) -> (:) (fab a) (fmapList fab l_a3))

From b805aa9bc364e0ccf5a3d0030c49d529db17a0ff Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:14:48 -0700
Subject: [PATCH 03/50] Don't trace scoring

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

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 4d560f78b7..afc4ab3058 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -86,9 +86,8 @@ scoreSolution
        , Penalize Int   -- number used bindings
        )
 scoreSolution TacticState{..} holes
-  = traceShowId
-    ( Penalize $ length holes
-    , Reward $ S.null $ traceShowId $ ts_intro_vals S.\\ ts_used_vals
+  = ( Penalize $ length holes
+    , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
     , Reward $ S.size ts_used_vals
     , Penalize $ S.size ts_intro_vals
     )

From 1dbec5b849b67d3dcf6eae3938d78dcd6881f765 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 12:33:10 -0700
Subject: [PATCH 04/50] Add fromMaybe test

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 6 +++---
 test/functional/Tactic.hs                          | 1 +
 test/testdata/tactic/GoldenFromMaybe.hs            | 2 ++
 test/testdata/tactic/GoldenFromMaybe.hs.expected   | 5 +++++
 4 files changed, 11 insertions(+), 3 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFromMaybe.hs
 create mode 100644 test/testdata/tactic/GoldenFromMaybe.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index afc4ab3058..6f1b9d2034 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -81,9 +81,9 @@ scoreSolution
     :: TacticState
     -> [Judgement]
     -> ( Penalize Int  -- number of holes
-       , Reward Bool  -- all bindings used
-       , Reward Int   -- number used bindings
-       , Penalize Int   -- number used bindings
+       , Reward Bool   -- all bindings used
+       , Reward Int    -- number used bindings
+       , Penalize Int  -- number of introduced bindings
        )
 scoreSolution TacticState{..} holes
   = ( Penalize $ length holes
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index ae4379a9fb..b70efb3376 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -94,6 +94,7 @@ tests = testGroup
   , goldenTest "GoldenNote.hs"              2 8  Auto ""
   , goldenTest "GoldenPureList.hs"          2 12 Auto ""
   , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
+  , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs b/test/testdata/tactic/GoldenFromMaybe.hs
new file mode 100644
index 0000000000..e3046a29c3
--- /dev/null
+++ b/test/testdata/tactic/GoldenFromMaybe.hs
@@ -0,0 +1,2 @@
+fromMaybe :: a -> Maybe a -> a
+fromMaybe = _
diff --git a/test/testdata/tactic/GoldenFromMaybe.hs.expected b/test/testdata/tactic/GoldenFromMaybe.hs.expected
new file mode 100644
index 0000000000..1375967a70
--- /dev/null
+++ b/test/testdata/tactic/GoldenFromMaybe.hs.expected
@@ -0,0 +1,5 @@
+fromMaybe :: a -> Maybe a -> a
+fromMaybe = (\ a ma
+   -> case ma of
+        Nothing -> a
+        (Just a2) -> a2)

From 803c8d70cf8daba17ab05c3e0107a06c18af159c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 4 Oct 2020 14:07:58 -0700
Subject: [PATCH 05/50] wtf; recursion stack frame doesnt seem to work

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  8 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 10 ++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 44 +++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 74 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 21 +++---
 5 files changed, 108 insertions(+), 49 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index c868028a1b..0b5c8c370b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -68,6 +68,7 @@ destructMatches f f2 t jdg = do
 -- resulting matches.
 destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
 destruct' f term jdg = do
+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let hy = jHypothesis jdg
   case find ((== term) . fst) $ toList hy of
     Nothing -> throwError $ UndefinedHypothesis term
@@ -82,6 +83,7 @@ destruct' f term jdg = do
 -- resulting matches.
 destructLambdaCase' :: (DataCon -> Judgement -> Rule) -> Judgement -> Rule
 destructLambdaCase' f jdg = do
+  when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
@@ -99,7 +101,11 @@ buildDataCon
     -> RuleM (LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
-  sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
+  sgs <- traverse ( newSubgoal
+                  . blacklistingDestruct
+                  . flip withNewGoal jdg
+                  . CType
+                  ) args
   pure
     . noLoc
     . foldl' (@@)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 19b040877d..50b4829f67 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -42,6 +42,14 @@ destructing n jdg@Judgement{..} = jdg
   { _jDestructed = _jDestructed <> S.singleton n
   }
 
+blacklistingDestruct :: Judgement -> Judgement
+blacklistingDestruct jdg = jdg
+  { _jBlacklistDestruct = True
+  }
+
+isDestructBlacklisted :: Judgement -> Bool
+isDestructBlacklisted = _jBlacklistDestruct
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t jdg = jdg
   { _jGoal = t
@@ -90,5 +98,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 6f1b9d2034..9d156e197f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,9 +18,9 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
-import           Control.Monad.Except (throwError)
+import           Control.Monad.Error.Class
 import           Control.Monad.Reader
-import           Control.Monad.State (gets, modify)
+import           Control.Monad.State.Class (gets, modify, MonadState)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
@@ -62,21 +62,55 @@ runTactic
     -> Either [TacticError] (LHsExpr GhcPs)
 runTactic ctx jdg t =
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
-        tacticState = mempty { ts_skolems = skolems }
+        tacticState = defaultTacticState { ts_skolems = skolems }
     in case partitionEithers
           . flip runReader ctx
           . unExtractM
           $ runTacticTWithState t jdg tacticState of
       (errs, []) -> Left $ errs
       (_, solns) -> do
+        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ intercalate "\n" $ fmap (unsafeRender . fst) $ solns
-        case sortBy (comparing $ Down . uncurry scoreSolution . snd) solns of
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (unsafeRender . fst) sorted
+        case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
           _ -> Left []
 
 
+recursionStackFrame
+    :: (MonadError TacticError m, MonadState TacticState m)
+    => m a
+    -> m (Bool, a)
+recursionStackFrame ma = do
+  modify $ withRecursionStack (False :)
+  finally
+    ( do
+      a <- ma
+      r <- gets $ head . ts_recursion_stack
+      pure (r, a)
+    )
+    (modify $ withRecursionStack tail)
+
+
+finally :: MonadError e m => m a -> m () -> m a
+finally action cleanup = do
+  a <-
+    action `catchError` \e -> do
+      cleanup
+      throwError e
+  cleanup
+  pure a
+
+
+setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
+setRecursionFrameData b = do
+  modify $ withRecursionStack $ \case
+    (_ : bs) -> b : bs
+    []       -> []
+
+
+
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index f5856fc8dc..e6cebe3360 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -34,6 +34,7 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Control.Monad
 
 
 
@@ -52,33 +53,34 @@ assume name = rule $ \jdg -> do
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
+          when (M.member name $ jPatHypothesis jdg) $ do
+            -- traceM $ "!!!simpler: " <> show name
+            setRecursionFrameData True
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
-
-------------------------------------------------------------------------------
--- | Restrict a tactic to looking only at pattern vals and functions
-simpler :: TacticsM () -> TacticsM ()
-simpler t = do
-  jdg <- goal
-  let funcs = M.filter (isFunction . unCType) $ jHypothesis jdg
-      hy' = jPatHypothesis jdg <> funcs
-  traceM $ mappend "!!! yo: " $ show hy'
-  localTactic t $ withHypothesis $ const hy'
-
-
 recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
-  traceM $ mappend "!!! recursion: " $ show defs
   attemptOn (const $ fmap fst defs) $ \name -> do
-    traceM $ mappend "!!! recursing: " $ show name
-    localTactic (apply' name) (introducing defs)
-    simpler assumption
-
+    localTactic (apply' name) $ introducing defs
+    (has_simple, _) <- recursionStackFrame assumption
+    case has_simple of
+      True -> traceM $ mappend "!!!recursion ok: " $ show defs
+      False -> do
+        traceM $ mappend "!!!recursion not ok >: " $ show defs
+        throwError NoProgress
+
+
+foo :: Int -> a -> a -> [[a]]
+foo n i b = map (take n) . take n $ go (i : repeat b)
+  where
+    go [] = [[]]
+    go [x] = [[x]]
+    go l@(x:y:ys) = l : map (y :) (go $ x:ys)
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
@@ -146,19 +148,25 @@ homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
 
 
 apply' :: OccName -> TacticsM ()
-apply' func = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case M.lookup func hy of
-    Just (CType ty) -> do
-        let (args, ret) = splitFunTys ty
-        unify g (CType ret)
-        useOccName jdg func
-        sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
-        pure . noLoc
-             . foldl' (@@) (var' func)
-             $ fmap unLoc sgs
-    Nothing -> throwError $ GoalMismatch "apply" g
+apply' func = do
+  rule $ \jdg -> do
+    let hy = jHypothesis jdg
+        g  = jGoal jdg
+    case M.lookup func hy of
+      Just (CType ty) -> do
+          let (args, ret) = splitFunTys ty
+          unify g (CType ret)
+          useOccName jdg func
+          sgs <- traverse ( newSubgoal
+                          . blacklistingDestruct
+                          . flip withNewGoal jdg
+                          . CType
+                          ) args
+          pure . noLoc
+              . foldl' (@@) (var' func)
+              $ fmap unLoc sgs
+      Nothing -> throwError $ GoalMismatch "apply" g
+  assumption
 
 
 ------------------------------------------------------------------------------
@@ -209,8 +217,10 @@ localTactic t f = do
 auto :: TacticsM ()
 auto = do
   current <- getCurrentDefinitions
-  traceM $ mappend "!!!auto defs:" $ show current
-  localTactic (auto' 4) $ disallowing $ fmap fst current
+  jdg <- goal
+  traceM $ mappend "!!!auto current:" $ show current
+  traceM $ mappend "!!!auto jdg:" $ show jdg
+  localTactic (auto' 5) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 1cb3e35db7..52a83780e3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -54,18 +54,18 @@ data TacticState = TacticState
     , ts_unifier   :: !(TCvSubst)
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
+    , ts_recursion_stack :: ![Bool]
     }
 
-instance Semigroup TacticState where
-  TacticState a1 b1 c1 d1 <> TacticState a2 b2 c2 d2
-    = TacticState
-        (a1 <> a2)
-        (unionTCvSubst b1 b2)
-        (c1 <> c2)
-        (d1 <> d2)
+defaultTacticState :: TacticState
+defaultTacticState =
+  TacticState mempty emptyTCvSubst mempty mempty mempty
 
-instance Monoid TacticState where
-  mempty = TacticState mempty emptyTCvSubst mempty mempty
+withRecursionStack
+  :: ([Bool] -> [Bool]) -> TacticState -> TacticState
+withRecursionStack f ts = ts
+  { ts_recursion_stack = f $ ts_recursion_stack ts
+  }
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
@@ -87,9 +87,10 @@ data Judgement' a = Judgement
     -- ^ These should align with keys of _jHypothesis
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
+  , _jBlacklistDestruct :: !(Bool)
   , _jGoal        :: !(a)
   }
-  deriving stock (Eq, Ord, Generic, Functor)
+  deriving stock (Eq, Ord, Generic, Functor, Show)
 
 type Judgement = Judgement' CType
 

From fe468f3cd401cefb59dfd5928ecd6f8f9b052fc0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:00:49 -0700
Subject: [PATCH 06/50] Better debugging and smarter apply'

---
 plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs   |  5 ++++-
 .../tactics/src/Ide/Plugin/Tactic/Machinery.hs   |  3 ++-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 16 +++++-----------
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs   | 11 ++++++++++-
 4 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index 6d1053c2c6..c81ea6e59a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -4,11 +4,12 @@ module Ide.Plugin.Tactic.Debug
   , traceM
   , traceShowId
   , trace
+  , traceMX
   ) where
 
 import Debug.Trace
 import DynFlags (unsafeGlobalDynFlags)
-import Outputable
+import Outputable hiding ((<>))
 
 ------------------------------------------------------------------------------
 -- | Print something
@@ -18,3 +19,5 @@ unsafeRender = unsafeRender' . ppr
 unsafeRender' :: SDoc -> String
 unsafeRender' = showSDoc unsafeGlobalDynFlags
 
+traceMX :: (Monad m, Show a) => String -> a -> m ()
+traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 9d156e197f..a2f5e74ec1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -35,6 +35,7 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import Control.Monad.State (MonadState(..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -71,7 +72,7 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (unsafeRender . fst) sorted
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e6cebe3360..bf788fea3f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE LambdaCase            #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeSynonymInstances  #-}
 {-# LANGUAGE ViewPatterns          #-}
@@ -11,6 +12,7 @@ module Ide.Plugin.Tactic.Tactics
   ) where
 
 import           Control.Applicative
+import           Control.Monad
 import           Control.Monad.Except (throwError)
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
@@ -34,7 +36,6 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Control.Monad
 
 
 
@@ -54,7 +55,7 @@ assume name = rule $ \jdg -> do
       case ty == jGoal jdg of
         True  -> do
           when (M.member name $ jPatHypothesis jdg) $ do
-            -- traceM $ "!!!simpler: " <> show name
+            traceM $ "!!!simpler: " <> show name
             setRecursionFrameData True
           useOccName jdg name
           pure $ noLoc $ var' name
@@ -75,13 +76,6 @@ recursion = do
         throwError NoProgress
 
 
-foo :: Int -> a -> a -> [[a]]
-foo n i b = map (take n) . take n $ go (i : repeat b)
-  where
-    go [] = [[]]
-    go [x] = [[x]]
-    go l@(x:y:ys) = l : map (y :) (go $ x:ys)
-
 ------------------------------------------------------------------------------
 -- | Introduce a lambda.
 intro :: TacticsM ()
@@ -165,8 +159,8 @@ apply' func = do
           pure . noLoc
               . foldl' (@@) (var' func)
               $ fmap unLoc sgs
-      Nothing -> throwError $ GoalMismatch "apply" g
-  assumption
+      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 52a83780e3..b4195c6573 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -47,6 +47,15 @@ instance Show CType where
 instance Show OccName where
   show  = unsafeRender
 
+instance Show Var where
+  show  = unsafeRender
+
+instance Show TCvSubst where
+  show  = unsafeRender
+
+instance Show (LHsExpr GhcPs) where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
@@ -55,7 +64,7 @@ data TacticState = TacticState
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
     , ts_recursion_stack :: ![Bool]
-    }
+    } deriving stock Show
 
 defaultTacticState :: TacticState
 defaultTacticState =

From 68cda515d606690e979faba0e53e924281fecb85 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:15:16 -0700
Subject: [PATCH 07/50] filterT

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 41 +++++++++++++------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  8 +---
 2 files changed, 30 insertions(+), 19 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index a2f5e74ec1..1115a90a27 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -79,19 +79,34 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
-recursionStackFrame
-    :: (MonadError TacticError m, MonadState TacticState m)
-    => m a
-    -> m (Bool, a)
-recursionStackFrame ma = do
-  modify $ withRecursionStack (False :)
-  finally
-    ( do
-      a <- ma
-      r <- gets $ head . ts_recursion_stack
-      pure (r, a)
-    )
-    (modify $ withRecursionStack tail)
+recursiveCleanup
+    :: TacticState
+    -> Maybe TacticError
+recursiveCleanup s =
+  let r = head $ ts_recursion_stack s
+   in traceShowId $ case r of
+        True  -> Nothing
+        False -> Just NoProgress
+
+
+filterT
+    :: (Monad m, Show s, Show ext)
+    => (s -> Maybe err)
+    -> (s -> s)
+    -> TacticT jdg ext err s m ()
+    -> TacticT jdg ext err s m ()
+filterT p s' t = do
+  s0 <- get
+  traceMX "state0" s0
+  tactic $ \j -> unRuleT $ do
+    e <- RuleT $ proofState t j
+    s <- get
+    traceMX "state" s
+    traceMX "extract" e
+    modify s'
+    case p s of
+      Just err -> throwError err
+      Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index bf788fea3f..82a1d24536 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -68,12 +68,8 @@ recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     localTactic (apply' name) $ introducing defs
-    (has_simple, _) <- recursionStackFrame assumption
-    case has_simple of
-      True -> traceM $ mappend "!!!recursion ok: " $ show defs
-      False -> do
-        traceM $ mappend "!!!recursion not ok >: " $ show defs
-        throwError NoProgress
+    modify $ withRecursionStack (False :)
+    filterT recursiveCleanup (withRecursionStack tail) assumption
 
 
 ------------------------------------------------------------------------------

From a480c197a42a638818fb9b86ea2fd0800c7d065a Mon Sep 17 00:00:00 2001
From: TOTBWF <reed.mullanix@calabrio.com>
Date: Mon, 5 Oct 2020 14:40:27 -0700
Subject: [PATCH 08/50] Fix FilterT

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 28 +++++++------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  5 ++--
 2 files changed, 13 insertions(+), 20 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1115a90a27..11570f51cc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -89,24 +89,16 @@ recursiveCleanup s =
         False -> Just NoProgress
 
 
-filterT
-    :: (Monad m, Show s, Show ext)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p s' t = do
-  s0 <- get
-  traceMX "state0" s0
-  tactic $ \j -> unRuleT $ do
-    e <- RuleT $ proofState t j
-    s <- get
-    traceMX "state" s
-    traceMX "extract" e
-    modify s'
-    case p s of
-      Just err -> throwError err
-      Nothing -> pure e
+filterT :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+filterT p f t = check >> t
+    where
+      check = rule $ \j -> do
+          e <- subgoal j
+          s <- get
+          modify f
+          case p s of
+            Just err -> throwError err
+            Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 82a1d24536..cd84680451 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -67,9 +67,10 @@ recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
-    localTactic (apply' name) $ introducing defs
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) assumption
+    filterT recursiveCleanup (withRecursionStack tail) $ do
+        localTactic (apply' name) $ introducing defs
+        assumption
 
 
 ------------------------------------------------------------------------------

From 8fa2a8340c737f2c6c87acef8e695ce8bd512c19 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 14:51:27 -0700
Subject: [PATCH 09/50] derive foldr

---
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 33 +++++++------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  6 ++--
 2 files changed, 16 insertions(+), 23 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 1115a90a27..cf6cb5891e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -88,25 +88,16 @@ recursiveCleanup s =
         True  -> Nothing
         False -> Just NoProgress
 
-
-filterT
-    :: (Monad m, Show s, Show ext)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p s' t = do
-  s0 <- get
-  traceMX "state0" s0
-  tactic $ \j -> unRuleT $ do
-    e <- RuleT $ proofState t j
-    s <- get
-    traceMX "state" s
-    traceMX "extract" e
-    modify s'
-    case p s of
-      Just err -> throwError err
-      Nothing -> pure e
+filterT :: (Monad m) => (s -> Maybe err) -> (s -> s) -> TacticT jdg ext err s m () -> TacticT jdg ext err s m ()
+filterT p f t = check >> t
+    where
+      check = rule $ \j -> do
+          e <- subgoal j
+          s <- get
+          modify f
+          case p s of
+            Just err -> throwError err
+            Nothing -> pure e
 
 
 finally :: MonadError e m => m a -> m () -> m a
@@ -132,14 +123,14 @@ scoreSolution
     -> [Judgement]
     -> ( Penalize Int  -- number of holes
        , Reward Bool   -- all bindings used
-       , Reward Int    -- number used bindings
        , Penalize Int  -- number of introduced bindings
+       , Reward Int    -- number used bindings
        )
 scoreSolution TacticState{..} holes
   = ( Penalize $ length holes
     , Reward $ S.null $ ts_intro_vals S.\\ ts_used_vals
-    , Reward $ S.size ts_used_vals
     , Penalize $ S.size ts_intro_vals
+    , Reward $ S.size ts_used_vals
     )
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 82a1d24536..58fda28b93 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -67,9 +67,11 @@ recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
-    localTactic (apply' name) $ introducing defs
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) assumption
+    filterT recursiveCleanup (withRecursionStack tail) $ do
+      localTactic (apply' name) $ introducing defs
+      assumption
+
 
 
 ------------------------------------------------------------------------------

From a6e40e1a35384f21333b5e52121a888afc07b2af Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 15:25:14 -0700
Subject: [PATCH 10/50] Test for foldr

---
 test/functional/Tactic.hs                    | 9 +++++----
 test/testdata/tactic/GoldenFoldr.hs          | 2 ++
 test/testdata/tactic/GoldenFoldr.hs.expected | 5 +++++
 3 files changed, 12 insertions(+), 4 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFoldr.hs
 create mode 100644 test/testdata/tactic/GoldenFoldr.hs.expected

diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index b70efb3376..f11717209e 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -86,15 +86,16 @@ tests = testGroup
       [ (not, DestructLambdaCase, "")
       ]
   , goldenTest "GoldenIntros.hs"            2 8  Intros ""
-  , goldenTest "GoldenEitherAuto.hs"        2 11 Auto   ""
-  , goldenTest "GoldenJoinCont.hs"          4 12 Auto   ""
-  , goldenTest "GoldenIdentityFunctor.hs"   3 11 Auto   ""
-  , goldenTest "GoldenIdTypeFam.hs"         7 11 Auto   ""
+  , goldenTest "GoldenEitherAuto.hs"        2 11 Auto ""
+  , goldenTest "GoldenJoinCont.hs"          4 12 Auto ""
+  , goldenTest "GoldenIdentityFunctor.hs"   3 11 Auto ""
+  , goldenTest "GoldenIdTypeFam.hs"         7 11 Auto ""
   , 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 "GoldenFromMaybe.hs"         2 13 Auto ""
+  , goldenTest "GoldenFoldr.hs"             2 10 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFoldr.hs b/test/testdata/tactic/GoldenFoldr.hs
new file mode 100644
index 0000000000..bade9c1e7a
--- /dev/null
+++ b/test/testdata/tactic/GoldenFoldr.hs
@@ -0,0 +1,2 @@
+foldr2 :: (a -> b -> b) -> b -> [a] -> b
+foldr2 = _
diff --git a/test/testdata/tactic/GoldenFoldr.hs.expected b/test/testdata/tactic/GoldenFoldr.hs.expected
new file mode 100644
index 0000000000..fe0463b75f
--- /dev/null
+++ b/test/testdata/tactic/GoldenFoldr.hs.expected
@@ -0,0 +1,5 @@
+foldr2 :: (a -> b -> b) -> b -> [a] -> b
+foldr2 = (\ f_b b l_a
+   -> case l_a of
+        [] -> b
+        ((:) a l_a4) -> f_b a (foldr2 f_b b l_a4))

From 7981a717d333664b1ffd0217814792d7e6b55654 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 15:29:44 -0700
Subject: [PATCH 11/50] Fix JoinCont test

---
 test/testdata/tactic/GoldenJoinCont.hs          | 2 +-
 test/testdata/tactic/GoldenJoinCont.hs.expected | 7 ++-----
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/test/testdata/tactic/GoldenJoinCont.hs b/test/testdata/tactic/GoldenJoinCont.hs
index a0cdb05da6..f2c63714da 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs
+++ b/test/testdata/tactic/GoldenJoinCont.hs
@@ -1,4 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
-joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
+joinCont :: Cont r (Cont r a) -> Cont r a
 joinCont = _
diff --git a/test/testdata/tactic/GoldenJoinCont.hs.expected b/test/testdata/tactic/GoldenJoinCont.hs.expected
index 306591b32c..ebf84d1371 100644
--- a/test/testdata/tactic/GoldenJoinCont.hs.expected
+++ b/test/testdata/tactic/GoldenJoinCont.hs.expected
@@ -1,7 +1,4 @@
 type Cont r a = ((a -> r) -> r)
 
-joinCont :: Show a => (a -> c) -> (b -> c) -> Either a b -> (c -> d) -> d
-joinCont = (\ fac fbc eab fcd
-   -> case eab of
-        (Left a) -> fcd (fac a)
-        (Right b) -> fcd (fbc b))
+joinCont :: Cont r (Cont r a) -> Cont r a
+joinCont = (\ f_r far -> f_r (\ f_r2 -> f_r2 far))

From 69d122bd689534eb07e719ee2736b765c8146d9a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 16:09:06 -0700
Subject: [PATCH 12/50] Use generic-lens

---
 haskell-language-server.cabal                 |  1 +
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 51 +++++++++----------
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 11 ----
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 19 +------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 33 +++++++-----
 5 files changed, 47 insertions(+), 68 deletions(-)

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index d931e72140..dfdf0789b3 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -158,6 +158,7 @@ executable haskell-language-server
     , refinery                 ^>=0.2
     , ghc-exactprint
     , fingertree
+    , generic-lens
 
   if flag(agpl)
     build-depends: brittany
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 50b4829f67..ed4d22bf69 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -1,8 +1,11 @@
-{-# LANGUAGE RecordWildCards #-}
-{-# LANGUAGE ViewPatterns    #-}
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE RecordWildCards  #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns     #-}
 
 module Ide.Plugin.Tactic.Judgements where
 
+import Control.Lens hiding (Context)
 import           Data.Char
 import           Data.Coerce
 import           Data.Map (Map)
@@ -14,6 +17,7 @@ import           Ide.Plugin.Tactic.Types
 import           OccName
 import           SrcLoc
 import           Type
+import Data.Generics.Product (field)
 
 
 ------------------------------------------------------------------------------
@@ -38,46 +42,41 @@ hasDestructed :: Judgement -> OccName -> Bool
 hasDestructed j n = S.member n $ _jDestructed j
 
 destructing :: OccName -> Judgement -> Judgement
-destructing n jdg@Judgement{..} = jdg
-  { _jDestructed = _jDestructed <> S.singleton n
-  }
+destructing n = field @"_jDestructed" <>~ S.singleton n
 
 blacklistingDestruct :: Judgement -> Judgement
-blacklistingDestruct jdg = jdg
-  { _jBlacklistDestruct = True
-  }
+blacklistingDestruct =
+  field @"_jBlacklistDestruct" .~ True
 
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
 withNewGoal :: a -> Judgement' a -> Judgement' a
-withNewGoal t jdg = jdg
-  { _jGoal = t
-  }
+withNewGoal t = field @"_jGoal" .~ t
 
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
-introducing ns jdg@Judgement{..} = jdg
-  { _jHypothesis = M.fromList ns <> _jHypothesis
-  }
+introducing ns =
+  field @"_jHypothesis" <>~ M.fromList ns
 
-withHypothesis :: (Map OccName a -> Map OccName a) -> Judgement' a -> Judgement' a
-withHypothesis f jdg@Judgement{..} = jdg
-  { _jHypothesis = f _jHypothesis
-  }
+withHypothesis
+    :: (Map OccName a -> Map OccName a)
+    -> Judgement' a
+    -> Judgement' a
+withHypothesis f =
+  field @"_jHypothesis" %~ f
 
 ------------------------------------------------------------------------------
 -- | Pattern vals are currently tracked in jHypothesis, with an extra piece of data sitting around in jPatternVals.
 introducingPat :: [(OccName, a)] -> Judgement' a -> Judgement' a
-introducingPat ns jdg@Judgement{..} = jdg
-  { _jHypothesis  = M.fromList ns <> _jHypothesis
-  , _jPatternVals = S.fromList (fmap fst ns) <> _jPatternVals
-  }
+introducingPat ns jdg = jdg
+  & field @"_jHypothesis"  <>~ M.fromList ns
+  & field @"_jPatternVals" <>~ S.fromList (fmap fst ns)
 
 
 disallowing :: [OccName] -> Judgement' a -> Judgement' a
-disallowing ns jdg@Judgement{..} = jdg
-  { _jHypothesis = M.withoutKeys _jHypothesis $ S.fromList ns
-  }
+disallowing ns =
+  field @"_jHypothesis" %~ flip M.withoutKeys (S.fromList ns)
+
 
 jHypothesis :: Judgement' a -> Map OccName a
 jHypothesis = _jHypothesis
@@ -98,5 +97,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 4aca416713..290f730390 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -106,16 +106,6 @@ filterT p f t = check >> t
             Nothing -> pure e
 
 
-finally :: MonadError e m => m a -> m () -> m a
-finally action cleanup = do
-  a <-
-    action `catchError` \e -> do
-      cleanup
-      throwError e
-  cleanup
-  pure a
-
-
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
@@ -123,7 +113,6 @@ setRecursionFrameData b = do
     []       -> []
 
 
-
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 717f1c1510..b7819b33a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -11,7 +11,6 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
-import           Control.Applicative
 import           Control.Monad
 import           Control.Monad.Except (throwError)
 import           Control.Monad.State.Class
@@ -73,22 +72,6 @@ recursion = do
       assumption
 
 
-------------------------------------------------------------------------------
--- | Introduce a lambda.
-intro :: TacticsM ()
-intro = rule $ \jdg -> do
-  let hy = jHypothesis jdg
-      g  = jGoal jdg
-  case splitFunTy_maybe $ unCType g of
-    Just (a, b) -> do
-      v <- pure $ mkGoodName (getInScope hy) a
-      let jdg' = introducing [(v, CType a)] $ withNewGoal (CType b) jdg
-      modify $ withIntroducedVals $ mappend $ S.singleton v
-      sg <- newSubgoal jdg'
-      pure $ noLoc $ lambda [bvar' v] $ unLoc sg
-    _ -> throwError $ GoalMismatch "intro" g
-
-
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
@@ -218,7 +201,7 @@ auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
-  intros <|> many_ intro
+  try intros
   choice
     [ attemptOn functionNames $ \fname -> do
         apply' fname
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index b4195c6573..99a05af917 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
 {-# LANGUAGE DerivingStrategies         #-}
@@ -18,6 +20,8 @@ module Ide.Plugin.Tactic.Types
   , Range
   ) where
 
+import Control.Lens hiding (Context)
+import Data.Generics.Product (field)
 import Control.Monad.Reader
 import Data.Function
 import Data.Map (Map)
@@ -64,40 +68,43 @@ data TacticState = TacticState
     , ts_used_vals :: !(Set OccName)
     , ts_intro_vals :: !(Set OccName)
     , ts_recursion_stack :: ![Bool]
-    } deriving stock Show
+    } deriving stock (Show, Generic)
+
 
 defaultTacticState :: TacticState
 defaultTacticState =
   TacticState mempty emptyTCvSubst mempty mempty mempty
 
+
 withRecursionStack
   :: ([Bool] -> [Bool]) -> TacticState -> TacticState
-withRecursionStack f ts = ts
-  { ts_recursion_stack = f $ ts_recursion_stack ts
-  }
+withRecursionStack f =
+  field @"ts_recursion_stack" %~ f
 
 
 withUsedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
-withUsedVals f ts = ts
-  { ts_used_vals = f $ ts_used_vals ts
-  }
+withUsedVals f =
+  field @"ts_used_vals" %~ f
+
 
 withIntroducedVals :: (Set OccName -> Set OccName) -> TacticState -> TacticState
-withIntroducedVals f ts = ts
-  { ts_intro_vals = f $ ts_intro_vals ts
-  }
+withIntroducedVals f =
+  field @"ts_intro_vals" %~ f
+
 
 
 ------------------------------------------------------------------------------
 -- | The current bindings and goal for a hole to be filled by refinery.
 data Judgement' a = Judgement
-  { _jHypothesis  :: !(Map OccName a)
-  , _jDestructed  :: !(Set OccName)
+  { _jHypothesis :: !(Map OccName a)
+  , _jDestructed :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
-  , _jGoal        :: !(a)
+  , _jPositionMaps :: !(Map OccName [OccName])
+  , _jAncestry     :: !(Map OccName OccName)
+  , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)
 

From a781803c6b77cdbeb0a3bef7e29d0741fa81fb15 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 19:54:32 -0700
Subject: [PATCH 13/50] Positionally-aware recursion

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 15 ++++--
 .../tactics/src/Ide/Plugin/Tactic/Debug.hs    |  5 ++
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 48 ++++++++++++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 34 ++++++++++--
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 52 ++++++++++++++-----
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  5 ++
 6 files changed, 137 insertions(+), 22 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 0b5c8c370b..3557e290c0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -33,7 +33,7 @@ useOccName jdg name =
 destructMatches
     :: (DataCon -> Judgement -> Rule)
        -- ^ How to construct each match
-    -> (Judgement -> Judgement)
+    -> ([(OccName, CType)] -> Judgement -> Judgement)
        -- ^ How to derive each match judgement
     -> CType
        -- ^ Type being destructed
@@ -51,12 +51,13 @@ destructMatches f f2 t jdg = do
         _ -> for dcs $ \dc -> do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
+          let hy' = zip names $ coerce args
 
           let pat :: Pat GhcPs
               pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
                   $ fmap bvar' names
-              j = f2
-                $ introducingPat (zip names $ coerce args)
+              j = f2 hy'
+                $ introducingPat hy'
                 $ withNewGoal g jdg
           sg <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
@@ -75,7 +76,11 @@ destruct' f term jdg = do
     Just (_, t) -> do
       useOccName jdg term
       fmap noLoc $ case' (var' term) <$>
-        destructMatches f (destructing term) t jdg
+        destructMatches
+          f
+          (\cs -> setParents term (fmap fst cs) . destructing term)
+          t
+          jdg
 
 
 ------------------------------------------------------------------------------
@@ -88,7 +93,7 @@ destructLambdaCase' f jdg = do
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
       fmap noLoc $ lambdaCase <$>
-        destructMatches f id (CType arg) jdg
+        destructMatches f (const id) (CType arg) jdg
     _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index c81ea6e59a..20acfc58ab 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -4,6 +4,7 @@ module Ide.Plugin.Tactic.Debug
   , traceM
   , traceShowId
   , trace
+  , traceX
   , traceMX
   ) where
 
@@ -21,3 +22,7 @@ unsafeRender' = showSDoc unsafeGlobalDynFlags
 
 traceMX :: (Monad m, Show a) => String -> a -> m ()
 traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
+
+traceX :: (Show a) => String -> a -> b -> b
+traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index ed4d22bf69..8a9c005d9b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DataKinds        #-}
 {-# LANGUAGE RecordWildCards  #-}
 {-# LANGUAGE TypeApplications #-}
@@ -58,6 +59,51 @@ introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+
+setParents
+    :: OccName    -- ^ parent
+    -> [OccName]  -- ^ children
+    -> Judgement
+    -> Judgement
+setParents p cs =
+  field @"_jAncestry" <>~ M.fromList (fmap (, p) cs)
+
+
+
+------------------------------------------------------------------------------
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
+-- in and of itself (see the note there.) Additionally, this doesn't check to
+-- make sure we're in the top-level scope, so it will set the recursive
+-- position mapping any time 'intros' is called.
+withPositionMapping :: Context -> [OccName] -> Judgement -> Judgement
+withPositionMapping ctx names j =
+  case M.member  defining (_jPositionMaps j) of
+    True  -> j
+    False ->
+      traceX "withPositionMapping hack" (defining, names)
+        $ j & field @"_jPositionMaps" . at defining ?~ names
+  where
+    defining = extremelyStupid__definingFunction ctx
+
+
+------------------------------------------------------------------------------
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined
+-- (eg, we might be in a where block). The head of this list is not guaranteed
+-- to be the one we're interested in.
+extremelyStupid__definingFunction :: Context -> OccName
+extremelyStupid__definingFunction =
+  fst . head . ctxDefiningFuncs
+
+
+withCurrentPosition :: Int -> Judgement -> Judgement
+withCurrentPosition i =
+  field @"_jCurrentPosition" ?~ i
+
+
 withHypothesis
     :: (Map OccName a -> Map OccName a)
     -> Judgement' a
@@ -97,5 +143,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty Nothing . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 290f730390..5a7378888e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,12 +18,15 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
+import           Control.Lens hiding (Context, matching, Empty)
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
-import           Control.Monad.State.Class (gets, modify, MonadState)
+import           Control.Monad.State (MonadState(..))
+import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
+import qualified Data.Map as M
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -35,7 +38,6 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
-import Control.Monad.State (MonadState(..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -79,12 +81,38 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
+--------------------------------------------------------------------------------
+-- TODO(sandy): this is probably the worst function I've ever written; sorry
+hasPositionalAncestry
+    :: Judgement
+    -> OccName     -- ^ defining fn
+    -> Int         -- ^ position
+    -> OccName     -- ^ thing to check ancestry
+    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
+                   -- just false if it's a descendent
+                   -- otherwise nothing
+hasPositionalAncestry jdg defn n name
+  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
+  = case name == ancestor of
+      True  -> Just True
+      False -> go ancestor name
+  | otherwise = Nothing
+  where
+    go ancestor who =
+      case M.lookup who $ _jAncestry  jdg of
+        Just parent ->
+          case parent == ancestor of
+            True  -> Just False
+            False -> go ancestor parent
+        Nothing -> Nothing
+
+
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
 recursiveCleanup s =
   let r = head $ ts_recursion_stack s
-   in traceShowId $ case r of
+   in case r of
         True  -> Nothing
         False -> Just NoProgress
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index b7819b33a6..80eafd3e37 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleContexts      #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -11,8 +13,9 @@ module Ide.Plugin.Tactic.Tactics
   , runTactic
   ) where
 
-import           Control.Monad
 import           Control.Monad.Except (throwError)
+import           Control.Monad.Reader (asks)
+import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
 import           Data.Function
@@ -37,7 +40,6 @@ import           TcType
 import           Type hiding (Var)
 
 
-
 ------------------------------------------------------------------------------
 -- | Use something in the hypothesis to fill the hole.
 assumption :: TacticsM ()
@@ -49,26 +51,41 @@ assumption = attemptOn allNames assume
 assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
+  defn <- asks extremelyStupid__definingFunction
   case M.lookup name $ jHypothesis jdg of
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
-          when (M.member name $ jPatHypothesis jdg) $ do
-            traceM $ "!!!simpler: " <> show name
-            setRecursionFrameData True
+          case _jCurrentPosition jdg of
+            -- If we have a current position (ie, we are in the context of
+            -- a recursive call):
+            Just pos ->
+              case hasPositionalAncestry jdg defn pos name of
+                -- If we are original arg, we're allowed to proceed.
+                Just True -> pure ()
+                -- If we are a descendent of the original arg, we are
+                -- guaranteed to be structurally smaller, and thus the
+                -- recursion won't be bottom.
+                Just False -> setRecursionFrameData True
+                -- Otherwise it doesn't make sense to use this variable,
+                -- because it is unrelated to the current argument in the
+                -- recursive call.
+                Nothing -> throwError $ RecursionOnWrongParam defn pos name
+            Nothing -> pure ()
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
+
 recursion :: TacticsM ()
 recursion = do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
     filterT recursiveCleanup (withRecursionStack tail) $ do
-      localTactic (apply' name) $ introducing defs
+      localTactic (apply' withCurrentPosition name) $ introducing defs
       assumption
 
 
@@ -78,11 +95,14 @@ intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
+  ctx <- ask
   case tcSplitFunTys $ unCType g of
     ([], _) -> throwError $ GoalMismatch "intro" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = introducing (zip vs $ coerce as) $ withNewGoal (CType b) jdg
+      let jdg' = withPositionMapping ctx vs
+               $ introducing (zip vs $ coerce as)
+               $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
       sg <- newSubgoal jdg'
       pure
@@ -121,8 +141,12 @@ homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
-apply' :: OccName -> TacticsM ()
-apply' func = do
+apply :: OccName -> TacticsM ()
+apply = apply' (const id)
+
+
+apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
+apply' f func = do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg
@@ -131,11 +155,13 @@ apply' func = do
           let (args, ret) = splitFunTys ty
           unify g (CType ret)
           useOccName jdg func
-          sgs <- traverse ( newSubgoal
+          sgs <- traverse ( \(i, t) ->
+                            newSubgoal
+                          . f i
                           . blacklistingDestruct
                           . flip withNewGoal jdg
-                          . CType
-                          ) args
+                          $ CType t
+                          ) $ zip [0..] args
           pure . noLoc
               . foldl' (@@) (var' func)
               $ fmap unLoc sgs
@@ -204,7 +230,7 @@ auto' n = do
   try intros
   choice
     [ attemptOn functionNames $ \fname -> do
-        apply' fname
+        apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
         progress ((==) `on` jGoal) NoProgress (destruct aname)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 99a05af917..8f4d805760 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -104,6 +104,7 @@ data Judgement' a = Judgement
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
   , _jAncestry     :: !(Map OccName OccName)
+  , _jCurrentPosition :: Maybe Int
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)
@@ -131,6 +132,7 @@ data TacticError
   | NoApplicableTactic
   | AlreadyDestructed OccName
   | IncorrectDataCon DataCon
+  | RecursionOnWrongParam OccName Int OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -160,6 +162,9 @@ instance Show TacticError where
       "Already destructed " <> unsafeRender name
     show (IncorrectDataCon dcon) =
       "Data con doesn't align with goal type (" <> unsafeRender dcon <> ")"
+    show (RecursionOnWrongParam call p arg) =
+      "Recursion on wrong param (" <> show call <> ") on arg"
+        <> show p <> ": " <> show arg
 
 
 ------------------------------------------------------------------------------

From 60ebb744ca9f31ad4c19a7dead4ecff6b57b7af4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 20:36:06 -0700
Subject: [PATCH 14/50] almost generate fmap for binary tree

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 2 +-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 5a7378888e..35d50c2cf8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -70,7 +70,7 @@ runTactic ctx jdg t =
           . flip runReader ctx
           . unExtractM
           $ runTacticTWithState t jdg tacticState of
-      (errs, []) -> Left $ errs
+      (errs, []) -> Left $ take 50 $ errs
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 80eafd3e37..69290d9361 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -59,7 +59,7 @@ assume name = rule $ \jdg -> do
           case _jCurrentPosition jdg of
             -- If we have a current position (ie, we are in the context of
             -- a recursive call):
-            Just pos ->
+            Just pos -> do
               case hasPositionalAncestry jdg defn pos name of
                 -- If we are original arg, we're allowed to proceed.
                 Just True -> pure ()
@@ -220,7 +220,7 @@ auto = do
   jdg <- goal
   traceM $ mappend "!!!auto current:" $ show current
   traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 5) $ disallowing $ fmap fst current
+  localTactic (auto' 4) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()

From 9714f7ecb4acb367c329b24718474bfd406cf659 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 5 Oct 2020 21:03:24 -0700
Subject: [PATCH 15/50] timeout tactic if it's too slow

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs | 36 +++++++++++++++---------
 1 file changed, 22 insertions(+), 14 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 199cc1a609..52b64bb8b1 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
@@ -50,6 +51,7 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           System.Timeout
 
 
 descriptor :: PluginId -> PluginDescriptor
@@ -266,20 +268,26 @@ 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
-        case runTactic ctx jdg
-              $ tac
-              $ mkVarOcc
-              $ T.unpack var_name of
-          Left err ->
-            pure $ (, Nothing)
-              $ Left
-              $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-          Right res -> do
-            let g = graft (RealSrcSpan span) res
-                response = transform dflags (clientCapabilities lf) uri g pm
-            pure $ case response of
-               Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
-               Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        x <- lift $ timeout 2e6 $
+          case runTactic ctx jdg
+                $ tac
+                $ mkVarOcc
+                $ T.unpack var_name of
+            Left err ->
+              pure $ (, Nothing)
+                $ Left
+                $ ResponseError InvalidRequest (T.pack $ show err) Nothing
+            Right res -> do
+              let g = graft (RealSrcSpan span) res
+                  response = transform dflags (clientCapabilities lf) uri g pm
+              pure $ case response of
+                Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
+                Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
+        pure $ case x of
+          Just y -> y
+          Nothing -> (, Nothing)
+                   $ Left
+                   $ ResponseError InvalidRequest "timed out" Nothing
 tacticCmd _ _ _ _ =
   pure ( Left $ ResponseError InvalidRequest (T.pack "Bad URI") Nothing
        , Nothing

From 3ac43d862f611a7c9ba0219a269ba2b656fcfc79 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 11:51:00 -0700
Subject: [PATCH 16/50] Simpler recursive hypothesis

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  1 +
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 31 +++++++++++++++++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 27 ----------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 25 +++------------
 4 files changed, 37 insertions(+), 47 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 3557e290c0..becb2690a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -127,3 +127,4 @@ var' = var . fromString . occNameString
 -- | Like 'bvar', but works over standard GHC 'OccName's.
 bvar' :: BVar a => OccName -> a
 bvar' = bvar . fromString . occNameString
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 8a9c005d9b..f1f7411033 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -59,6 +59,37 @@ introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+filterPosition :: OccName -> Int -> Judgement -> Judgement
+filterPosition defn pos jdg =
+    withHypothesis (M.filterWithKey go) jdg
+  where
+    go name _ = isJust $ hasPositionalAncestry jdg defn pos name
+
+--------------------------------------------------------------------------------
+-- TODO(sandy): this is probably the worst function I've ever written; sorry
+hasPositionalAncestry
+    :: Judgement
+    -> OccName     -- ^ defining fn
+    -> Int         -- ^ position
+    -> OccName     -- ^ thing to check ancestry
+    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
+                   -- just false if it's a descendent
+                   -- otherwise nothing
+hasPositionalAncestry jdg defn n name
+  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
+  = case name == ancestor of
+      True  -> Just True
+      False -> go ancestor name
+  | otherwise = Nothing
+  where
+    go ancestor who =
+      case M.lookup who $ _jAncestry  jdg of
+        Just parent ->
+          case parent == ancestor of
+            True  -> Just False
+            False -> go ancestor parent
+        Nothing -> Nothing
+
 
 setParents
     :: OccName    -- ^ parent
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 35d50c2cf8..51530bac25 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -18,7 +18,6 @@ module Ide.Plugin.Tactic.Machinery
   ) where
 
 import           Control.Applicative
-import           Control.Lens hiding (Context, matching, Empty)
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State (MonadState(..))
@@ -26,7 +25,6 @@ import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
-import qualified Data.Map as M
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -81,31 +79,6 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
---------------------------------------------------------------------------------
--- TODO(sandy): this is probably the worst function I've ever written; sorry
-hasPositionalAncestry
-    :: Judgement
-    -> OccName     -- ^ defining fn
-    -> Int         -- ^ position
-    -> OccName     -- ^ thing to check ancestry
-    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
-                   -- just false if it's a descendent
-                   -- otherwise nothing
-hasPositionalAncestry jdg defn n name
-  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
-  = case name == ancestor of
-      True  -> Just True
-      False -> go ancestor name
-  | otherwise = Nothing
-  where
-    go ancestor who =
-      case M.lookup who $ _jAncestry  jdg of
-        Just parent ->
-          case parent == ancestor of
-            True  -> Just False
-            False -> go ancestor parent
-        Nothing -> Nothing
-
 
 recursiveCleanup
     :: TacticState
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 69290d9361..04b19263ca 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -14,7 +14,6 @@ module Ide.Plugin.Tactic.Tactics
   ) where
 
 import           Control.Monad.Except (throwError)
-import           Control.Monad.Reader (asks)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
@@ -51,27 +50,13 @@ assumption = attemptOn allNames assume
 assume :: OccName -> TacticsM ()
 assume name = rule $ \jdg -> do
   let g  = jGoal jdg
-  defn <- asks extremelyStupid__definingFunction
   case M.lookup name $ jHypothesis jdg of
     Just ty ->
       case ty == jGoal jdg of
         True  -> do
-          case _jCurrentPosition jdg of
-            -- If we have a current position (ie, we are in the context of
-            -- a recursive call):
-            Just pos -> do
-              case hasPositionalAncestry jdg defn pos name of
-                -- If we are original arg, we're allowed to proceed.
-                Just True -> pure ()
-                -- If we are a descendent of the original arg, we are
-                -- guaranteed to be structurally smaller, and thus the
-                -- recursion won't be bottom.
-                Just False -> setRecursionFrameData True
-                -- Otherwise it doesn't make sense to use this variable,
-                -- because it is unrelated to the current argument in the
-                -- recursive call.
-                Nothing -> throwError $ RecursionOnWrongParam defn pos name
-            Nothing -> pure ()
+          case M.member name (jPatHypothesis jdg) of
+            True  -> setRecursionFrameData True
+            False -> pure ()
           useOccName jdg name
           pure $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
@@ -85,8 +70,8 @@ recursion = do
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
     filterT recursiveCleanup (withRecursionStack tail) $ do
-      localTactic (apply' withCurrentPosition name) $ introducing defs
-      assumption
+      (localTactic (apply' (const id) name) $ introducing defs)
+        <@> fmap (localTactic assumption . filterPosition name) [0..]
 
 
 ------------------------------------------------------------------------------

From 89a488aca78e4a5f708b9bbd4e3c470263792e7e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 11:53:36 -0700
Subject: [PATCH 17/50] Remove current position from jdg

---
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 19 ++++++-------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  1 -
 3 files changed, 7 insertions(+), 15 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index f1f7411033..fe1936e9b2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -108,15 +108,13 @@ setParents p cs =
 -- in and of itself (see the note there.) Additionally, this doesn't check to
 -- make sure we're in the top-level scope, so it will set the recursive
 -- position mapping any time 'intros' is called.
-withPositionMapping :: Context -> [OccName] -> Judgement -> Judgement
-withPositionMapping ctx names j =
-  case M.member  defining (_jPositionMaps j) of
+withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
+withPositionMapping defn names j =
+  case M.member defn (_jPositionMaps j) of
     True  -> j
     False ->
-      traceX "withPositionMapping hack" (defining, names)
-        $ j & field @"_jPositionMaps" . at defining ?~ names
-  where
-    defining = extremelyStupid__definingFunction ctx
+      traceX "withPositionMapping hack" (defn, names)
+        $ j & field @"_jPositionMaps" . at defn ?~ names
 
 
 ------------------------------------------------------------------------------
@@ -130,11 +128,6 @@ extremelyStupid__definingFunction =
   fst . head . ctxDefiningFuncs
 
 
-withCurrentPosition :: Int -> Judgement -> Judgement
-withCurrentPosition i =
-  field @"_jCurrentPosition" ?~ i
-
-
 withHypothesis
     :: (Map OccName a -> Map OccName a)
     -> Judgement' a
@@ -174,5 +167,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty Nothing . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 04b19263ca..928828d513 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -85,7 +85,7 @@ intros = rule $ \jdg -> do
     ([], _) -> throwError $ GoalMismatch "intro" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = withPositionMapping ctx vs
+      let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
                $ introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 8f4d805760..7ba39ef2b4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -104,7 +104,6 @@ data Judgement' a = Judgement
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
   , _jAncestry     :: !(Map OccName OccName)
-  , _jCurrentPosition :: Maybe Int
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From c774fe190c1b79c9edd296195dfcea0f7a08c14a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 12:09:26 -0700
Subject: [PATCH 18/50] Restrict homomorphic splits to positional args

---
 plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs    | 13 +++++++++----
 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 13 ++++++-------
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs    |  7 +++++++
 test/functional/Tactic.hs                           |  2 ++
 test/testdata/tactic/GoldenFmapTree.hs              |  4 ++++
 test/testdata/tactic/GoldenFmapTree.hs.expected     |  7 +++++++
 test/testdata/tactic/GoldenSwap.hs                  |  2 ++
 test/testdata/tactic/GoldenSwap.hs.expected         |  2 ++
 8 files changed, 39 insertions(+), 11 deletions(-)
 create mode 100644 test/testdata/tactic/GoldenFmapTree.hs
 create mode 100644 test/testdata/tactic/GoldenFmapTree.hs.expected
 create mode 100644 test/testdata/tactic/GoldenSwap.hs
 create mode 100644 test/testdata/tactic/GoldenSwap.hs.expected

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index becb2690a6..191b4e7c3b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -52,11 +52,13 @@ destructMatches f f2 t jdg = do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
+              dcon_name = nameOccName $ dataConName dc
 
           let pat :: Pat GhcPs
-              pat = conP (fromString $ occNameString $ nameOccName $ dataConName dc)
+              pat = conP (fromString $ occNameString dcon_name)
                   $ fmap bvar' names
               j = f2 hy'
+                $ withPositionMapping dcon_name names
                 $ introducingPat hy'
                 $ withNewGoal g jdg
           sg <- f dc j
@@ -106,11 +108,14 @@ buildDataCon
     -> RuleM (LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
-  sgs <- traverse ( newSubgoal
+      dcon_name = nameOccName $ dataConName dc
+  sgs <- traverse ( \(arg, n) ->
+                    newSubgoal
+                  . filterSameTypeFromOtherPositions dcon_name n
                   . blacklistingDestruct
                   . flip withNewGoal jdg
-                  . CType
-                  ) args
+                  $ CType arg
+                  ) $ zip args [0..]
   pure
     . noLoc
     . foldl' (@@)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index fe1936e9b2..5a3a6a11d8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -65,6 +65,12 @@ filterPosition defn pos jdg =
   where
     go name _ = isJust $ hasPositionalAncestry jdg defn pos name
 
+filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement
+filterSameTypeFromOtherPositions defn pos jdg =
+  let hy = jHypothesis $ filterPosition defn pos jdg
+      tys = S.fromList $ fmap snd $ M.toList hy
+   in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg
+
 --------------------------------------------------------------------------------
 -- TODO(sandy): this is probably the worst function I've ever written; sorry
 hasPositionalAncestry
@@ -101,13 +107,6 @@ setParents p cs =
 
 
 
-------------------------------------------------------------------------------
--- TODO(sandy): THIS THING IS A BIG BIG HACK
---
--- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
--- in and of itself (see the note there.) Additionally, this doesn't check to
--- make sure we're in the top-level scope, so it will set the recursive
--- position mapping any time 'intros' is called.
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
 withPositionMapping defn names j =
   case M.member defn (_jPositionMaps j) of
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 928828d513..e952c1ac41 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -76,6 +76,13 @@ recursion = do
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
+--
+-- TODO(sandy): THIS THING IS A BIG BIG HACK
+--
+-- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
+-- in and of itself (see the note there.) Additionally, this doesn't check to
+-- make sure we're in the top-level scope, so it will set the recursive
+-- position mapping any time 'intros' is called.
 intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs
index f11717209e..5b5a6b4154 100644
--- a/test/functional/Tactic.hs
+++ b/test/functional/Tactic.hs
@@ -96,6 +96,8 @@ tests = testGroup
   , goldenTest "GoldenListFmap.hs"          2 12 Auto ""
   , goldenTest "GoldenFromMaybe.hs"         2 13 Auto ""
   , goldenTest "GoldenFoldr.hs"             2 10 Auto ""
+  , goldenTest "GoldenSwap.hs"              2 8  Auto ""
+  , goldenTest "GoldenFmapTree.hs"          4 11 Auto ""
   ]
 
 
diff --git a/test/testdata/tactic/GoldenFmapTree.hs b/test/testdata/tactic/GoldenFmapTree.hs
new file mode 100644
index 0000000000..679e7902df
--- /dev/null
+++ b/test/testdata/tactic/GoldenFmapTree.hs
@@ -0,0 +1,4 @@
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+instance Functor Tree where
+   fmap = _
diff --git a/test/testdata/tactic/GoldenFmapTree.hs.expected b/test/testdata/tactic/GoldenFmapTree.hs.expected
new file mode 100644
index 0000000000..4e8b97d735
--- /dev/null
+++ b/test/testdata/tactic/GoldenFmapTree.hs.expected
@@ -0,0 +1,7 @@
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+instance Functor Tree where
+   fmap = (\ fab ta
+      -> case ta of
+           (Leaf a) -> Leaf (fab a)
+           (Branch ta2 ta3) -> Branch (fmap fab ta2) (fmap fab ta3))
diff --git a/test/testdata/tactic/GoldenSwap.hs b/test/testdata/tactic/GoldenSwap.hs
new file mode 100644
index 0000000000..9243955c54
--- /dev/null
+++ b/test/testdata/tactic/GoldenSwap.hs
@@ -0,0 +1,2 @@
+swap :: (a, b) -> (b, a)
+swap = _
diff --git a/test/testdata/tactic/GoldenSwap.hs.expected b/test/testdata/tactic/GoldenSwap.hs.expected
new file mode 100644
index 0000000000..4281fc81d9
--- /dev/null
+++ b/test/testdata/tactic/GoldenSwap.hs.expected
@@ -0,0 +1,2 @@
+swap :: (a, b) -> (b, a)
+swap = (\ p_ab -> case p_ab of { ((,) a b) -> (,) b a })

From 4b682a265815f9e1c5954d7aec14b8b5caf7e7d0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 6 Oct 2020 12:49:54 -0700
Subject: [PATCH 19/50] Silence a trace

---
 plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 5a3a6a11d8..d5e5efa78a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -111,9 +111,7 @@ withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
 withPositionMapping defn names j =
   case M.member defn (_jPositionMaps j) of
     True  -> j
-    False ->
-      traceX "withPositionMapping hack" (defn, names)
-        $ j & field @"_jPositionMaps" . at defn ?~ names
+    False -> j & field @"_jPositionMaps" . at defn ?~ names
 
 
 ------------------------------------------------------------------------------

From ab2e592ee7f290674de45917144c94b6ccbe4907 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 10:12:13 -0700
Subject: [PATCH 20/50] Better data provenance

(thanks to @i-am-tom for the idea!)
---
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 38 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  2 +-
 2 files changed, 23 insertions(+), 17 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index d5e5efa78a..f03adb169a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -6,9 +6,11 @@
 
 module Ide.Plugin.Tactic.Judgements where
 
-import Control.Lens hiding (Context)
+import           Control.Lens hiding (Context)
+import           Data.Bool
 import           Data.Char
 import           Data.Coerce
+import           Data.Generics.Product (field)
 import           Data.Map (Map)
 import qualified Data.Map as M
 import           Data.Maybe
@@ -18,7 +20,6 @@ import           Ide.Plugin.Tactic.Types
 import           OccName
 import           SrcLoc
 import           Type
-import Data.Generics.Product (field)
 
 
 ------------------------------------------------------------------------------
@@ -42,37 +43,43 @@ buildHypothesis
 hasDestructed :: Judgement -> OccName -> Bool
 hasDestructed j n = S.member n $ _jDestructed j
 
+
 destructing :: OccName -> Judgement -> Judgement
 destructing n = field @"_jDestructed" <>~ S.singleton n
 
+
 blacklistingDestruct :: Judgement -> Judgement
 blacklistingDestruct =
   field @"_jBlacklistDestruct" .~ True
 
+
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
+
 introducing :: [(OccName, a)] -> Judgement' a -> Judgement' a
 introducing ns =
   field @"_jHypothesis" <>~ M.fromList ns
 
+
 filterPosition :: OccName -> Int -> Judgement -> Judgement
 filterPosition defn pos jdg =
     withHypothesis (M.filterWithKey go) jdg
   where
     go name _ = isJust $ hasPositionalAncestry jdg defn pos name
 
+
 filterSameTypeFromOtherPositions :: OccName -> Int -> Judgement -> Judgement
 filterSameTypeFromOtherPositions defn pos jdg =
   let hy = jHypothesis $ filterPosition defn pos jdg
       tys = S.fromList $ fmap snd $ M.toList hy
    in withHypothesis (\hy2 -> M.filter (not . flip S.member tys) hy2 <> hy) jdg
 
---------------------------------------------------------------------------------
--- TODO(sandy): this is probably the worst function I've ever written; sorry
+
 hasPositionalAncestry
     :: Judgement
     -> OccName     -- ^ defining fn
@@ -85,16 +92,12 @@ hasPositionalAncestry jdg defn n name
   | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
   = case name == ancestor of
       True  -> Just True
-      False -> go ancestor name
+      False ->
+        case M.lookup name $ _jAncestry jdg of
+          Just ancestry ->
+            bool Nothing (Just False) $ S.member ancestor ancestry
+          Nothing -> Nothing
   | otherwise = Nothing
-  where
-    go ancestor who =
-      case M.lookup who $ _jAncestry  jdg of
-        Just parent ->
-          case parent == ancestor of
-            True  -> Just False
-            False -> go ancestor parent
-        Nothing -> Nothing
 
 
 setParents
@@ -102,9 +105,12 @@ setParents
     -> [OccName]  -- ^ children
     -> Judgement
     -> Judgement
-setParents p cs =
-  field @"_jAncestry" <>~ M.fromList (fmap (, p) cs)
-
+setParents p cs jdg =
+  let ancestry = mappend (S.singleton p)
+               $ fromMaybe mempty
+               $ M.lookup p
+               $ _jAncestry jdg
+   in jdg & field @"_jAncestry" <>~ M.fromList (fmap (, ancestry) cs)
 
 
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 7ba39ef2b4..3ff4be9799 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -103,7 +103,7 @@ data Judgement' a = Judgement
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
   , _jPositionMaps :: !(Map OccName [OccName])
-  , _jAncestry     :: !(Map OccName OccName)
+  , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From 5ddd36013226ed091d3b3e7150dc7d2ed064ecdd Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 11:57:37 -0700
Subject: [PATCH 21/50] Support multiple positional binding sets

---
 plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs   |  4 ++++
 .../tactics/src/Ide/Plugin/Tactic/Judgements.hs  | 16 +++++++++-------
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs   |  2 +-
 3 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
index 20acfc58ab..ba91a7c1cb 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Debug.hs
@@ -5,6 +5,7 @@ module Ide.Plugin.Tactic.Debug
   , traceShowId
   , trace
   , traceX
+  , traceIdX
   , traceMX
   ) where
 
@@ -26,3 +27,6 @@ traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a
 traceX :: (Show a) => String -> a -> b -> b
 traceX str a = trace (mappend ("!!!" <> str <> ": ") $ show a)
 
+traceIdX :: (Show a) => String -> a -> a
+traceIdX str a = trace (mappend ("!!!" <> str <> ": ") $ show a) a
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index f03adb169a..90d3f0ddb3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -89,15 +89,19 @@ hasPositionalAncestry
                    -- just false if it's a descendent
                    -- otherwise nothing
 hasPositionalAncestry jdg defn n name
-  | Just ancestor <- preview (_Just . ix n) $ M.lookup defn $ _jPositionMaps jdg
-  = case name == ancestor of
+  | not $ null ancestors
+  = case any (== name) ancestors of
       True  -> Just True
       False ->
         case M.lookup name $ _jAncestry jdg of
           Just ancestry ->
-            bool Nothing (Just False) $ S.member ancestor ancestry
+            bool Nothing (Just False) $ any (flip S.member ancestry) ancestors
           Nothing -> Nothing
   | otherwise = Nothing
+  where
+    ancestors = toListOf (_Just . traversed . ix n)
+              $ M.lookup defn
+              $ _jPositionMaps jdg
 
 
 setParents
@@ -114,10 +118,8 @@ setParents p cs jdg =
 
 
 withPositionMapping :: OccName -> [OccName] -> Judgement -> Judgement
-withPositionMapping defn names j =
-  case M.member defn (_jPositionMaps j) of
-    True  -> j
-    False -> j & field @"_jPositionMaps" . at defn ?~ names
+withPositionMapping defn names =
+  field @"_jPositionMaps" . at defn <>~ Just [names]
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 3ff4be9799..e04815ac16 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -102,7 +102,7 @@ data Judgement' a = Judgement
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
-  , _jPositionMaps :: !(Map OccName [OccName])
+  , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
   }

From a3dc93532571820786095a814a2907bde6075f6b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 13:01:02 -0700
Subject: [PATCH 22/50] Prune destructing on pattern vals if they don't
 introduce new types

(thanks to @Lysxia for the insight)
---
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  4 ++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 21 ++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 22 ++++++++++++++++++-
 3 files changed, 46 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 90d3f0ddb3..2b45e40a8f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -157,6 +157,10 @@ jHypothesis :: Judgement' a -> Map OccName a
 jHypothesis = _jHypothesis
 
 
+isPatVal :: Judgement' a -> OccName -> Bool
+isPatVal j n = S.member n $ _jPatternVals j
+
+
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
 jPatHypothesis :: Judgement' a -> Map OccName a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 51530bac25..9f14cc1856 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -107,6 +107,27 @@ filterT p f t = check >> t
             Nothing -> pure e
 
 
+gather
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m a
+    -> ([(a, jdg)] -> TacticT jdg ext err s m a)
+    -> TacticT jdg ext err s m a
+gather t f = tactic $ \j -> do
+    s <- get
+    results <- lift $ proofs s $ proofState t j
+    msum $ flip fmap results $ \case
+        Left err -> throwError err
+        Right (_, jdgs) -> proofState (f jdgs) j
+
+
+pruning
+    :: (MonadExtract ext m)
+    => TacticT jdg ext err s m ()
+    -> ([jdg] -> Maybe err)
+    -> TacticT jdg ext err s m ()
+pruning t p = gather t (maybe (pure ()) throwError . p . fmap snd)
+
+
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e952c1ac41..e944a2d681 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -103,6 +103,26 @@ intros = rule $ \jdg -> do
         $ unLoc sg
 
 
+------------------------------------------------------------------------------
+-- | Case split, and leave holes in the matches.
+destructAuto :: OccName -> TacticsM ()
+destructAuto name = do
+  jdg <- goal
+  case hasDestructed jdg name of
+    True -> throwError $ AlreadyDestructed name
+    False ->
+      let subtactic = rule $ destruct' (const subgoal) name
+       in case isPatVal jdg name of
+            True  ->
+              pruning subtactic $ \jdgs ->
+                let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis
+                    new_hy = foldMap getHyTypes jdgs
+                    old_hy = getHyTypes jdg
+                 in case S.null (traceIdX "newly introduced bindings" $ new_hy S.\\old_hy) of
+                      True  -> Just NoProgress
+                      False -> Nothing
+            False -> subtactic
+
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: OccName -> TacticsM ()
@@ -225,7 +245,7 @@ auto' n = do
         apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
-        progress ((==) `on` jGoal) NoProgress (destruct aname)
+        progress ((==) `on` jGoal) NoProgress (destructAuto aname)
         loop
     , split >> loop
     , assumption >> loop

From abd365fdcf4e39ba8f1f78901ae6cf654353e7a1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:15:02 -0700
Subject: [PATCH 23/50] Fix pruning to actually run the tactic

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 2 +-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 9 ++++-----
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs     | 3 +++
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 9f14cc1856..254ef19ccd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -125,7 +125,7 @@ pruning
     => TacticT jdg ext err s m ()
     -> ([jdg] -> Maybe err)
     -> TacticT jdg ext err s m ()
-pruning t p = gather t (maybe (pure ()) throwError . p . fmap snd)
+pruning t p = gather t $ maybe t throwError . p . fmap snd
 
 
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index e944a2d681..81689857e0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -17,7 +17,6 @@ import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
-import           Data.Function
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
@@ -113,13 +112,13 @@ destructAuto name = do
     False ->
       let subtactic = rule $ destruct' (const subgoal) name
        in case isPatVal jdg name of
-            True  ->
+            True ->
               pruning subtactic $ \jdgs ->
                 let getHyTypes = S.fromList . fmap snd . M.toList . jHypothesis
                     new_hy = foldMap getHyTypes jdgs
                     old_hy = getHyTypes jdg
-                 in case S.null (traceIdX "newly introduced bindings" $ new_hy S.\\old_hy) of
-                      True  -> Just NoProgress
+                 in case S.null $ new_hy S.\\ old_hy of
+                      True  -> Just $ UnhelpfulDestruct name
                       False -> Nothing
             False -> subtactic
 
@@ -245,7 +244,7 @@ auto' n = do
         apply fname
         loop
     , attemptOn algebraicNames $ \aname -> do
-        progress ((==) `on` jGoal) NoProgress (destructAuto aname)
+        destructAuto aname
         loop
     , split >> loop
     , assumption >> loop
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index e04815ac16..c7d722f5e4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -132,6 +132,7 @@ data TacticError
   | AlreadyDestructed OccName
   | IncorrectDataCon DataCon
   | RecursionOnWrongParam OccName Int OccName
+  | UnhelpfulDestruct OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -164,6 +165,8 @@ instance Show TacticError where
     show (RecursionOnWrongParam call p arg) =
       "Recursion on wrong param (" <> show call <> ") on arg"
         <> show p <> ": " <> show arg
+    show (UnhelpfulDestruct n) =
+      "Destructing patval " <> show n <> " leads to no new types"
 
 
 ------------------------------------------------------------------------------

From 8d530324e1b9309301cafd4170c762873e74dbc1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:30:59 -0700
Subject: [PATCH 24/50] Count duplicates

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 13 ++++++++++++-
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs   |  4 ++--
 2 files 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 254ef19ccd..73f32f1417 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -24,7 +24,9 @@ import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
-import           Data.List (intercalate, sortBy)
+import           Data.Function (on)
+import           Data.List (groupBy, intercalate, sortBy)
+import           Data.Maybe (listToMaybe, fromMaybe)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -73,6 +75,7 @@ runTactic ctx jdg t =
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
         traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
+        traceMX "duplicates" $ countDuplicates solns
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
@@ -135,6 +138,14 @@ setRecursionFrameData b = do
     []       -> []
 
 
+countDuplicates :: Show a => [a] -> [Int]
+countDuplicates
+    = sortBy (comparing Down)
+    . fmap length
+    . groupBy ((==) `on` show)
+    . sortBy (comparing show)
+
+
 scoreSolution
     :: TacticState
     -> [Judgement]
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 81689857e0..2d325b76a0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -88,7 +88,7 @@ intros = rule $ \jdg -> do
       g  = jGoal jdg
   ctx <- ask
   case tcSplitFunTys $ unCType g of
-    ([], _) -> throwError $ GoalMismatch "intro" g
+    ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
       let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
@@ -187,7 +187,7 @@ split = do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
-    Nothing -> throwError $ GoalMismatch "getGoalTyCon" g
+    Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs

From b8b0d0dc77ec1ae3f0e823ee7920e2fa1377eb5d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 21:35:34 -0700
Subject: [PATCH 25/50] ?

---
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 73f32f1417..b8a160429a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -24,9 +24,7 @@ import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
 import           Data.Coerce
 import           Data.Either
-import           Data.Function (on)
-import           Data.List (groupBy, intercalate, sortBy)
-import           Data.Maybe (listToMaybe, fromMaybe)
+import           Data.List (intercalate, sortBy)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -75,14 +73,12 @@ runTactic ctx jdg t =
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
         traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
-        traceMX "duplicates" $ countDuplicates solns
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
           _ -> Left []
 
 
-
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
@@ -138,14 +134,6 @@ setRecursionFrameData b = do
     []       -> []
 
 
-countDuplicates :: Show a => [a] -> [Int]
-countDuplicates
-    = sortBy (comparing Down)
-    . fmap length
-    . groupBy ((==) `on` show)
-    . sortBy (comparing show)
-
-
 scoreSolution
     :: TacticState
     -> [Judgement]

From ec13e9fcd43f41f94fdd686e1f34ae8a23420c60 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Wed, 7 Oct 2020 23:06:00 -0700
Subject: [PATCH 26/50] Don't allow splitting if it doesn't buy you anything

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  2 +-
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 11 +++++++-
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 25 ++++++++++++++++---
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  4 +++
 5 files changed, 38 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 52b64bb8b1..d06fb16282 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -268,7 +268,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 $
+        x <- lift $ timeout 2e8 $
           case runTactic ctx jdg
                 $ tac
                 $ mkVarOcc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 2b45e40a8f..ab152cd7c5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -53,10 +53,19 @@ blacklistingDestruct =
   field @"_jBlacklistDestruct" .~ True
 
 
+unwhitelistingSplit :: Judgement -> Judgement
+unwhitelistingSplit =
+  field @"_jWhitelistSplit" .~ False
+
+
 isDestructBlacklisted :: Judgement -> Bool
 isDestructBlacklisted = _jBlacklistDestruct
 
 
+isSplitWhitelisted :: Judgement -> Bool
+isSplitWhitelisted = _jWhitelistSplit
+
+
 withNewGoal :: a -> Judgement' a -> Judgement' a
 withNewGoal t = field @"_jGoal" .~ t
 
@@ -176,5 +185,5 @@ substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
 mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False mempty mempty . CType
+mkFirstJudgement hy = Judgement hy mempty mempty False True mempty mempty . CType
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index b8a160429a..eae8613874 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -72,7 +72,7 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 5 $  fmap (show . fst) sorted
+        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 50 $  fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 2d325b76a0..c5f5ac853e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -36,6 +36,8 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Name (nameOccName)
+import DataCon
 
 
 ------------------------------------------------------------------------------
@@ -192,6 +194,23 @@ split = do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs
 
+------------------------------------------------------------------------------
+-- | Choose between each of the goal's data constructors.
+splitAuto :: TacticsM ()
+splitAuto = do
+  jdg <- goal
+  let g = jGoal jdg
+  case splitTyConApp_maybe $ unCType g of
+    Nothing -> throwError $ GoalMismatch "split" g
+    Just (tc, _) -> do
+      let dcs = tyConDataCons tc
+      case isSplitWhitelisted jdg of
+        True -> choice $ fmap splitDataCon dcs
+        False -> choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+          case any ((/= jGoal jdg)  . jGoal) jdgs of
+            True  -> Nothing
+            False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+
 
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
@@ -201,7 +220,7 @@ splitDataCon dc = rule $ \jdg -> do
   case splitTyConApp_maybe $ unCType g of
     Just (tc, apps) -> do
       case elem dc $ tyConDataCons tc of
-        True -> buildDataCon jdg dc apps
+        True -> buildDataCon (unwhitelistingSplit jdg) dc apps
         False -> throwError $ IncorrectDataCon dc
     Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
@@ -231,7 +250,7 @@ auto = do
   jdg <- goal
   traceM $ mappend "!!!auto current:" $ show current
   traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 4) $ disallowing $ fmap fst current
+  localTactic (auto' 5) $ disallowing $ fmap fst current
 
 
 auto' :: Int -> TacticsM ()
@@ -246,7 +265,7 @@ auto' n = do
     , attemptOn algebraicNames $ \aname -> do
         destructAuto aname
         loop
-    , split >> loop
+    , 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 c7d722f5e4..624ecc9e76 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -102,6 +102,7 @@ data Judgement' a = Judgement
   , _jPatternVals :: !(Set OccName)
     -- ^ These should align with keys of _jHypothesis
   , _jBlacklistDestruct :: !(Bool)
+  , _jWhitelistSplit :: !(Bool)
   , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
   , _jGoal         :: !(a)
@@ -133,6 +134,7 @@ data TacticError
   | IncorrectDataCon DataCon
   | RecursionOnWrongParam OccName Int OccName
   | UnhelpfulDestruct OccName
+  | UnhelpfulSplit OccName
   deriving stock (Eq)
 
 instance Show TacticError where
@@ -167,6 +169,8 @@ instance Show TacticError where
         <> show p <> ": " <> show arg
     show (UnhelpfulDestruct n) =
       "Destructing patval " <> show n <> " leads to no new types"
+    show (UnhelpfulSplit n) =
+      "Splitting constructor " <> show n <> " leads to no new goals"
 
 
 ------------------------------------------------------------------------------

From 683c7914e937ba3d9258486e102b92b36fa4be7c Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 8 Oct 2020 10:33:32 -0700
Subject: [PATCH 27/50] Known fmap strategy

---
 haskell-language-server.cabal                 |  2 +
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  1 +
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs | 18 +++++++++
 .../src/Ide/Plugin/Tactic/KnownStrategies.hs  | 37 +++++++++++++++++++
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 34 ++++++-----------
 5 files changed, 69 insertions(+), 23 deletions(-)
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
 create mode 100644 plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index dfdf0789b3..4cca9280fd 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -93,11 +93,13 @@ executable haskell-language-server
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
     Ide.Plugin.Tactic
+    Ide.Plugin.Tactic.Auto
     Ide.Plugin.Tactic.CodeGen
     Ide.Plugin.Tactic.Context
     Ide.Plugin.Tactic.Debug
     Ide.Plugin.Tactic.GHC
     Ide.Plugin.Tactic.Judgements
+    Ide.Plugin.Tactic.KnownStrategies
     Ide.Plugin.Tactic.Machinery
     Ide.Plugin.Tactic.Naming
     Ide.Plugin.Tactic.Range
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index d06fb16282..2d1dc085c4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -39,6 +39,7 @@ import qualified FastString
 import           GHC.Generics (Generic)
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin (mkLspCommand)
+import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.Context
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
new file mode 100644
index 0000000000..40ff05b089
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -0,0 +1,18 @@
+module Ide.Plugin.Tactic.Auto where
+
+import Control.Applicative
+import Ide.Plugin.Tactic.Context
+import Ide.Plugin.Tactic.Judgements
+import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+
+
+------------------------------------------------------------------------------
+-- | Automatically solve a goal.
+auto :: TacticsM ()
+auto = do
+  current <- getCurrentDefinitions
+  knownStrategies
+    <|> (localTactic (auto' 4) $ disallowing $ fmap fst current)
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
new file mode 100644
index 0000000000..0855cd97e8
--- /dev/null
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Ide.Plugin.Tactic.KnownStrategies where
+
+import Control.Monad.Error.Class
+import Ide.Plugin.Tactic.Context (getCurrentDefinitions)
+import Ide.Plugin.Tactic.Tactics
+import Ide.Plugin.Tactic.Types
+import OccName (mkVarOcc)
+import Refinery.Tactic
+
+
+knownStrategies :: TacticsM ()
+knownStrategies = choice
+  [ deriveFmap
+  ]
+
+
+known :: String -> TacticsM () -> TacticsM ()
+known name t = do
+  getCurrentDefinitions >>= \case
+    [(def, _)] | def == mkVarOcc name -> do
+      traceMX "running known strategy" name
+      t
+    _ -> throwError NoApplicableTactic
+
+
+deriveFmap :: TacticsM ()
+deriveFmap = known "fmap" $ do
+  try intros
+  overAlgebraicTerms homo
+  choice
+    [ overFunctions apply >> auto' 2
+    , assumption
+    , recursion
+    ]
+
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index c5f5ac853e..7ea75eb1fb 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -21,6 +21,7 @@ import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
 import qualified Data.Set as S
+import           DataCon
 import           Development.IDE.GHC.Compat
 import           GHC.Exts
 import           GHC.SourceGen.Expr
@@ -32,12 +33,11 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
+import           Name (nameOccName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Name (nameOccName)
-import DataCon
 
 
 ------------------------------------------------------------------------------
@@ -242,27 +242,16 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
-------------------------------------------------------------------------------
--- | Automatically solve a goal.
-auto :: TacticsM ()
-auto = do
-  current <- getCurrentDefinitions
-  jdg <- goal
-  traceM $ mappend "!!!auto current:" $ show current
-  traceM $ mappend "!!!auto jdg:" $ show jdg
-  localTactic (auto' 5) $ disallowing $ fmap fst current
-
-
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
   let loop = auto' (n - 1)
   try intros
   choice
-    [ attemptOn functionNames $ \fname -> do
+    [ overFunctions $ \fname -> do
         apply fname
         loop
-    , attemptOn algebraicNames $ \aname -> do
+    , overAlgebraicTerms $ \aname -> do
         destructAuto aname
         loop
     , splitAuto >> loop
@@ -270,15 +259,14 @@ auto' n = do
     , recursion
     ]
 
+overFunctions :: (OccName -> TacticsM ()) -> TacticsM ()
+overFunctions =
+  attemptOn $ M.keys . M.filter (isFunction . unCType) . jHypothesis
 
-functionNames :: Judgement -> [OccName]
-functionNames  =
-  M.keys . M.filter (isFunction . unCType) . jHypothesis
-
-
-algebraicNames :: Judgement -> [OccName]
-algebraicNames =
-  M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
+overAlgebraicTerms :: (OccName -> TacticsM ()) -> TacticsM ()
+overAlgebraicTerms =
+  attemptOn $
+    M.keys . M.filter (isJust . algebraicTyCon . unCType) . jHypothesis
 
 
 allNames :: Judgement -> [OccName]

From 4114d03aa9aba971f0ec962c6aad34832029b746 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 13:19:19 -0700
Subject: [PATCH 28/50] Commit to a known solution if one exists

---
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs      | 8 ++++++--
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 3 +++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 40ff05b089..6a51601a39 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -6,13 +6,17 @@ import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
+import Refinery.Tactic
 
 
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
 auto = do
+  jdg <- goal
   current <- getCurrentDefinitions
-  knownStrategies
-    <|> (localTactic (auto' 4) $ disallowing $ fmap fst current)
+  traceMX "goal" jdg
+  commit
+    knownStrategies
+    (localTactic (auto' 4) $ disallowing $ fmap fst current)
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index eae8613874..04e1cf4cac 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -182,6 +182,9 @@ proofs' s p = go s [] p
           in go s' goals p
       go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
       go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
+      go s goals (Commit p1 p2) = go s goals p1 >>= \case
+          (rights -> []) -> go s goals p2
+          solns -> pure solns
       go _ _ Empty = pure []
       go _ _ (Failure err) = pure [throwError err]
       go s goals (Axiom ext) = pure [Right (ext, (s, goals))]

From 6ff650473d56d5298f8825f6e878c13111e6ea39 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:12:15 -0700
Subject: [PATCH 29/50] Compute top level position vals

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs | 45 ++++++++++++++++++++++++
 1 file changed, 45 insertions(+)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 2d1dc085c4..06782e36d8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -21,8 +21,12 @@ import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
 import           Data.Coerce
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
+import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
+import           Data.Monoid
 import qualified Data.Set as S
 import qualified Data.Text as T
 import           Data.Traversable
@@ -52,6 +56,7 @@ import           Ide.Types
 import           Language.Haskell.LSP.Core (clientCapabilities)
 import           Language.Haskell.LSP.Types
 import           OccName
+import           SrcLoc (containsSpan)
 import           System.Timeout
 
 
@@ -252,6 +257,7 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
+  traceMX "holes!" $ isRhsHole rss $ tm_typechecked_source $ tmrModule tcmod
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
@@ -301,3 +307,42 @@ fromMaybeT def = fmap (fromMaybe def) . runMaybeT
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
+
+------------------------------------------------------------------------------
+-- | Compute top-level position vals of a function
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
+isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
+  (Match _
+      (FunRhs (L _ name) _ _)         -- function name
+      ps                              -- patterns
+      (GRHSs _
+        [L _ (GRHS _ []
+               (L (RealSrcSpan span)  -- body with no guards and a single defn
+                  (HsVar _ (L _ hole))))] _)
+          :: Match GhcTc (LHsExpr GhcTc))
+    | containsSpan span rss           -- which contains our span
+    , isHole $ occName hole           -- and the span is a hole
+    -> First $ do
+        patnames <- traverse getPatName ps
+        pure (occName name, patnames)
+  _ -> mempty
+  ) tcs
+
+
+-- TODO(sandy): Make this more robust
+isHole :: OccName -> Bool
+isHole = isPrefixOf "_" . occNameString
+
+
+getPatName :: Pat GhcTc -> Maybe OccName
+getPatName = \case
+   VarPat _ x    -> Just $ occName $ unLoc x
+   LazyPat _ p   -> getPatName p
+   AsPat _ x _   -> Just $ occName $ unLoc x
+   ParPat _ p    -> getPatName p
+   BangPat _ p   -> getPatName p
+   ViewPat _ _ p -> getPatName p
+   SigPat _ p _  -> getPatName p
+   XPat p        -> getPatName $ unLoc p
+   _             -> Nothing
+

From 29858b0bab568237a603d74c5f8eb9613303f775 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:30:01 -0700
Subject: [PATCH 30/50] Add tophole to jdg

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      | 56 ++++++++++++++-----
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs |  1 -
 .../src/Ide/Plugin/Tactic/Judgements.hs       | 19 ++++++-
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    |  1 +
 4 files changed, 60 insertions(+), 17 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 06782e36d8..1dbccedfa0 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE NumDecimals         #-}
 {-# LANGUAGE OverloadedStrings   #-}
+{-# LANGUAGE PatternSynonyms     #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE TypeApplications    #-}
@@ -257,14 +258,26 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
-  traceMX "holes!" $ isRhsHole rss $ tm_typechecked_source $ tmrModule tcmod
+  -- traceMX "holes!" $ isRhsHole rss $
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
+      tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
               (mapMaybe (sequenceA . (occName *** coerce))
                 $ getDefiningBindings binds rss)
               tcg
       hyps = hypothesisFromBindings rss binds
-  pure (resulting_range, mkFirstJudgement hyps goal, ctx, dflags)
+  pure ( resulting_range
+       , mkFirstJudgement
+           hyps
+           (isRhsHole rss tcs)
+           (maybe
+              mempty
+              (uncurry M.singleton . fmap pure)
+                $ getRhsPosVals rss tcs)
+           goal
+       , ctx
+       , dflags
+       )
 
 
 
@@ -308,20 +321,24 @@ liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
 
+------------------------------------------------------------------------------
+-- | Is this hole immediately to the right of an equals sign?
+isRhsHole :: RealSrcSpan -> TypecheckedSource -> Bool
+isRhsHole rss tcs = everything (||) (mkQ False $ \case
+  TopLevelRHS _ _ (L (RealSrcSpan span) _) -> containsSpan rss span
+  _ -> False
+  ) tcs
+
+
 ------------------------------------------------------------------------------
 -- | Compute top-level position vals of a function
-isRhsHole :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
-isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
-  (Match _
-      (FunRhs (L _ name) _ _)         -- function name
-      ps                              -- patterns
-      (GRHSs _
-        [L _ (GRHS _ []
-               (L (RealSrcSpan span)  -- body with no guards and a single defn
-                  (HsVar _ (L _ hole))))] _)
-          :: Match GhcTc (LHsExpr GhcTc))
-    | containsSpan span rss           -- which contains our span
-    , isHole $ occName hole           -- and the span is a hole
+getRhsPosVals :: RealSrcSpan -> TypecheckedSource -> Maybe (OccName, [OccName])
+getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
+  TopLevelRHS name ps
+      (L (RealSrcSpan span)  -- body with no guards and a single defn
+         (HsVar _ (L _ hole)))
+    | containsSpan rss span  -- which contains our span
+    , isHole $ occName hole  -- and the span is a hole
     -> First $ do
         patnames <- traverse getPatName ps
         pure (occName name, patnames)
@@ -329,6 +346,17 @@ isRhsHole rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
   ) tcs
 
 
+------------------------------------------------------------------------------
+-- | Should make sure it's a fun bind
+pattern TopLevelRHS :: OccName -> [Pat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
+pattern TopLevelRHS name ps body <-
+  Match _
+    (FunRhs (L _ (occName -> name)) _ _)
+    ps
+    (GRHSs _
+      [L _ (GRHS _ [] body)] _)
+
+
 -- TODO(sandy): Make this more robust
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 6a51601a39..4aadd75ee2 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -1,6 +1,5 @@
 module Ide.Plugin.Tactic.Auto where
 
-import Control.Applicative
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index ab152cd7c5..57cf95e7ed 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -184,6 +184,21 @@ jGoal = _jGoal
 substJdg :: TCvSubst -> Judgement -> Judgement
 substJdg subst = fmap $ coerce . substTy subst . coerce
 
-mkFirstJudgement :: M.Map OccName CType -> Type -> Judgement' CType
-mkFirstJudgement hy = Judgement hy mempty mempty False True mempty mempty . CType
+mkFirstJudgement
+    :: M.Map OccName CType
+    -> 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
+  { _jHypothesis        = hy
+  , _jDestructed        = mempty
+  , _jPatternVals       = mempty
+  , _jBlacklistDestruct = False
+  , _jWhitelistSplit    = True
+  , _jPositionMaps      = posvals
+  , _jAncestry          = mempty
+  , _jIsTopHole         = top
+  , _jGoal              = CType goal
+  }
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 624ecc9e76..cca6fe8247 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -105,6 +105,7 @@ data Judgement' a = Judgement
   , _jWhitelistSplit :: !(Bool)
   , _jPositionMaps :: !(Map OccName [[OccName]])
   , _jAncestry     :: !(Map OccName (Set OccName))
+  , _jIsTopHole    :: !Bool
   , _jGoal         :: !(a)
   }
   deriving stock (Eq, Ord, Generic, Functor, Show)

From 929bcc94f34791c1f948b4286cfc5335e7a24338 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:36:16 -0700
Subject: [PATCH 31/50] Cleanup ugly hack in intros! \o/

---
 .../src/Ide/Plugin/Tactic/Judgements.hs       |  6 ++++++
 .../src/Ide/Plugin/Tactic/Machinery.hs        |  4 +++-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 19 +++++++++----------
 3 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
index 57cf95e7ed..32ad70bc2e 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Judgements.hs
@@ -169,6 +169,12 @@ jHypothesis = _jHypothesis
 isPatVal :: Judgement' a -> OccName -> Bool
 isPatVal j n = S.member n $ _jPatternVals j
 
+isTopHole :: Judgement' a -> Bool
+isTopHole = _jIsTopHole
+
+unsetIsTopHole :: Judgement' a -> Judgement' a
+unsetIsTopHole = field @"_jIsTopHole" .~ False
+
 
 ------------------------------------------------------------------------------
 -- | Only the hypothesis members which are pattern vals
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 04e1cf4cac..8228feee00 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -50,7 +50,9 @@ newSubgoal
     -> RuleM (LHsExpr GhcPs)
 newSubgoal j = do
     unifier <- gets ts_unifier
-    subgoal $ substJdg unifier j
+    subgoal
+      $ substJdg unifier
+      $ unsetIsTopHole j
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7ea75eb1fb..2fd8aef1e4 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -38,6 +38,7 @@ import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
+import Data.Bool (bool)
 
 
 ------------------------------------------------------------------------------
@@ -77,13 +78,6 @@ recursion = do
 
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
---
--- TODO(sandy): THIS THING IS A BIG BIG HACK
---
--- Why? Two reasons. It uses extremelyStupid__definingFunction, which is stupid
--- in and of itself (see the note there.) Additionally, this doesn't check to
--- make sure we're in the top-level scope, so it will set the recursive
--- position mapping any time 'intros' is called.
 intros :: TacticsM ()
 intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
@@ -93,11 +87,16 @@ intros = rule $ \jdg -> do
     ([], _) -> throwError $ GoalMismatch "intros" g
     (as, b) -> do
       vs <- mkManyGoodNames hy as
-      let jdg' = withPositionMapping (extremelyStupid__definingFunction ctx) vs
-               $ introducing (zip vs $ coerce as)
+      let jdg' = introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
-      sg <- newSubgoal jdg'
+      sg <- newSubgoal
+          $ bool
+              id
+              (withPositionMapping
+                (extremelyStupid__definingFunction ctx) vs)
+              (isTopHole jdg)
+          $ jdg'
       pure
         . noLoc
         . lambda (fmap bvar' vs)

From 3272a1ea651db264120f7be10ffe0742c3185358 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 9 Oct 2020 14:50:01 -0700
Subject: [PATCH 32/50] Fix improperly pruning split of split

---
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs   | 18 ++++++++++++------
 1 file changed, 12 insertions(+), 6 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 2fd8aef1e4..4b20cdfb01 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -203,12 +203,18 @@ splitAuto = do
     Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
-      case isSplitWhitelisted jdg of
-        True -> choice $ fmap splitDataCon dcs
-        False -> choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-          case any ((/= jGoal jdg)  . jGoal) jdgs of
-            True  -> Nothing
-            False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+      -- TODO(sandy): Figure out the right strategy for pruning splits of
+      -- splits
+      choice $ fmap splitDataCon dcs
+      -- case isSplitWhitelisted jdg of
+      --   True -> choice $ fmap splitDataCon dcs
+      --   False -> do
+      --     choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+      --       case all ((== jGoal jdg)  . jGoal) jdgs of
+      --         False  -> Nothing
+      --         True -> do
+      --           traceMX "unhelpful split" $ nameOccName $ dataConName dc
+      --           Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From 30c9b580093433bfdc9a2ec671decdc5309de2d2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 00:36:26 -0700
Subject: [PATCH 33/50] Tracing

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs      |  6 +--
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs |  3 +-
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 27 +++++++----
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 20 ++++++++-
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  | 45 +++++++++++--------
 .../tactics/src/Ide/Plugin/Tactic/Types.hs    | 36 ++++++++++++---
 6 files changed, 98 insertions(+), 39 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 1dbccedfa0..27171fe7fd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -258,7 +258,6 @@ judgementForHole state nfp range = do
 
   resulting_range <- liftMaybe $ toCurrentRange amapping $ realSrcSpanToRange rss
   (tcmod, _) <- MaybeT $ runIde state $ useWithStale TypeCheck nfp
-  -- traceMX "holes!" $ isRhsHole rss $
   let tcg = fst $ tm_internals_ $ tmrModule tcmod
       tcs = tm_typechecked_source $ tmrModule tcmod
       ctx = mkContext
@@ -297,9 +296,10 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right res -> do
-              let g = graft (RealSrcSpan span) res
+            Right (tr, ext) -> do
+              let g = graft (RealSrcSpan span) ext
                   response = transform dflags (clientCapabilities lf) uri g pm
+              traceMX "trace" tr
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
                 Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 4aadd75ee2..392bcf3c80 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -3,6 +3,7 @@ module Ide.Plugin.Tactic.Auto where
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Machinery
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import Refinery.Tactic
@@ -11,7 +12,7 @@ import Refinery.Tactic
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
-auto = do
+auto = tracing "auto" $ do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 191b4e7c3b..7bae665f54 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE FlexibleContexts #-}
 module Ide.Plugin.Tactic.CodeGen where
 
@@ -38,7 +39,7 @@ destructMatches
     -> CType
        -- ^ Type being destructed
     -> Judgement
-    -> RuleM [RawMatch]
+    -> RuleM (Trace, [RawMatch])
 destructMatches f f2 t jdg = do
   let hy = jHypothesis jdg
       g  = jGoal jdg
@@ -48,7 +49,7 @@ destructMatches f f2 t jdg = do
       let dcs = tyConDataCons tc
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
-        _ -> for dcs $ \dc -> do
+        _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstArgTys dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
@@ -61,9 +62,15 @@ destructMatches f f2 t jdg = do
                 $ withPositionMapping dcon_name names
                 $ introducingPat hy'
                 $ withNewGoal g jdg
-          sg <- f dc j
+          (tr, sg) <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
-          pure $ match [pat] $ unLoc sg
+          pure $ (tr, match [pat] $ unLoc sg)
+
+
+unzipTrace :: [(Trace, a)] -> (Trace, [a])
+unzipTrace l =
+  let (trs, as) = unzip l
+   in (rose mempty trs, as)
 
 
 ------------------------------------------------------------------------------
@@ -77,7 +84,7 @@ destruct' f term jdg = do
     Nothing -> throwError $ UndefinedHypothesis term
     Just (_, t) -> do
       useOccName jdg term
-      fmap noLoc $ case' (var' term) <$>
+      fmap (fmap noLoc $ case' (var' term)) <$>
         destructMatches
           f
           (\cs -> setParents term (fmap fst cs) . destructing term)
@@ -94,7 +101,7 @@ destructLambdaCase' f jdg = do
   let g  = jGoal jdg
   case splitFunTy_maybe (unCType g) of
     Just (arg, _) | isAlgType arg ->
-      fmap noLoc $ lambdaCase <$>
+      fmap (fmap noLoc $ lambdaCase) <$>
         destructMatches f (const id) (CType arg) jdg
     _ -> throwError $ GoalMismatch "destructLambdaCase'" g
 
@@ -105,11 +112,13 @@ buildDataCon
     :: Judgement
     -> DataCon            -- ^ The data con to build
     -> [Type]             -- ^ Type arguments for the data con
-    -> RuleM (LHsExpr GhcPs)
+    -> RuleM (Trace, LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
   let args = dataConInstArgTys dc apps
       dcon_name = nameOccName $ dataConName dc
-  sgs <- traverse ( \(arg, n) ->
+  (tr, sgs)
+      <- fmap unzipTrace
+       $ traverse ( \(arg, n) ->
                     newSubgoal
                   . filterSameTypeFromOtherPositions dcon_name n
                   . blacklistingDestruct
@@ -117,6 +126,7 @@ buildDataCon jdg dc apps = do
                   $ CType arg
                   ) $ zip args [0..]
   pure
+    . (tr,)
     . noLoc
     . foldl' (@@)
         (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
@@ -128,6 +138,7 @@ buildDataCon jdg dc apps = do
 var' :: Var a => OccName -> a
 var' = var . fromString . occNameString
 
+
 ------------------------------------------------------------------------------
 -- | Like 'bvar', but works over standard GHC 'OccName's.
 bvar' :: BVar a => OccName -> a
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 8228feee00..588445ebb7 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -36,6 +36,8 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
+import Control.Arrow
+import Control.Monad.State.Strict (StateT (..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -47,7 +49,7 @@ substCTy subst = coerce . substTy subst . coerce
 -- goal.
 newSubgoal
     :: Judgement
-    -> RuleM (LHsExpr GhcPs)
+    -> Rule
 newSubgoal j = do
     unifier <- gets ts_unifier
     subgoal
@@ -62,7 +64,7 @@ runTactic
     :: Context
     -> Judgement
     -> TacticsM ()       -- ^ Tactic to use
-    -> Either [TacticError] (LHsExpr GhcPs)
+    -> Either [TacticError] (Trace, LHsExpr GhcPs)
 runTactic ctx jdg t =
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
         tacticState = defaultTacticState { ts_skolems = skolems }
@@ -81,6 +83,20 @@ runTactic ctx jdg t =
           _ -> Left []
 
 
+tracePrim :: String -> Trace
+tracePrim = flip rose []
+
+
+tracing
+    :: Functor m
+    => String
+    -> TacticT jdg (Trace, ext) err s m a
+    -> TacticT jdg (Trace, ext) err s m a
+tracing s (TacticT m)
+  = TacticT $ StateT $ \jdg ->
+      mapExtract' (first $ rose s . pure) $ runStateT m jdg
+
+
 recursiveCleanup
     :: TacticState
     -> Maybe TacticError
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 4b20cdfb01..7b4dd2855f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DeriveGeneric         #-}
@@ -17,6 +18,7 @@ import           Control.Monad.Except (throwError)
 import           Control.Monad.Reader.Class (MonadReader(ask))
 import           Control.Monad.State.Class
 import           Control.Monad.State.Strict (StateT(..), runStateT)
+import           Data.Bool (bool)
 import           Data.List
 import qualified Data.Map as M
 import           Data.Maybe
@@ -33,12 +35,11 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (nameOccName)
+import           Name (occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
 import           Type hiding (Var)
-import Data.Bool (bool)
 
 
 ------------------------------------------------------------------------------
@@ -60,14 +61,14 @@ assume name = rule $ \jdg -> do
             True  -> setRecursionFrameData True
             False -> pure ()
           useOccName jdg name
-          pure $ noLoc $ var' name
+          pure $ (tracePrim $ "assume:" <> occNameString name, ) $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
 
 
 recursion :: TacticsM ()
-recursion = do
+recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
@@ -79,7 +80,7 @@ recursion = do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = rule $ \jdg -> do
+intros = tracing "intros" $ rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
   ctx <- ask
@@ -90,7 +91,8 @@ intros = rule $ \jdg -> do
       let jdg' = introducing (zip vs $ coerce as)
                $ withNewGoal (CType b) jdg
       modify $ withIntroducedVals $ mappend $ S.fromList vs
-      sg <- newSubgoal
+      (tr, sg)
+        <- newSubgoal
           $ bool
               id
               (withPositionMapping
@@ -98,6 +100,7 @@ intros = rule $ \jdg -> do
               (isTopHole jdg)
           $ jdg'
       pure
+        . (tr, )
         . noLoc
         . lambda (fmap bvar' vs)
         $ unLoc sg
@@ -106,7 +109,7 @@ intros = rule $ \jdg -> do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destructAuto :: OccName -> TacticsM ()
-destructAuto name = do
+destructAuto name = tracing "destruct(auto)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -126,7 +129,7 @@ destructAuto name = do
 ------------------------------------------------------------------------------
 -- | Case split, and leave holes in the matches.
 destruct :: OccName -> TacticsM ()
-destruct name = do
+destruct name = tracing "destruct(user)" $ do
   jdg <- goal
   case hasDestructed jdg name of
     True -> throwError $ AlreadyDestructed name
@@ -136,20 +139,20 @@ destruct name = do
 ------------------------------------------------------------------------------
 -- | Case split, using the same data constructor in the matches.
 homo :: OccName -> TacticsM ()
-homo = rule . destruct' (\dc jdg ->
+homo = tracing "homo" . rule . destruct' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
 ------------------------------------------------------------------------------
 -- | LambdaCase split, and leave holes in the matches.
 destructLambdaCase :: TacticsM ()
-destructLambdaCase = rule $ destructLambdaCase' (const subgoal)
+destructLambdaCase = tracing "destructLambdaCase" $ rule $ destructLambdaCase' (const subgoal)
 
 
 ------------------------------------------------------------------------------
 -- | LambdaCase split, using the same data constructor in the matches.
 homoLambdaCase :: TacticsM ()
-homoLambdaCase = rule $ destructLambdaCase' (\dc jdg ->
+homoLambdaCase = tracing "homoLambdaCase" $ rule $ destructLambdaCase' (\dc jdg ->
   buildDataCon jdg dc $ snd $ splitAppTys $ unCType $ jGoal jdg)
 
 
@@ -158,7 +161,7 @@ apply = apply' (const id)
 
 
 apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
-apply' f func = do
+apply' f func = tracing ("apply':" <> show func) $ do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg
@@ -167,16 +170,20 @@ apply' f func = do
           let (args, ret) = splitFunTys ty
           unify g (CType ret)
           useOccName jdg func
-          sgs <- traverse ( \(i, t) ->
+          (tr, sgs)
+              <- fmap unzipTrace
+               $ traverse ( \(i, t) ->
                             newSubgoal
                           . f i
                           . blacklistingDestruct
                           . flip withNewGoal jdg
                           $ CType t
                           ) $ zip [0..] args
-          pure . noLoc
-              . foldl' (@@) (var' func)
-              $ fmap unLoc sgs
+          pure
+            . (tr, )
+            . noLoc
+            . foldl' (@@) (var' func)
+            $ fmap unLoc sgs
       Nothing -> do
         throwError $ GoalMismatch "apply" g
 
@@ -184,7 +191,7 @@ apply' f func = do
 ------------------------------------------------------------------------------
 -- | Choose between each of the goal's data constructors.
 split :: TacticsM ()
-split = do
+split = tracing "split(user)" $ do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
@@ -196,7 +203,7 @@ split = do
 ------------------------------------------------------------------------------
 -- | Choose between each of the goal's data constructors.
 splitAuto :: TacticsM ()
-splitAuto = do
+splitAuto = tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
@@ -220,7 +227,7 @@ splitAuto = do
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
 splitDataCon :: DataCon -> TacticsM ()
-splitDataCon dc = rule $ \jdg -> do
+splitDataCon dc = tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
   let g = jGoal jdg
   case splitTyConApp_maybe $ unCType g of
     Just (tc, apps) -> do
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index cca6fe8247..7cce195acc 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -26,13 +26,15 @@ import Control.Monad.Reader
 import Data.Function
 import Data.Map (Map)
 import Data.Set (Set)
-import Development.IDE.GHC.Compat
+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 Type
+import Data.Tree
+import Data.Coerce
 
 
 ------------------------------------------------------------------------------
@@ -60,6 +62,9 @@ instance Show TCvSubst where
 instance Show (LHsExpr GhcPs) where
   show  = unsafeRender
 
+instance Show DataCon where
+  show  = unsafeRender
+
 
 ------------------------------------------------------------------------------
 data TacticState = TacticState
@@ -118,8 +123,8 @@ newtype ExtractM a = ExtractM { unExtractM :: Reader Context a }
 
 ------------------------------------------------------------------------------
 -- | Orphan instance for producing holes when attempting to solve tactics.
-instance MonadExtract (LHsExpr GhcPs) ExtractM where
-  hole = pure $ noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_"
+instance MonadExtract (Trace, LHsExpr GhcPs) ExtractM where
+  hole = pure (mempty, noLoc $ HsVar noExtField $ noLoc $ Unqual $ mkVarOcc "_")
 
 
 ------------------------------------------------------------------------------
@@ -175,9 +180,11 @@ instance Show TacticError where
 
 
 ------------------------------------------------------------------------------
-type TacticsM  = TacticT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
-type RuleM     = RuleT Judgement (LHsExpr GhcPs) TacticError TacticState ExtractM
-type Rule      = RuleM (LHsExpr GhcPs)
+type TacticsM  = TacticT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
+type RuleM     = RuleT Judgement (Trace, LHsExpr GhcPs) TacticError TacticState ExtractM
+type Rule      = RuleM (Trace, LHsExpr GhcPs)
+
+type Trace = Rose String
 
 
 ------------------------------------------------------------------------------
@@ -190,3 +197,20 @@ data Context = Context
   }
   deriving stock (Eq, Ord)
 
+
+newtype Rose a = Rose (Tree a)
+  deriving stock (Eq, Functor, Generic)
+
+instance Show (Rose String) where
+  show = drawTree . coerce
+
+instance Semigroup a => Semigroup (Rose a) where
+  Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)
+
+instance Monoid a => Monoid (Rose a) where
+  mempty = Rose $ Node mempty mempty
+
+rose :: (Eq a, Monoid a) => a -> [Rose a] -> Rose a
+rose a [Rose (Node a' rs)] | a' == mempty = Rose $ Node a rs
+rose a rs = Rose $ Node a $ coerce rs
+

From 6b8a0b9f464458e203c23071bee89fb63b739936 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 00:53:49 -0700
Subject: [PATCH 34/50] unpack introduced bindings

---
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  | 23 ++++++++++++-------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  4 ++--
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index 7bae665f54..85373a9f61 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -64,7 +64,11 @@ destructMatches f f2 t jdg = do
                 $ withNewGoal g jdg
           (tr, sg) <- f dc j
           modify $ withIntroducedVals $ mappend $ S.fromList names
-          pure $ (tr, match [pat] $ unLoc sg)
+          pure ( rose ("match " <> show dc <> " {" <>
+                          intercalate ", " (fmap show names) <> "}")
+                    $ pure tr
+               , match [pat] $ unLoc sg
+               )
 
 
 unzipTrace :: [(Trace, a)] -> (Trace, [a])
@@ -84,12 +88,15 @@ destruct' f term jdg = do
     Nothing -> throwError $ UndefinedHypothesis term
     Just (_, t) -> do
       useOccName jdg term
-      fmap (fmap noLoc $ case' (var' term)) <$>
-        destructMatches
-          f
-          (\cs -> setParents term (fmap fst cs) . destructing term)
-          t
-          jdg
+      (tr, ms)
+          <- destructMatches
+               f
+               (\cs -> setParents term (fmap fst cs) . destructing term)
+               t
+               jdg
+      pure ( rose ("destruct " <> show term) $ pure tr
+           , noLoc $ case' (var' term) ms
+           )
 
 
 ------------------------------------------------------------------------------
@@ -126,7 +133,7 @@ buildDataCon jdg dc apps = do
                   $ CType arg
                   ) $ zip args [0..]
   pure
-    . (tr,)
+    . (rose (show dc) $ pure tr,)
     . noLoc
     . foldl' (@@)
         (HsVar noExtField $ noLoc $ Unqual $ nameOccName $ dataConName dc)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 7b4dd2855f..0a39a47aae 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -80,7 +80,7 @@ recursion = tracing "recursion" $ do
 ------------------------------------------------------------------------------
 -- | Introduce a lambda binding every variable.
 intros :: TacticsM ()
-intros = tracing "intros" $ rule $ \jdg -> do
+intros = rule $ \jdg -> do
   let hy = jHypothesis jdg
       g  = jGoal jdg
   ctx <- ask
@@ -100,7 +100,7 @@ intros = tracing "intros" $ rule $ \jdg -> do
               (isTopHole jdg)
           $ jdg'
       pure
-        . (tr, )
+        . (rose ("intros {" <> intercalate ", " (fmap show vs) <> "}") $ pure tr, )
         . noLoc
         . lambda (fmap bvar' vs)
         $ unLoc sg

From 872cfec1c5097ce6c49282872f9f8725cee67128 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 01:07:32 -0700
Subject: [PATCH 35/50] Slightly better format

---
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs        | 12 +++++++-----
 .../tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs |  6 +++---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs     |  4 ++--
 3 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 392bcf3c80..3e4a28d21f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -3,20 +3,22 @@ module Ide.Plugin.Tactic.Auto where
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
-import Ide.Plugin.Tactic.Machinery
 import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import Refinery.Tactic
+import Ide.Plugin.Tactic.Machinery (tracing)
 
 
 ------------------------------------------------------------------------------
 -- | Automatically solve a goal.
 auto :: TacticsM ()
-auto = tracing "auto" $ do
+auto = do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
-  commit
-    knownStrategies
-    (localTactic (auto' 4) $ disallowing $ fmap fst current)
+  commit knownStrategies
+    . tracing "auto"
+    . localTactic (auto' 4)
+    . disallowing
+    $ fmap fst current
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
index 0855cd97e8..610740aba3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/KnownStrategies.hs
@@ -8,6 +8,7 @@ import Ide.Plugin.Tactic.Tactics
 import Ide.Plugin.Tactic.Types
 import OccName (mkVarOcc)
 import Refinery.Tactic
+import Ide.Plugin.Tactic.Machinery (tracing)
 
 
 knownStrategies :: TacticsM ()
@@ -19,9 +20,8 @@ knownStrategies = choice
 known :: String -> TacticsM () -> TacticsM ()
 known name t = do
   getCurrentDefinitions >>= \case
-    [(def, _)] | def == mkVarOcc name -> do
-      traceMX "running known strategy" name
-      t
+    [(def, _)] | def == mkVarOcc name ->
+      tracing ("known " <> name) t
     _ -> throwError NoApplicableTactic
 
 
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 0a39a47aae..dc6358fec8 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -61,7 +61,7 @@ assume name = rule $ \jdg -> do
             True  -> setRecursionFrameData True
             False -> pure ()
           useOccName jdg name
-          pure $ (tracePrim $ "assume:" <> occNameString name, ) $ noLoc $ var' name
+          pure $ (tracePrim $ "assume " <> occNameString name, ) $ noLoc $ var' name
         False -> throwError $ GoalMismatch "assume" g
     Nothing -> throwError $ UndefinedHypothesis name
 
@@ -161,7 +161,7 @@ apply = apply' (const id)
 
 
 apply' :: (Int -> Judgement -> Judgement) -> OccName -> TacticsM ()
-apply' f func = tracing ("apply':" <> show func) $ do
+apply' f func = tracing ("apply' " <> show func) $ do
   rule $ \jdg -> do
     let hy = jHypothesis jdg
         g  = jGoal jdg

From 8a416d978ebc777f030acd2d933109a817849545 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 11 Oct 2020 01:13:58 -0700
Subject: [PATCH 36/50] compress ppr tree

---
 plugins/tactics/src/Ide/Plugin/Tactic/Types.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
index 7cce195acc..5cfd62b5a6 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Types.hs
@@ -202,7 +202,12 @@ newtype Rose a = Rose (Tree a)
   deriving stock (Eq, Functor, Generic)
 
 instance Show (Rose String) where
-  show = drawTree . coerce
+  show = unlines . dropEveryOther . lines . drawTree . coerce
+
+dropEveryOther :: [a] -> [a]
+dropEveryOther []           = []
+dropEveryOther [a]          = [a]
+dropEveryOther (a : _ : as) = a : dropEveryOther as
 
 instance Semigroup a => Semigroup (Rose a) where
   Rose (Node a as) <> Rose (Node b bs) = Rose $ Node (a <> b) (as <> bs)

From 8e690047025ec05e92c69a3536cba9669f3e18e2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 00:42:03 -0700
Subject: [PATCH 37/50] Fix splitAuto

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

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index dc6358fec8..0703fa2a94 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -35,7 +35,7 @@ import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Machinery
 import           Ide.Plugin.Tactic.Naming
 import           Ide.Plugin.Tactic.Types
-import           Name (occNameString)
+import           Name (nameOccName, occNameString)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -200,8 +200,11 @@ split = tracing "split(user)" $ do
       let dcs = tyConDataCons tc
       choice $ fmap splitDataCon dcs
 
+
 ------------------------------------------------------------------------------
--- | Choose between each of the goal's data constructors.
+-- | Choose between each of the goal's data constructors. Different than
+-- '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
   jdg <- goal
@@ -210,18 +213,15 @@ splitAuto = tracing "split(auto)" $ do
     Nothing -> throwError $ GoalMismatch "split" g
     Just (tc, _) -> do
       let dcs = tyConDataCons tc
-      -- TODO(sandy): Figure out the right strategy for pruning splits of
-      -- splits
-      choice $ fmap splitDataCon dcs
-      -- case isSplitWhitelisted jdg of
-      --   True -> choice $ fmap splitDataCon dcs
-      --   False -> do
-      --     choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-      --       case all ((== jGoal jdg)  . jGoal) jdgs of
-      --         False  -> Nothing
-      --         True -> do
-      --           traceMX "unhelpful split" $ nameOccName $ dataConName dc
-      --           Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+      case isSplitWhitelisted jdg of
+        True -> choice $ fmap splitDataCon dcs
+        False -> do
+          choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
+            case any (/= jGoal jdg) $ traceIdX "goals" $ fmap jGoal jdgs of
+              False  -> Nothing
+              True -> do
+                traceMX "unhelpful split" $ nameOccName $ dataConName dc
+                Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From a84195c1db03a9f024ca08d3aaa79368c097e413 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 11:39:51 -0700
Subject: [PATCH 38/50] Cleanup traces

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs           | 3 +--
 plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs      | 1 +
 plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs | 7 ++++++-
 plugins/tactics/src/Ide/TreeTransform.hs           | 3 +--
 4 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index 27171fe7fd..c7ebd3cad3 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -296,10 +296,9 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right (tr, ext) -> do
+            Right (_, ext) -> do
               let g = graft (RealSrcSpan span) ext
                   response = transform dflags (clientCapabilities lf) uri g pm
-              traceMX "trace" tr
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))
                 Left err -> (Left $ ResponseError InternalError (T.pack err) Nothing, Nothing)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
index 3e4a28d21f..0a22255e60 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs
@@ -16,6 +16,7 @@ auto = do
   jdg <- goal
   current <- getCurrentDefinitions
   traceMX "goal" jdg
+  traceMX "ctx" current
   commit knownStrategies
     . tracing "auto"
     . localTactic (auto' 4)
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 588445ebb7..7a02fa1d66 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -76,7 +76,12 @@ runTactic ctx jdg t =
       (_, solns) -> do
         let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         -- TODO(sandy): remove this trace sometime
-        traceM $ mappend "!!!solns: " $ intercalate "\n" $ take 50 $  fmap (show . fst) sorted
+        traceM
+            $ mappend "!!!solns: "
+            $ intercalate "\n"
+            $ reverse
+            $ take 5
+            $ fmap (show . fst) sorted
         case sorted of
           (res : _) -> Right $ fst res
           -- guaranteed to not be empty
diff --git a/plugins/tactics/src/Ide/TreeTransform.hs b/plugins/tactics/src/Ide/TreeTransform.hs
index 012426de68..80b0062ff5 100644
--- a/plugins/tactics/src/Ide/TreeTransform.hs
+++ b/plugins/tactics/src/Ide/TreeTransform.hs
@@ -12,7 +12,6 @@ import           BasicTypes (appPrec)
 import           Control.Monad
 import           Control.Monad.Trans.Class
 import qualified Data.Text as T
-import           Debug.Trace
 import           Development.IDE.Core.RuleTypes
 import           Development.IDE.Core.Rules
 import           Development.IDE.Core.Shake
@@ -104,7 +103,7 @@ fixAnns ParsedModule {..} =
 annotate :: DynFlags -> LHsExpr GhcPs -> TransformT (Either String) (Anns, LHsExpr GhcPs)
 annotate dflags expr = do
   uniq <- show <$> uniqueSrcSpanT
-  let rendered = traceId $ render dflags expr
+  let rendered = render dflags expr
   (anns, expr') <- lift $ either (Left . show) Right $ parseExpr dflags uniq rendered
   let anns' = setPrecedingLines expr' 0 1 anns
   pure (anns', expr')

From 5f44746777e7f708c46b7c0d65332a3effd794ad Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Tue, 13 Oct 2020 11:40:30 -0700
Subject: [PATCH 39/50] Fix autosplit

---
 plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 0703fa2a94..364eb6718f 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -217,11 +217,9 @@ splitAuto = tracing "split(auto)" $ do
         True -> choice $ fmap splitDataCon dcs
         False -> do
           choice $ flip fmap dcs $ \dc -> pruning (splitDataCon dc) $ \jdgs ->
-            case any (/= jGoal jdg) $ traceIdX "goals" $ fmap jGoal jdgs of
-              False  -> Nothing
-              True -> do
-                traceMX "unhelpful split" $ nameOccName $ dataConName dc
-                Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+            case any (/= jGoal jdg) $ fmap jGoal jdgs of
+              False -> Nothing
+              True  -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

From 4eca10df5a3f5a8904ce5509e8e67d3f5809c8ba Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Thu, 15 Oct 2020 20:44:19 -0700
Subject: [PATCH 40/50] Update refinery

---
 cabal.project                                 |  2 +-
 haskell-language-server.cabal                 |  2 +-
 .../tactics/src/Ide/Plugin/Tactic/CodeGen.hs  |  9 +-
 .../src/Ide/Plugin/Tactic/Machinery.hs        | 84 ++-----------------
 .../tactics/src/Ide/Plugin/Tactic/Tactics.hs  |  2 +-
 stack-8.10.1.yaml                             |  2 +-
 stack-8.10.2.yaml                             |  2 +-
 stack-8.6.4.yaml                              |  2 +-
 stack-8.6.5.yaml                              |  2 +-
 stack-8.8.2.yaml                              |  2 +-
 stack-8.8.3.yaml                              |  2 +-
 stack-8.8.4.yaml                              |  2 +-
 stack.yaml                                    |  2 +-
 13 files changed, 21 insertions(+), 94 deletions(-)

diff --git a/cabal.project b/cabal.project
index 334c3417f5..6323590cf8 100644
--- a/cabal.project
+++ b/cabal.project
@@ -20,6 +20,6 @@ package ghcide
 
 write-ghc-environment-files: never
 
-index-state: 2020-10-08T12:51:21Z
+index-state: 2020-10-16T04:00:00Z
 
 allow-newer: data-tree-print:base
diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index e2d3f2fd72..4f75fad4c6 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -158,7 +158,7 @@ executable haskell-language-server
     , transformers
     , unordered-containers
     , ghc-source-gen
-    , refinery                 ^>=0.2
+    , refinery                 ^>=0.3
     , ghc-exactprint
     , fingertree
     , generic-lens
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
index f755b79a24..f89a9964dd 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/CodeGen.hs
@@ -49,7 +49,7 @@ destructMatches f f2 t jdg = do
       let dcs = tyConDataCons tc
       case dcs of
         [] -> throwError $ GoalMismatch "destruct" g
-        _ -> for dcs $ \dc -> do
+        _ -> fmap unzipTrace $ for dcs $ \dc -> do
           let args = dataConInstOrigArgTys' dc apps
           names <- mkManyGoodNames hy args
           let hy' = zip names $ coerce args
@@ -131,8 +131,7 @@ buildDataCon
     -> [Type]             -- ^ Type arguments for the data con
     -> RuleM (Trace, LHsExpr GhcPs)
 buildDataCon jdg dc apps = do
-<<<<<<< HEAD
-  let args = dataConInstArgTys dc apps
+  let args = dataConInstOrigArgTys' dc apps
       dcon_name = nameOccName $ dataConName dc
   (tr, sgs)
       <- fmap unzipTrace
@@ -143,10 +142,6 @@ buildDataCon jdg dc apps = do
                   . flip withNewGoal jdg
                   $ CType arg
                   ) $ zip args [0..]
-=======
-  let args = dataConInstOrigArgTys' dc apps
-  sgs <- traverse (newSubgoal . flip withNewGoal jdg . CType) args
->>>>>>> master
   pure
     . (rose (show dc) $ pure tr,)
     . noLoc
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
index 7a02fa1d66..972cb8a574 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs
@@ -17,11 +17,12 @@ module Ide.Plugin.Tactic.Machinery
   ( module Ide.Plugin.Tactic.Machinery
   ) where
 
-import           Control.Applicative
+import           Control.Arrow
 import           Control.Monad.Error.Class
 import           Control.Monad.Reader
 import           Control.Monad.State (MonadState(..))
 import           Control.Monad.State.Class (gets, modify)
+import           Control.Monad.State.Strict (StateT (..))
 import           Data.Coerce
 import           Data.Either
 import           Data.List (intercalate, sortBy)
@@ -36,8 +37,6 @@ import           Refinery.Tactic.Internal
 import           TcType
 import           Type
 import           Unify
-import Control.Arrow
-import Control.Monad.State.Strict (StateT (..))
 
 
 substCTy :: TCvSubst -> CType -> CType
@@ -71,10 +70,10 @@ runTactic ctx jdg t =
     in case partitionEithers
           . flip runReader ctx
           . unExtractM
-          $ runTacticTWithState t jdg tacticState of
+          $ runTacticT t jdg tacticState of
       (errs, []) -> Left $ take 50 $ errs
-      (_, solns) -> do
-        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
+      (_, fmap assoc23 -> solns) -> do
+        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) $ solns
         -- TODO(sandy): remove this trace sometime
         traceM
             $ mappend "!!!solns: "
@@ -87,6 +86,9 @@ runTactic ctx jdg t =
           -- guaranteed to not be empty
           _ -> Left []
 
+assoc23 :: (a, b, c) -> (a, (b, c))
+assoc23 (a, b, c) = (a, (b, c))
+
 
 tracePrim :: String -> Trace
 tracePrim = flip rose []
@@ -112,44 +114,6 @@ recursiveCleanup s =
         False -> Just NoProgress
 
 
-filterT
-    :: (Monad m)
-    => (s -> Maybe err)
-    -> (s -> s)
-    -> TacticT jdg ext err s m ()
-    -> TacticT jdg ext err s m ()
-filterT p f t = check >> t
-    where
-      check = rule $ \j -> do
-          e <- subgoal j
-          s <- get
-          modify f
-          case p s of
-            Just err -> throwError err
-            Nothing -> pure e
-
-
-gather
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m a
-    -> ([(a, jdg)] -> TacticT jdg ext err s m a)
-    -> TacticT jdg ext err s m a
-gather t f = tactic $ \j -> do
-    s <- get
-    results <- lift $ proofs s $ proofState t j
-    msum $ flip fmap results $ \case
-        Left err -> throwError err
-        Right (_, jdgs) -> proofState (f jdgs) j
-
-
-pruning
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m ()
-    -> ([jdg] -> Maybe err)
-    -> TacticT jdg ext err s m ()
-pruning t p = gather t $ maybe t throwError . p . fmap snd
-
-
 setRecursionFrameData :: MonadState TacticState m => Bool -> m ()
 setRecursionFrameData b = do
   modify $ withRecursionStack $ \case
@@ -180,38 +144,6 @@ newtype Reward a = Reward a
   deriving (Eq, Ord, Show) via a
 
 
-runTacticTWithState
-    :: (MonadExtract ext m)
-    => TacticT jdg ext err s m ()
-    -> jdg
-    -> s
-    -> m [Either err (ext, (s, [jdg]))]
-runTacticTWithState t j s = proofs' s $ fmap snd $ proofState t j
-
-
-proofs'
-    :: (MonadExtract ext m)
-    => s
-    -> ProofStateT ext ext err s m goal
-    -> m [(Either err (ext, (s, [goal])))]
-proofs' s p = go s [] p
-    where
-      go s goals (Subgoal goal k) = do
-         h <- hole
-         (go s (goals ++ [goal]) $ k h)
-      go s goals (Effect m) = go s goals =<< m
-      go s goals (Stateful f) =
-          let (s', p) = f s
-          in go s' goals p
-      go s goals (Alt p1 p2) = liftA2 (<>) (go s goals p1) (go s goals p2)
-      go s goals (Interleave p1 p2) = liftA2 (interleave) (go s goals p1) (go s goals p2)
-      go s goals (Commit p1 p2) = go s goals p1 >>= \case
-          (rights -> []) -> go s goals p2
-          solns -> pure solns
-      go _ _ Empty = pure []
-      go _ _ (Failure err) = pure [throwError err]
-      go s goals (Axiom ext) = pure [Right (ext, (s, goals))]
-
 
 ------------------------------------------------------------------------------
 -- | We need to make sure that we don't try to unify any skolems.
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
index 364eb6718f..4fcccbb61b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs
@@ -72,7 +72,7 @@ recursion = tracing "recursion" $ do
   defs <- getCurrentDefinitions
   attemptOn (const $ fmap fst defs) $ \name -> do
     modify $ withRecursionStack (False :)
-    filterT recursiveCleanup (withRecursionStack tail) $ do
+    ensure recursiveCleanup (withRecursionStack tail) $ do
       (localTactic (apply' (const id) name) $ introducing defs)
         <@> fmap (localTactic assumption . filterPosition name) [0..]
 
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index e462e45fca..8353abf148 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -21,7 +21,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.12.2.0
 - semigroups-0.18.5
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index a594da29c8..66fa833fb6 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -19,7 +19,7 @@ extra-deps:
 - fourmolu-0.2.0.0
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - stylish-haskell-0.12.2.0
 - semigroups-0.18.5
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index 97051012b9..9796b068ef 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -46,7 +46,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 888670dd8f..1a0b67c2b2 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index 0d6a229d1f..94ad80cd99 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -38,7 +38,7 @@ extra-deps:
 - monad-dijkstra-0.1.1.2
 - opentelemetry-0.4.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index 1468ae7444..c01a2649e1 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -30,7 +30,7 @@ extra-deps:
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
 - ormolu-0.1.3.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index ebf11425f1..57518e9e24 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -30,7 +30,7 @@ extra-deps:
 - ilist-0.3.1.0
 - lsp-test-0.11.0.5
 - monad-dijkstra-0.1.1.2
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - retrie-0.1.1.1
 - semigroups-0.18.5
 # - github: wz1000/shake
diff --git a/stack.yaml b/stack.yaml
index 888670dd8f..1a0b67c2b2 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -45,7 +45,7 @@ extra-deps:
 - ormolu-0.1.3.0
 - parser-combinators-1.2.1
 - primitive-0.7.1.0
-- refinery-0.2.0.0
+- refinery-0.3.0.0
 - regex-base-0.94.0.0
 - regex-pcre-builtin-0.95.1.1.8.43
 - regex-tdfa-1.3.1.0

From de0cfb912eef276b9de4702226bf2e8f3c2e51e8 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:21:05 -0700
Subject: [PATCH 41/50] Attempt GHC compatability

---
 plugins/tactics/src/Ide/Plugin/Tactic.hs     | 23 -----------
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 41 +++++++++++++++++++-
 2 files changed, 39 insertions(+), 25 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic.hs b/plugins/tactics/src/Ide/Plugin/Tactic.hs
index c7ebd3cad3..82b91d942b 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic.hs
@@ -345,31 +345,8 @@ getRhsPosVals rss tcs = getFirst $ everything (<>) (mkQ mempty $ \case
   ) tcs
 
 
-------------------------------------------------------------------------------
--- | Should make sure it's a fun bind
-pattern TopLevelRHS :: OccName -> [Pat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
-pattern TopLevelRHS name ps body <-
-  Match _
-    (FunRhs (L _ (occName -> name)) _ _)
-    ps
-    (GRHSs _
-      [L _ (GRHS _ [] body)] _)
-
 
 -- TODO(sandy): Make this more robust
 isHole :: OccName -> Bool
 isHole = isPrefixOf "_" . occNameString
 
-
-getPatName :: Pat GhcTc -> Maybe OccName
-getPatName = \case
-   VarPat _ x    -> Just $ occName $ unLoc x
-   LazyPat _ p   -> getPatName p
-   AsPat _ x _   -> Just $ occName $ unLoc x
-   ParPat _ p    -> getPatName p
-   BangPat _ p   -> getPatName p
-   ViewPat _ _ p -> getPatName p
-   SigPat _ p _  -> getPatName p
-   XPat p        -> getPatName $ unLoc p
-   _             -> Nothing
-
diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 9d1c34851b..8e1fa57a0a 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -1,11 +1,14 @@
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE CPP             #-}
+{-# 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 TyCon
 import Type
 import TysWiredIn (intTyCon, floatTyCon, doubleTyCon, charTyCon)
 import Unique
@@ -67,3 +70,37 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
 
+fromPatCompat :: PatCompat pass -> Pat pass
+#if __GLASGOW_HASKELL__ <= 808
+type PatCompat = Pat
+fromPatCompat = id
+#elif
+type PatCompat = LPat
+fromPatCompat = unLoc
+#endif
+
+------------------------------------------------------------------------------
+-- | Should make sure it's a fun bind
+pattern TopLevelRHS :: OccName -> [PatCompat GhcTc] -> LHsExpr GhcTc -> Match GhcTc (LHsExpr GhcTc)
+pattern TopLevelRHS name ps body <-
+  Match _
+    (FunRhs (L _ (occName -> name)) _ _)
+    ps
+    (GRHSs _
+      [L _ (GRHS _ [] body)] _)
+
+getPatName :: PatCompat GhcTc -> Maybe OccName
+getPatName (fromPatCompat -> p0) =
+  case p0 of
+    VarPat  _ x   -> Just $ occName $ unLoc x
+    LazyPat _ p   -> getPatName p
+    AsPat   _ x _ -> Just $ occName $ unLoc x
+    ParPat  _ p   -> getPatName p
+    BangPat _ p   -> getPatName p
+    ViewPat _ _ p -> getPatName p
+#if __GLASGOW_HASKELL__ >= 808
+    SigPat  _ p _ -> getPatName p
+#endif
+    XPat    p     -> getPatName $ unLoc p
+    _             -> Nothing
+

From 1b70cee68fd42059a138b791777c9d61729277e6 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:43:29 -0700
Subject: [PATCH 42/50] cpp nightmares

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 8e1fa57a0a..5007147301 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -71,10 +71,10 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
 lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
-#if __GLASGOW_HASKELL__ <= 808
+#if __GLASGOW_HASKELL__ >= 808
 type PatCompat = Pat
 fromPatCompat = id
-#elif
+#else
 type PatCompat = LPat
 fromPatCompat = unLoc
 #endif

From b700c35c5219305accabcd451b3ca7a0efc056d6 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:52:34 -0700
Subject: [PATCH 43/50] type syn of type syn

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 5007147301..1296a9d6d5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -72,10 +72,10 @@ lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
 #if __GLASGOW_HASKELL__ >= 808
-type PatCompat = Pat
+type PatCompat pass = Pat pass
 fromPatCompat = id
 #else
-type PatCompat = LPat
+type PatCompat pass = LPat pass
 fromPatCompat = unLoc
 #endif
 

From 25b9133dffa0ffea6106f41df891b13dc6a44de9 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 10:53:30 -0700
Subject: [PATCH 44/50] wtfff

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

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 1296a9d6d5..9381d180d5 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -71,7 +71,7 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
 lambdaCaseable _ = Nothing
 
 fromPatCompat :: PatCompat pass -> Pat pass
-#if __GLASGOW_HASKELL__ >= 808
+#if __GLASGOW_HASKELL__ == 808
 type PatCompat pass = Pat pass
 fromPatCompat = id
 #else

From baac4508e9ef28cd07af7b75ae4d2c68c111eb6d Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 11:09:32 -0700
Subject: [PATCH 45/50] maybe this time

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 9381d180d5..85a96adfca 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -70,7 +70,7 @@ lambdaCaseable (splitFunTy_maybe -> Just (arg, res))
   = Just $ isJust $ algebraicTyCon res
 lambdaCaseable _ = Nothing
 
-fromPatCompat :: PatCompat pass -> Pat pass
+fromPatCompat :: PatCompat GhcTc -> Pat GhcTc
 #if __GLASGOW_HASKELL__ == 808
 type PatCompat pass = Pat pass
 fromPatCompat = id
@@ -100,7 +100,7 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-#endif
     XPat    p     -> getPatName $ unLoc p
+#endif
     _             -> Nothing
 

From c6e10fddbc78b06c2607f03eb9933a655f6fc19b Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 12:00:27 -0700
Subject: [PATCH 46/50] omg plzz 810

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index 85a96adfca..c5933e6240 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -100,7 +100,11 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-    XPat    p     -> getPatName $ unLoc p
+    XPat    p     -> getPatName $
+#if __GLASGOW_HASKELL__ < 810
+      unLoc
+#endif
+            p
 #endif
     _             -> Nothing
 

From c26f9bae021c3cc8819f737c60f6b3b129b7fcba Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Fri, 16 Oct 2020 12:13:49 -0700
Subject: [PATCH 47/50] dsgjdsgidgjis

---
 plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
index c5933e6240..7f89e4c0c9 100644
--- a/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/tactics/src/Ide/Plugin/Tactic/GHC.hs
@@ -100,11 +100,9 @@ getPatName (fromPatCompat -> p0) =
     ViewPat _ _ p -> getPatName p
 #if __GLASGOW_HASKELL__ >= 808
     SigPat  _ p _ -> getPatName p
-    XPat    p     -> getPatName $
-#if __GLASGOW_HASKELL__ < 810
-      unLoc
 #endif
-            p
+#if __GLASGOW_HASKELL__ == 808
+    XPat   p      -> getPatName $ unLoc p
 #endif
     _             -> Nothing
 

From 71d09399d256e2b6d05c48bbe1334ae29167ed0f Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 18:25:52 -0700
Subject: [PATCH 48/50] Split tactics into a separate package

---
 .circleci/config.yml                         |  9 +++
 cabal.project                                |  1 +
 haskell-language-server.cabal                | 24 +-----
 hie.yaml.cbl                                 |  2 +-
 hie.yaml.stack                               |  2 +-
 plugins/default/src/Ide/Plugin/ModuleName.hs |  1 -
 plugins/tactics/hls-tactics-plugin.cabal     | 80 ++++++++++++++++++++
 stack-8.10.1.yaml                            |  1 +
 stack-8.10.2.yaml                            |  1 +
 stack-8.6.4.yaml                             |  1 +
 stack-8.6.5.yaml                             |  1 +
 stack-8.8.2.yaml                             |  1 +
 stack-8.8.3.yaml                             |  1 +
 stack-8.8.4.yaml                             |  1 +
 14 files changed, 101 insertions(+), 25 deletions(-)
 create mode 100644 plugins/tactics/hls-tactics-plugin.cabal

diff --git a/.circleci/config.yml b/.circleci/config.yml
index fbd50f1df9..2046c7934d 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -72,6 +72,15 @@ defaults: &defaults
         command: stack --stack-yaml=${STACK_FILE} test haskell-language-server --dump-logs --test-arguments="-j1"
         no_output_timeout: 120m
 
+    - run:
+        name: Test hls-tactics-plugin
+        # Tasty by default will run all the tests in parallel. Which should
+        # work ok, but given that these CircleCI runners aren't the beefiest
+        # machine can cause some flakiness. So pass -j1 to Tasty (NOT Stack) to
+        # tell it to go slow and steady.
+        command: stack --stack-yaml=${STACK_FILE} test hls-tactics-plugin:test:func-test --dump-logs --test-arguments="-j1"
+        no_output_timeout: 120m
+
     - store_test_results:
         path: test-results
 
diff --git a/cabal.project b/cabal.project
index 6323590cf8..205abb9eee 100644
--- a/cabal.project
+++ b/cabal.project
@@ -2,6 +2,7 @@ packages:
          ./
          ghcide
          hls-plugin-api
+         ./plugins/tactics
 
 source-repository-package
   type: git
diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index 4f75fad4c6..6b514fc6f4 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -80,7 +80,7 @@ library
 executable haskell-language-server
   import:           agpl, common-deps
   main-is:          Main.hs
-  hs-source-dirs:   exe plugins/default/src plugins/tactics/src
+  hs-source-dirs:   exe plugins/default/src
   other-modules:
     Ide.Plugin.Eval
     Ide.Plugin.Example
@@ -93,21 +93,6 @@ executable haskell-language-server
     Ide.Plugin.Pragmas
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
-    Ide.Plugin.Tactic
-    Ide.Plugin.Tactic.Auto
-    Ide.Plugin.Tactic.CodeGen
-    Ide.Plugin.Tactic.Context
-    Ide.Plugin.Tactic.Debug
-    Ide.Plugin.Tactic.GHC
-    Ide.Plugin.Tactic.Judgements
-    Ide.Plugin.Tactic.KnownStrategies
-    Ide.Plugin.Tactic.Machinery
-    Ide.Plugin.Tactic.Naming
-    Ide.Plugin.Tactic.Range
-    Ide.Plugin.Tactic.Tactics
-    Ide.Plugin.Tactic.Types
-    Ide.Plugin.Tactic.TestTypes
-    Ide.TreeTransform
 
   ghc-options:
     -threaded -Wall -Wno-name-shadowing -Wredundant-constraints
@@ -135,6 +120,7 @@ executable haskell-language-server
     , haskell-language-server
     , haskell-lsp              ^>=0.22
     , hls-plugin-api
+    , hls-tactics-plugin
     , lens
     , ormolu                   ^>=0.1.2
     , regex-tdfa
@@ -153,15 +139,9 @@ executable haskell-language-server
     , stylish-haskell          ^>=0.12
     , temporary
     , text
-    , syb
     , time
     , transformers
     , unordered-containers
-    , ghc-source-gen
-    , refinery                 ^>=0.3
-    , ghc-exactprint
-    , fingertree
-    , generic-lens
 
   if flag(agpl)
     build-depends: brittany
diff --git a/hie.yaml.cbl b/hie.yaml.cbl
index 46730ab9d9..af9ba677d6 100644
--- a/hie.yaml.cbl
+++ b/hie.yaml.cbl
@@ -26,7 +26,7 @@ cradle:
               component: "haskell-language-server:exe:haskell-language-server"
 
             - path: "./plugins/tactics/src"
-              component: "haskell-language-server:exe:haskell-language-server"
+              component: "lib:hls-tactics-plugin"
 
             - path: "./exe/Wrapper.hs"
               component: "haskell-language-server:exe:haskell-language-server-wrapper"
diff --git a/hie.yaml.stack b/hie.yaml.stack
index f9400d0914..1c5362b45f 100644
--- a/hie.yaml.stack
+++ b/hie.yaml.stack
@@ -22,7 +22,7 @@ cradle:
             - path: "./plugins/default/src"
               component: "haskell-language-server:exe:haskell-language-server"
             - path: "./plugins/tactics/src"
-              component: "haskell-language-server:exe:haskell-language-server"
+              component: "hls-tactics-plugin:lib:hls-tactics-plugin"
 
             - path: "./exe/Arguments.hs"
               component: "haskell-language-server:exe:haskell-language-server"
diff --git a/plugins/default/src/Ide/Plugin/ModuleName.hs b/plugins/default/src/Ide/Plugin/ModuleName.hs
index 97ffbe0abf..a7b878f387 100644
--- a/plugins/default/src/Ide/Plugin/ModuleName.hs
+++ b/plugins/default/src/Ide/Plugin/ModuleName.hs
@@ -94,7 +94,6 @@ import           Development.IDE.Core.Shake
 import           Data.Text                      ( pack )
 import           System.Directory               ( canonicalizePath )
 import           Data.List
-import           Ide.Plugin.Tactic.Debug        ( unsafeRender )
 -- |Plugin descriptor
 descriptor :: PluginId -> PluginDescriptor
 descriptor plId = (defaultPluginDescriptor plId)
diff --git a/plugins/tactics/hls-tactics-plugin.cabal b/plugins/tactics/hls-tactics-plugin.cabal
new file mode 100644
index 0000000000..9abb2b549d
--- /dev/null
+++ b/plugins/tactics/hls-tactics-plugin.cabal
@@ -0,0 +1,80 @@
+cabal-version:      2.2
+category:           Development
+name:               hls-tactics-plugin
+version:            0.5.1.0
+synopsis:           LSP server for GHC
+description:
+  Please see the README on GitHub at <https://github.com/isovector/hls-tactics-plugin#readme>
+
+homepage:           https://github.com/isovector/hls-tactics-plugin#readme
+bug-reports:        https://github.com/isovector/hls-tactics-plugin/issues
+author:             Sandy Maguire, Reed Mullanix
+maintainer:         sandy@sandymaguire.me
+copyright:          Sandy Maguire, Reed Mullanix
+-- license:            Apache-2.0
+-- license-file:       LICENSE
+build-type:         Simple
+-- extra-source-files:
+--   README.md
+--   ChangeLog.md
+
+flag pedantic
+  description: Enable -Werror
+  default:     False
+  manual:      True
+
+source-repository head
+  type:     git
+  location: https://github.com/isovector/hls-tactics-plugin
+
+library
+  hs-source-dirs:   src
+  exposed-modules:
+    Ide.Plugin.Tactic
+    Ide.Plugin.Tactic.Auto
+    Ide.Plugin.Tactic.CodeGen
+    Ide.Plugin.Tactic.Context
+    Ide.Plugin.Tactic.Debug
+    Ide.Plugin.Tactic.GHC
+    Ide.Plugin.Tactic.Judgements
+    Ide.Plugin.Tactic.KnownStrategies
+    Ide.Plugin.Tactic.Machinery
+    Ide.Plugin.Tactic.Naming
+    Ide.Plugin.Tactic.Range
+    Ide.Plugin.Tactic.Tactics
+    Ide.Plugin.Tactic.Types
+    Ide.Plugin.Tactic.TestTypes
+    Ide.TreeTransform
+
+  ghc-options:
+    -Wno-name-shadowing -Wredundant-constraints
+  if flag(pedantic)
+    ghc-options: -Werror
+
+  build-depends:
+    , aeson
+    , base           >=4.12 && <5
+    , containers
+    , directory
+    , extra
+    , filepath
+    , fingertree
+    , generic-lens
+    , ghc
+    , ghc-boot-th
+    , ghc-exactprint
+    , ghc-source-gen
+    , ghcide         >=0.1
+    , haskell-lsp    ^>=0.22
+    , hls-plugin-api
+    , lens
+    , mtl
+    , refinery       ^>=0.3
+    , retrie         >=0.1.1.0
+    , shake          >=0.17.5
+    , syb
+    , text
+    , transformers
+
+  default-language: Haskell2010
+
diff --git a/stack-8.10.1.yaml b/stack-8.10.1.yaml
index 8353abf148..577041af4a 100644
--- a/stack-8.10.1.yaml
+++ b/stack-8.10.1.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.10.2.yaml b/stack-8.10.2.yaml
index 66fa833fb6..3570c1cdb5 100644
--- a/stack-8.10.2.yaml
+++ b/stack-8.10.2.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.6.4.yaml b/stack-8.6.4.yaml
index 9796b068ef..e27a62be4f 100644
--- a/stack-8.6.4.yaml
+++ b/stack-8.6.4.yaml
@@ -5,6 +5,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.6.5.yaml b/stack-8.6.5.yaml
index 1a0b67c2b2..93a47a3472 100644
--- a/stack-8.6.5.yaml
+++ b/stack-8.6.5.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.8.2.yaml b/stack-8.8.2.yaml
index 94ad80cd99..3b780ed048 100644
--- a/stack-8.8.2.yaml
+++ b/stack-8.8.2.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.8.3.yaml b/stack-8.8.3.yaml
index c01a2649e1..07e3e6310f 100644
--- a/stack-8.8.3.yaml
+++ b/stack-8.8.3.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock
diff --git a/stack-8.8.4.yaml b/stack-8.8.4.yaml
index 57518e9e24..3627d24139 100644
--- a/stack-8.8.4.yaml
+++ b/stack-8.8.4.yaml
@@ -4,6 +4,7 @@ packages:
 - .
 - ./ghcide/
 - ./hls-plugin-api
+- ./plugins/tactics
 
 ghc-options:
   "$everything": -haddock

From 91f3be0b4ce56caf745b455340fa59aca176b046 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 18 Oct 2020 18:32:38 -0700
Subject: [PATCH 49/50] Tactics don't have tests, so CI doesn't need to change

---
 .circleci/config.yml | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 2046c7934d..fbd50f1df9 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -72,15 +72,6 @@ defaults: &defaults
         command: stack --stack-yaml=${STACK_FILE} test haskell-language-server --dump-logs --test-arguments="-j1"
         no_output_timeout: 120m
 
-    - run:
-        name: Test hls-tactics-plugin
-        # Tasty by default will run all the tests in parallel. Which should
-        # work ok, but given that these CircleCI runners aren't the beefiest
-        # machine can cause some flakiness. So pass -j1 to Tasty (NOT Stack) to
-        # tell it to go slow and steady.
-        command: stack --stack-yaml=${STACK_FILE} test hls-tactics-plugin:test:func-test --dump-logs --test-arguments="-j1"
-        no_output_timeout: 120m
-
     - store_test_results:
         path: test-results
 

From b2e1fb3ceaa823a475dce05039b613d3db3dc715 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Mon, 19 Oct 2020 09:54:40 -0700
Subject: [PATCH 50/50] Oops; bad merge

---
 haskell-language-server.cabal | 18 ------------------
 1 file changed, 18 deletions(-)

diff --git a/haskell-language-server.cabal b/haskell-language-server.cabal
index e03b23b7be..6b514fc6f4 100644
--- a/haskell-language-server.cabal
+++ b/haskell-language-server.cabal
@@ -93,24 +93,6 @@ executable haskell-language-server
     Ide.Plugin.Pragmas
     Ide.Plugin.Retrie
     Ide.Plugin.StylishHaskell
-<<<<<<< HEAD
-=======
-    Ide.Plugin.Tactic
-    Ide.Plugin.Tactic.Auto
-    Ide.Plugin.Tactic.CodeGen
-    Ide.Plugin.Tactic.Context
-    Ide.Plugin.Tactic.Debug
-    Ide.Plugin.Tactic.GHC
-    Ide.Plugin.Tactic.Judgements
-    Ide.Plugin.Tactic.KnownStrategies
-    Ide.Plugin.Tactic.Machinery
-    Ide.Plugin.Tactic.Naming
-    Ide.Plugin.Tactic.Range
-    Ide.Plugin.Tactic.Tactics
-    Ide.Plugin.Tactic.Types
-    Ide.Plugin.Tactic.TestTypes
-    Ide.TreeTransform
->>>>>>> master
 
   ghc-options:
     -threaded -Wall -Wno-name-shadowing -Wredundant-constraints