From 425953d5a1ac59477c5f998276b2ee13d6e02214 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 10:26:10 -0800
Subject: [PATCH 01/10] Implement "use constructor" code action

---
 .../src/Ide/Plugin/Tactic/FeatureSet.hs       |  2 +-
 .../src/Ide/Plugin/Tactic/GHC.hs              | 30 +++++++----
 .../Tactic/LanguageServer/TacticProviders.hs  | 27 ++++++++++
 .../src/Ide/Plugin/Tactic/Tactics.hs          | 31 ++++++++---
 .../src/Ide/Plugin/Tactic/TestTypes.hs        |  2 +
 plugins/hls-tactics-plugin/test/GoldenSpec.hs | 53 +++++++++++++------
 .../test/golden/ConProviders.hs               | 10 ++++
 .../test/golden/UseConLeft.hs                 |  3 ++
 .../test/golden/UseConLeft.hs.expected        |  3 ++
 .../test/golden/UseConPair.hs                 |  2 +
 .../test/golden/UseConPair.hs.expected        |  2 +
 .../test/golden/UseConRight.hs                |  3 ++
 .../test/golden/UseConRight.hs.expected       |  3 ++
 13 files changed, 137 insertions(+), 34 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/ConProviders.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConLeft.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConPair.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConRight.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
index a5bf4b53c8..394e688f73 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
@@ -21,7 +21,7 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = CantHaveAnEmptyDataType
+data Feature = FeatureUseDataCon
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index b05952b1af..c3f05d9ad7 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -9,26 +9,25 @@
 
 module Ide.Plugin.Tactic.GHC where
 
+import           Control.Arrow
 import           Control.Monad.State
-import           Data.Function              (on)
-import           Data.List                  (isPrefixOf)
-import qualified Data.Map                   as M
-import           Data.Maybe                 (isJust)
-import           Data.Set                   (Set)
-import qualified Data.Set                   as S
+import           Data.Function (on)
+import           Data.List (isPrefixOf)
+import qualified Data.Map as M
+import           Data.Maybe (isJust)
+import           Data.Set (Set)
+import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
 import           Development.IDE.GHC.Compat
-import           GHC.SourceGen              (case', lambda, match)
-import           Generics.SYB               (Data, everything, everywhere,
-                                             listify, mkQ, mkT)
+import           GHC.SourceGen (case', lambda, match)
+import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
 import           Ide.Plugin.Tactic.Types
 import           OccName
 import           TcType
 import           TyCoRep
 import           Type
-import           TysWiredIn                 (charTyCon, doubleTyCon, floatTyCon,
-                                             intTyCon)
+import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
 import           Unique
 import           Var
 
@@ -81,6 +80,12 @@ tacticsThetaTy :: Type -> ThetaType
 tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 
 
+------------------------------------------------------------------------------
+-- | Get the data cons of a type, if it has any.
+tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
+tacticsGetDataCons =
+  fmap (first tyConDataCons) . splitTyConApp_maybe
+
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
 -- skolems.
@@ -131,6 +136,9 @@ algebraicTyCon _ = Nothing
 eqRdrName :: RdrName -> RdrName -> Bool
 eqRdrName = (==) `on` occNameString . occName
 
+sloppyEqOccName :: OccName -> OccName -> Bool
+sloppyEqOccName = (==) `on` occNameString
+
 
 ------------------------------------------------------------------------------
 -- | Does this thing contain any references to 'HsVar's with the given
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index d495bb8d37..b661e42985 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE OverloadedStrings  #-}
 {-# LANGUAGE ViewPatterns       #-}
+{-# OPTIONS_GHC -Wall           #-}
 
 module Ide.Plugin.Tactic.LanguageServer.TacticProviders
   ( commandProvider
@@ -14,12 +15,14 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders
 import           Control.Monad
 import           Control.Monad.Error.Class    (MonadError (throwError))
 import           Data.Aeson
+import           Data.Bool (bool)
 import           Data.Coerce
 import qualified Data.Map                     as M
 import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Text                    as T
 import           Data.Traversable
+import           DataCon (dataConName)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
 import           GHC.LanguageExtensions.Type  (Extension (LambdaCase))
@@ -47,6 +50,7 @@ commandTactic Destruct               = useNameFromHypothesis destruct
 commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic UseDataCon             = userSplit
 
 
 ------------------------------------------------------------------------------
@@ -71,6 +75,22 @@ commandProvider HomomorphismLambdaCase =
   requireExtension LambdaCase $
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
+commandProvider UseDataCon =
+  requireFeature FeatureUseDataCon $
+    filterTypeProjection
+        ( guardLength (<= 5)
+        . fromMaybe []
+        . fmap fst
+        . tacticsGetDataCons
+        ) $ \dcon ->
+      provide UseDataCon
+        . T.pack
+        . occNameString
+        . occName
+        $ dataConName dcon
+
+guardLength :: (Int -> Bool) -> [a] -> [a]
+guardLength f as = bool [] as $ f $ length as
 
 
 ------------------------------------------------------------------------------
@@ -140,6 +160,13 @@ filterBindingType p tp dflags fs plId uri range jdg =
               True  -> tp (hi_name hi) ty dflags fs plId uri range jdg
               False -> pure []
 
+filterTypeProjection
+    :: (Type -> [a])  -- ^ Features of the goal to look into further
+    -> (a -> TacticProvider)
+    -> TacticProvider
+filterTypeProjection p tp dflags fs plId uri range jdg =
+  fmap join $ for ( p $ unCType $ jGoal jdg) $ \a ->
+      tp a dflags fs plId uri range jdg
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index ae1eda428c..c85b4104f3 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -31,7 +31,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 (occNameString, occName)
 import           Refinery.Tactic
 import           Refinery.Tactic.Internal
 import           TcType
@@ -197,10 +197,9 @@ splitAuto :: TacticsM ()
 splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
   jdg <- goal
   let g = jGoal jdg
-  case splitTyConApp_maybe $ unCType g of
+  case tacticsGetDataCons $ unCType g of
     Nothing -> throwError $ GoalMismatch "split" g
-    Just (tc, _) -> do
-      let dcs = tyConDataCons tc
+    Just (dcs, _) -> do
       case isSplitWhitelisted jdg of
         True -> choice $ fmap splitDataCon dcs
         False -> do
@@ -222,18 +221,36 @@ requireNewHoles m = do
 
 ------------------------------------------------------------------------------
 -- | Attempt to instantiate the given data constructor to solve the goal.
+--
+-- INVARIANT: Assumes the give datacon is appropriate to construct the type
+-- with.
 splitDataCon :: DataCon -> TacticsM ()
 splitDataCon dc =
   requireConcreteHole $ tracing ("splitDataCon:" <> show dc) $ rule $ \jdg -> do
     let g = jGoal jdg
     case splitTyConApp_maybe $ unCType g of
       Just (tc, apps) -> do
-        case elem dc $ tyConDataCons tc of
-          True  -> buildDataCon (unwhitelistingSplit jdg) dc apps
-          False -> throwError $ IncorrectDataCon dc
+        buildDataCon (unwhitelistingSplit jdg) dc apps
       Nothing -> throwError $ GoalMismatch "splitDataCon" g
 
 
+------------------------------------------------------------------------------
+-- | User-facing tactic to implement "Use constructor <x>"
+userSplit :: OccName -> TacticsM ()
+userSplit occ = do
+  jdg <- goal
+  let g = jGoal jdg
+  -- TODO(sandy): It's smelly that we need to find the datacon to generate the
+  -- code action, send it as a string, and then look it up again. Can we push
+  -- this over LSP somehow instead?
+  case splitTyConApp_maybe $ unCType g of
+    Just (tc, apps) -> do
+      case find (sloppyEqOccName occ . occName . dataConName)
+             $ tyConDataCons tc of
+        Just dc -> splitDataCon dc
+        Nothing -> throwError $ NotInScope occ
+
+
 ------------------------------------------------------------------------------
 -- | @matching f@ takes a function from a judgement to a @Tactic@, and
 -- then applies the resulting @Tactic@.
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index 970e7b6671..641c1b1d28 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -17,6 +17,7 @@ data TacticCommand
   | Homomorphism
   | DestructLambdaCase
   | HomomorphismLambdaCase
+  | UseDataCon
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -27,6 +28,7 @@ tacticTitle Destruct var             = "Case split on " <> var
 tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
+tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index 7a8b63e0d8..d3082831b7 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -8,26 +8,24 @@
 module GoldenSpec where
 
 import           Control.Applicative.Combinators (skipManyTill)
-import           Control.Lens                    hiding (failing, (<.>))
-import           Control.Monad                   (unless)
+import           Control.Lens hiding (failing, (<.>))
+import           Control.Monad (unless)
 import           Control.Monad.IO.Class
 import           Data.Aeson
-import           Data.Default                    (Default (def))
+import           Data.Default (Default (def))
 import           Data.Foldable
-import qualified Data.Map                        as M
+import qualified Data.Map as M
 import           Data.Maybe
-import           Data.Text                       (Text)
-import qualified Data.Text.IO                    as T
-import qualified Ide.Plugin.Config               as Plugin
-import           Ide.Plugin.Tactic.FeatureSet    (FeatureSet, allFeatures)
+import           Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+import qualified Ide.Plugin.Config as Plugin
+import           Ide.Plugin.Tactic.FeatureSet (FeatureSet, allFeatures)
 import           Ide.Plugin.Tactic.TestTypes
 import           Language.LSP.Test
 import           Language.LSP.Types
-import           Language.LSP.Types.Lens         hiding (actions, applyEdit,
-                                                  capabilities, executeCommand,
-                                                  id, line, message, name,
-                                                  rename, title)
-import           System.Directory                (doesFileExist)
+import           Language.LSP.Types.Lens hiding (actions, applyEdit, capabilities, executeCommand, id, line, message, name, rename, title)
+import           System.Directory (doesFileExist)
 import           System.FilePath
 import           Test.Hspec
 
@@ -73,9 +71,33 @@ spec = do
       [ (not, DestructLambdaCase, "")
       ]
 
+  let goldenTest = mkGoldenTest allFeatures
+
+  describe "use constructor" $ do
+    let useTest = mkGoldenTest allFeatures UseDataCon
+    describe "provider" $ do
+      mkTest
+        "Suggests all data cons for Either"
+        "ConProviders.hs" 3 6
+        [ (id, UseDataCon, "Left")
+        , (id, UseDataCon, "Right")
+        , (not, UseDataCon, ":")
+        , (not, UseDataCon, "[]")
+        , (not, UseDataCon, "C1")
+        ]
+      mkTest
+        "Suggests no data cons for big types"
+        "ConProviders.hs" 9 17 $ do
+          c <- [1 :: Int .. 10]
+          pure $ (not, UseDataCon, T.pack $ show c)
+
+    describe "golden" $ do
+      useTest "(,)"   "UseConPair.hs"  2 8
+      useTest "Left"  "UseConLeft.hs"  2 8
+      useTest "Right" "UseConRight.hs" 2 8
+
   describe "golden tests" $ do
-    let goldenTest = mkGoldenTest allFeatures
-        autoTest = mkGoldenTest allFeatures Auto ""
+    let autoTest = mkGoldenTest allFeatures Auto ""
 
     goldenTest Intros "" "GoldenIntros.hs" 2 8
     autoTest "GoldenEitherAuto.hs"        2 11
@@ -150,6 +172,7 @@ mkTest
     -> SpecWith (Arg Bool)
 mkTest name fp line col ts = it name $ do
   runSession testCommand fullCaps tacticPath $ do
+    setFeatureSet allFeatures
     doc <- openDoc fp "haskell"
     _ <- waitForDiagnostics
     actions <- getCodeActions doc $ pointRange line col
diff --git a/plugins/hls-tactics-plugin/test/golden/ConProviders.hs b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs
new file mode 100644
index 0000000000..d3124fecd5
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs
@@ -0,0 +1,10 @@
+-- Should suggest Left and Right, but not []
+t1 :: Either a b
+t1 = _
+
+
+data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10
+
+noCtorsIfMany :: ManyConstructors
+noCtorsIfMany = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs
new file mode 100644
index 0000000000..59d03ae7d0
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs
@@ -0,0 +1,3 @@
+test :: Either a b
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected
new file mode 100644
index 0000000000..cd04697d6a
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConLeft.hs.expected
@@ -0,0 +1,3 @@
+test :: Either a b
+test = Left _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConPair.hs b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs
new file mode 100644
index 0000000000..2d15fe3500
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs
@@ -0,0 +1,2 @@
+test :: (a, b)
+test = _
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected
new file mode 100644
index 0000000000..130c3dd7c9
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConPair.hs.expected
@@ -0,0 +1,2 @@
+test :: (a, b)
+test = (_, _)
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConRight.hs b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs
new file mode 100644
index 0000000000..59d03ae7d0
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs
@@ -0,0 +1,3 @@
+test :: Either a b
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected
new file mode 100644
index 0000000000..beaecf28c5
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/UseConRight.hs.expected
@@ -0,0 +1,3 @@
+test :: Either a b
+test = Right _
+

From 82cdc8babebb075f37a705669c00e68b572dcca2 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 10:33:34 -0800
Subject: [PATCH 02/10] Haddock

---
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs    |  7 +++++--
 .../Plugin/Tactic/LanguageServer/TacticProviders.hs    | 10 ++++++++--
 plugins/hls-tactics-plugin/test/GoldenSpec.hs          |  2 ++
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index c3f05d9ad7..f385d6085a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -131,11 +131,14 @@ algebraicTyCon _ = Nothing
 
 
 ------------------------------------------------------------------------------
--- | We can't compare 'RdrName' for equality directly. Instead, compare them by
--- their 'OccName's.
+-- | We can't compare 'RdrName' for equality directly. Instead, sloppily
+-- compare them by their 'OccName's.
 eqRdrName :: RdrName -> RdrName -> Bool
 eqRdrName = (==) `on` occNameString . occName
 
+
+------------------------------------------------------------------------------
+-- | Compare two 'OccName's for unqualified equality.
 sloppyEqOccName :: OccName -> OccName -> Bool
 sloppyEqOccName = (==) `on` occNameString
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index b661e42985..db08508940 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -89,6 +89,9 @@ commandProvider UseDataCon =
         . occName
         $ dataConName dcon
 
+
+------------------------------------------------------------------------------
+-- | Return an empty list if the given predicate doesn't hold over the length
 guardLength :: (Int -> Bool) -> [a] -> [a]
 guardLength f as = bool [] as $ f $ length as
 
@@ -160,12 +163,16 @@ filterBindingType p tp dflags fs plId uri range jdg =
               True  -> tp (hi_name hi) ty dflags fs plId uri range jdg
               False -> pure []
 
+
+------------------------------------------------------------------------------
+-- | Multiply a 'TacticProvider' by some feature projection out of the goal
+-- type. Used e.g. to crete a code action for every data constructor.
 filterTypeProjection
     :: (Type -> [a])  -- ^ Features of the goal to look into further
     -> (a -> TacticProvider)
     -> TacticProvider
 filterTypeProjection p tp dflags fs plId uri range jdg =
-  fmap join $ for ( p $ unCType $ jGoal jdg) $ \a ->
+  fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
       tp a dflags fs plId uri range jdg
 
 
@@ -201,7 +208,6 @@ tcCommandId :: TacticCommand -> CommandId
 tcCommandId c = coerce $ T.pack $ "tactics" <> show c <> "Command"
 
 
-
 ------------------------------------------------------------------------------
 -- | We should show homos only when the goal type is the same as the binding
 -- type, and that both are usual algebraic types.
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index d3082831b7..9b4a8ca119 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -73,6 +73,8 @@ spec = do
 
   let goldenTest = mkGoldenTest allFeatures
 
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/use constructor/"'
   describe "use constructor" $ do
     let useTest = mkGoldenTest allFeatures UseDataCon
     describe "provider" $ do

From b73cf83e06117fd666917b78dd4fa38ee52a37a0 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 11:04:42 -0800
Subject: [PATCH 03/10] Make use ctor actions configurable

---
 .../src/Ide/Plugin/Tactic.hs                  | 30 +++++-----
 .../src/Ide/Plugin/Tactic/LanguageServer.hs   | 18 ++++--
 .../Tactic/LanguageServer/TacticProviders.hs  | 56 +++++++++++--------
 .../src/Ide/Plugin/Tactic/TestTypes.hs        | 18 +++---
 4 files changed, 69 insertions(+), 53 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 3fb774d4d1..5a0a8e0156 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -13,30 +13,28 @@ module Ide.Plugin.Tactic
   , TacticCommand (..)
   ) where
 
-import           Bag                                              (bagToList,
-                                                                   listToBag)
-import           Control.Exception                                (evaluate)
+import           Bag (bagToList, listToBag)
+import           Control.Exception (evaluate)
 import           Control.Monad
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.Aeson
-import           Data.Bifunctor                                   (Bifunctor (bimap))
-import           Data.Bool                                        (bool)
-import           Data.Data                                        (Data)
+import           Data.Bifunctor (Bifunctor (bimap))
+import           Data.Bool (bool)
+import           Data.Data (Data)
 import           Data.Foldable (for_)
-import           Data.Generics.Aliases                            (mkQ)
-import           Data.Generics.Schemes                            (everything)
+import           Data.Generics.Aliases (mkQ)
+import           Data.Generics.Schemes (everything)
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.Text                                        as T
+import qualified Data.Text as T
 import           Data.Traversable
-import           Development.IDE.Core.Shake                       (IdeState (..))
+import           Development.IDE.Core.Shake (IdeState (..))
 import           Development.IDE.GHC.Compat
 import           Development.IDE.GHC.ExactPrint
 import           Development.Shake.Classes
 import           Ide.Plugin.Tactic.CaseSplit
-import           Ide.Plugin.Tactic.FeatureSet                     (Feature (..),
-                                                                   hasFeature)
+import           Ide.Plugin.Tactic.FeatureSet (Feature (..), hasFeature)
 import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.LanguageServer
 import           Ide.Plugin.Tactic.LanguageServer.TacticProviders
@@ -49,7 +47,7 @@ import           Language.LSP.Server
 import           Language.LSP.Types
 import           Language.LSP.Types.Capabilities
 import           OccName
-import           Prelude                                          hiding (span)
+import           Prelude hiding (span)
 import           System.Timeout
 
 
@@ -71,14 +69,14 @@ descriptor plId = (defaultPluginDescriptor plId)
 codeActionProvider :: PluginMethodHandler IdeState TextDocumentCodeAction
 codeActionProvider state plId (CodeActionParams _ _ (TextDocumentIdentifier uri) range _ctx)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      features <- getFeatureSet (shakeExtras state)
+      cfg <- getTacticConfig $ shakeExtras state
       liftIO $ fromMaybeT (Right $ List []) $ do
-        (_, jdg, _, dflags) <- judgementForHole state nfp range features
+        (_, jdg, _, dflags) <- judgementForHole state nfp range $ cfg_feature_set cfg
         actions <- lift $
           -- This foldMap is over the function monoid.
           foldMap commandProvider [minBound .. maxBound]
             dflags
-            features
+            cfg
             plId
             uri
             range
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
index 4fcbdabd5a..bd8c5e8038 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs
@@ -44,7 +44,7 @@ import           Ide.Plugin.Tactic.GHC
 import           Ide.Plugin.Tactic.Judgements
 import           Ide.Plugin.Tactic.Range
 import           Ide.Plugin.Tactic.TestTypes          (TacticCommand,
-                                                       cfg_feature_set)
+                                                       cfg_feature_set, emptyConfig, Config)
 import           Ide.Plugin.Tactic.Types
 import           Language.LSP.Server                  (MonadLsp)
 import           Language.LSP.Types
@@ -82,13 +82,19 @@ runStaleIde state nfp a = MaybeT $ runIde state $ useWithStale a nfp
 
 
 ------------------------------------------------------------------------------
--- | Get the current feature set from the plugin config.
-getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet
-getFeatureSet extras = do
+-- | Get the the plugin config
+getTacticConfig :: MonadLsp Plugin.Config m => ShakeExtras -> m Config
+getTacticConfig extras = do
   pcfg <- getPluginConfig extras "tactics"
   pure $ case fromJSON $ Object $ plcConfig pcfg of
-    Success cfg -> cfg_feature_set cfg
-    Error _     -> defaultFeatures
+    Success cfg -> cfg
+    Error _     -> emptyConfig
+
+
+------------------------------------------------------------------------------
+-- | Get the current feature set from the plugin config.
+getFeatureSet :: MonadLsp Plugin.Config m => ShakeExtras -> m FeatureSet
+getFeatureSet  = fmap cfg_feature_set . getTacticConfig
 
 
 getIdeDynflags
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index db08508940..140be14eee 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -76,18 +76,19 @@ commandProvider HomomorphismLambdaCase =
     filterGoalType ((== Just True) . lambdaCaseable) $
       provide HomomorphismLambdaCase ""
 commandProvider UseDataCon =
-  requireFeature FeatureUseDataCon $
-    filterTypeProjection
-        ( guardLength (<= 5)
-        . fromMaybe []
-        . fmap fst
-        . tacticsGetDataCons
-        ) $ \dcon ->
-      provide UseDataCon
-        . T.pack
-        . occNameString
-        . occName
-        $ dataConName dcon
+  withConfig $ \cfg ->
+    requireFeature FeatureUseDataCon $
+      filterTypeProjection
+          ( guardLength (<= cfg_max_use_ctor_actions cfg)
+          . fromMaybe []
+          . fmap fst
+          . tacticsGetDataCons
+          ) $ \dcon ->
+        provide UseDataCon
+          . T.pack
+          . occNameString
+          . occName
+          $ dataConName dcon
 
 
 ------------------------------------------------------------------------------
@@ -101,7 +102,7 @@ guardLength f as = bool [] as $ f $ length as
 -- UI.
 type TacticProvider
      = DynFlags
-    -> FeatureSet
+    -> Config
     -> PluginId
     -> Uri
     -> Range
@@ -122,18 +123,18 @@ data TacticParams = TacticParams
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- 'Feature' is in the feature set.
 requireFeature :: Feature -> TacticProvider -> TacticProvider
-requireFeature f tp dflags fs plId uri range jdg = do
-  guard $ hasFeature f fs
-  tp dflags fs plId uri range jdg
+requireFeature f tp dflags cfg plId uri range jdg = do
+  guard $ hasFeature f $ cfg_feature_set cfg
+  tp dflags cfg plId uri range jdg
 
 
 ------------------------------------------------------------------------------
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 requireExtension :: Extension -> TacticProvider -> TacticProvider
-requireExtension ext tp dflags fs plId uri range jdg =
+requireExtension ext tp dflags cfg plId uri range jdg =
   case xopt ext dflags of
-    True  -> tp dflags fs plId uri range jdg
+    True  -> tp dflags cfg plId uri range jdg
     False -> pure []
 
 
@@ -141,9 +142,9 @@ requireExtension ext tp dflags fs plId uri range jdg =
 -- | Restrict a 'TacticProvider', making sure it appears only when the given
 -- predicate holds for the goal.
 filterGoalType :: (Type -> Bool) -> TacticProvider -> TacticProvider
-filterGoalType p tp dflags fs plId uri range jdg =
+filterGoalType p tp dflags cfg plId uri range jdg =
   case p $ unCType $ jGoal jdg of
-    True  -> tp dflags fs plId uri range jdg
+    True  -> tp dflags cfg plId uri range jdg
     False -> pure []
 
 
@@ -154,13 +155,13 @@ filterBindingType
     :: (Type -> Type -> Bool)  -- ^ Goal and then binding types.
     -> (OccName -> Type -> TacticProvider)
     -> TacticProvider
-filterBindingType p tp dflags fs plId uri range jdg =
+filterBindingType p tp dflags cfg plId uri range jdg =
   let hy = jHypothesis jdg
       g  = jGoal jdg
    in fmap join $ for (unHypothesis hy) $ \hi ->
         let ty = unCType $ hi_type hi
          in case p (unCType g) ty of
-              True  -> tp (hi_name hi) ty dflags fs plId uri range jdg
+              True  -> tp (hi_name hi) ty dflags cfg plId uri range jdg
               False -> pure []
 
 
@@ -171,9 +172,16 @@ filterTypeProjection
     :: (Type -> [a])  -- ^ Features of the goal to look into further
     -> (a -> TacticProvider)
     -> TacticProvider
-filterTypeProjection p tp dflags fs plId uri range jdg =
+filterTypeProjection p tp dflags cfg plId uri range jdg =
   fmap join $ for (p $ unCType $ jGoal jdg) $ \a ->
-      tp a dflags fs plId uri range jdg
+      tp a dflags cfg plId uri range jdg
+
+
+------------------------------------------------------------------------------
+-- | Get access to the 'Config' when building a 'TacticProvider'.
+withConfig :: (Config -> TacticProvider) -> TacticProvider
+withConfig tp dflags cfg plId uri range jdg = tp cfg dflags cfg plId uri range jdg
+
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index 641c1b1d28..fa97f1b9c9 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards   #-}
 
 module Ide.Plugin.Tactic.TestTypes where
 
@@ -33,20 +34,23 @@ tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
 
 ------------------------------------------------------------------------------
 -- | Plugin configuration for tactics
-newtype Config = Config
-  { cfg_feature_set :: FeatureSet
+data Config = Config
+  { cfg_feature_set          :: FeatureSet
+  , cfg_max_use_ctor_actions :: Int
   }
 
 emptyConfig :: Config
-emptyConfig = Config defaultFeatures
+emptyConfig = Config defaultFeatures 5
 
 instance ToJSON Config where
-  toJSON (Config features) = object
-    [ "features" .= prettyFeatureSet features
+  toJSON Config{..} = object
+    [ "features" .= prettyFeatureSet cfg_feature_set
+    , "max_use_ctor_actions" .= cfg_max_use_ctor_actions
     ]
 
 instance FromJSON Config where
   parseJSON = withObject "Config" $ \obj -> do
-    features <- parseFeatureSet <$> obj .: "features"
-    pure $ Config features
+    cfg_feature_set          <- parseFeatureSet <$> obj .: "features"
+    cfg_max_use_ctor_actions <- obj .: "max_use_ctor_actions"
+    pure $ Config{..}
 

From 9c20a3ab0b983787942de40e9228f4a2012455e1 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 11:07:54 -0800
Subject: [PATCH 04/10] Undo more stupid formatting

---
 .../Plugin/Tactic/LanguageServer/TacticProviders.hs  | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index 140be14eee..905bf43ecb 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -13,19 +13,19 @@ module Ide.Plugin.Tactic.LanguageServer.TacticProviders
   ) where
 
 import           Control.Monad
-import           Control.Monad.Error.Class    (MonadError (throwError))
+import           Control.Monad.Error.Class (MonadError (throwError))
 import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
-import qualified Data.Map                     as M
+import qualified Data.Map as M
 import           Data.Maybe
 import           Data.Monoid
-import qualified Data.Text                    as T
+import qualified Data.Text as T
 import           Data.Traversable
 import           DataCon (dataConName)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
-import           GHC.LanguageExtensions.Type  (Extension (LambdaCase))
+import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
 import           Ide.Plugin.Tactic.Auto
 import           Ide.Plugin.Tactic.FeatureSet
 import           Ide.Plugin.Tactic.GHC
@@ -37,8 +37,8 @@ import           Ide.PluginUtils
 import           Ide.Types
 import           Language.LSP.Types
 import           OccName
-import           Prelude                      hiding (span)
-import           Refinery.Tactic              (goal)
+import           Prelude hiding (span)
+import           Refinery.Tactic (goal)
 
 
 ------------------------------------------------------------------------------

From 557432e311e6541a704d6d5410f8d6c4de3c0974 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 11:21:03 -0800
Subject: [PATCH 05/10] Use loose parsing for config

---
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs  | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index fa97f1b9c9..219731fbc2 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -4,6 +4,7 @@
 module Ide.Plugin.Tactic.TestTypes where
 
 import           Data.Aeson
+import           Data.Maybe (fromMaybe)
 import qualified Data.Text                    as T
 import           Ide.Plugin.Tactic.FeatureSet
 
@@ -50,7 +51,9 @@ instance ToJSON Config where
 
 instance FromJSON Config where
   parseJSON = withObject "Config" $ \obj -> do
-    cfg_feature_set          <- parseFeatureSet <$> obj .: "features"
-    cfg_max_use_ctor_actions <- obj .: "max_use_ctor_actions"
+    cfg_feature_set          <-
+      parseFeatureSet . fromMaybe "" <$> obj .:? "features"
+    cfg_max_use_ctor_actions <-
+      fromMaybe 5 <$> obj .:? "max_use_ctor_actions"
     pure $ Config{..}
 

From 3d79859f22e6bee41bd6a31e3f7d6bcfcc0b2d10 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 11:30:58 -0800
Subject: [PATCH 06/10] Only show unifiable ctors

---
 .../Tactic/LanguageServer/TacticProviders.hs    | 17 +++++++++++++----
 plugins/hls-tactics-plugin/test/GoldenSpec.hs   | 11 +++++++++--
 .../test/golden/ConProviders.hs                 | 11 +++++++++++
 3 files changed, 33 insertions(+), 6 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index 905bf43ecb..3cd9460cd6 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -22,7 +22,7 @@ import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
-import           DataCon (dataConName)
+import           DataCon (dataConName, dataConCannotMatch)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
@@ -80,9 +80,7 @@ commandProvider UseDataCon =
     requireFeature FeatureUseDataCon $
       filterTypeProjection
           ( guardLength (<= cfg_max_use_ctor_actions cfg)
-          . fromMaybe []
-          . fmap fst
-          . tacticsGetDataCons
+          . useCtorFilter
           ) $ \dcon ->
         provide UseDataCon
           . T.pack
@@ -231,3 +229,14 @@ destructFilter :: Type -> Type -> Bool
 destructFilter _ (algebraicTyCon -> Just _) = True
 destructFilter _ _                          = False
 
+
+------------------------------------------------------------------------------
+-- | Only show data cons in "Use constructor" if they can unify with the goal
+useCtorFilter :: Type -> [DataCon]
+useCtorFilter ty
+  | Just (dcs, apps) <- tacticsGetDataCons ty = do
+      dc <- dcs
+      guard $ not $ dataConCannotMatch apps dc
+      pure dc
+useCtorFilter _ = []
+
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index 9b4a8ca119..5e3fd4b9e5 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -80,7 +80,7 @@ spec = do
     describe "provider" $ do
       mkTest
         "Suggests all data cons for Either"
-        "ConProviders.hs" 3 6
+        "ConProviders.hs" 5 6
         [ (id, UseDataCon, "Left")
         , (id, UseDataCon, "Right")
         , (not, UseDataCon, ":")
@@ -89,9 +89,16 @@ spec = do
         ]
       mkTest
         "Suggests no data cons for big types"
-        "ConProviders.hs" 9 17 $ do
+        "ConProviders.hs" 11 17 $ do
           c <- [1 :: Int .. 10]
           pure $ (not, UseDataCon, T.pack $ show c)
+      mkTest
+        "Suggests only matching data cons for GADT"
+        "ConProviders.hs" 20 12
+        [ (id, UseDataCon, "IntGADT")
+        , (id, UseDataCon, "VarGADT")
+        , (not, UseDataCon, "BoolGADT")
+        ]
 
     describe "golden" $ do
       useTest "(,)"   "UseConPair.hs"  2 8
diff --git a/plugins/hls-tactics-plugin/test/golden/ConProviders.hs b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs
index d3124fecd5..19dbc3c6e5 100644
--- a/plugins/hls-tactics-plugin/test/golden/ConProviders.hs
+++ b/plugins/hls-tactics-plugin/test/golden/ConProviders.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 -- Should suggest Left and Right, but not []
 t1 :: Either a b
 t1 = _
@@ -8,3 +10,12 @@ data ManyConstructors = C1 | C2 | C3 | C4 | C5 | C6 | C7 | C8 | C9 | C10
 noCtorsIfMany :: ManyConstructors
 noCtorsIfMany = _
 
+
+data GADT a where
+  IntGADT  :: GADT Int
+  BoolGADT :: GADT Bool
+  VarGADT  :: GADT a
+
+gadtCtor :: GADT Int
+gadtCtor = _
+

From 94c02b374cc533163b16b0d7f05cf3eaa88db98e Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 12:08:18 -0800
Subject: [PATCH 07/10] Don't use guard in IO

Missing features were accidentally blocking all code actions
---
 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs          | 2 +-
 .../src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs  | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 5a0a8e0156..011315dd8b 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -88,7 +88,7 @@ codeActionProvider _ _ _ = pure $ Right $ List []
 tacticCmd :: (OccName -> TacticsM ()) -> CommandFunction IdeState TacticParams
 tacticCmd tac state (TacticParams uri range var_name)
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
-      features <- getFeatureSet (shakeExtras state)
+      features <- getFeatureSet $ shakeExtras state
       ccs <- getClientCapabilities
       res <- liftIO $ fromMaybeT (Right Nothing) $ do
         (range', jdg, ctx, dflags) <- judgementForHole state nfp range features
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index 3cd9460cd6..ea2399e571 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -122,8 +122,9 @@ data TacticParams = TacticParams
 -- 'Feature' is in the feature set.
 requireFeature :: Feature -> TacticProvider -> TacticProvider
 requireFeature f tp dflags cfg plId uri range jdg = do
-  guard $ hasFeature f $ cfg_feature_set cfg
-  tp dflags cfg plId uri range jdg
+  case hasFeature f $ cfg_feature_set cfg of
+    True  -> tp dflags cfg plId uri range jdg
+    False -> pure []
 
 
 ------------------------------------------------------------------------------

From 277bb649b5ba1b2486f64e3ed1da5f94d69938db Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 12:50:54 -0800
Subject: [PATCH 08/10] Push data con matching into tacticsGetDataCons

---
 .../src/Ide/Plugin/Tactic/GHC.hs                |  8 ++++++--
 .../Tactic/LanguageServer/TacticProviders.hs    | 17 ++++-------------
 2 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index f385d6085a..e5644cebae 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -30,6 +30,7 @@ import           Type
 import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
 import           Unique
 import           Var
+import Data.Functor ((<&>))
 
 
 tcTyVar_maybe :: Type -> Maybe Var
@@ -83,8 +84,11 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons =
-  fmap (first tyConDataCons) . splitTyConApp_maybe
+tacticsGetDataCons ty =
+  splitTyConApp_maybe ty <&> \(tc, apps) ->
+    ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
+    , apps
+    )
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index ea2399e571..d082e4441f 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -22,7 +22,7 @@ import           Data.Maybe
 import           Data.Monoid
 import qualified Data.Text as T
 import           Data.Traversable
-import           DataCon (dataConName, dataConCannotMatch)
+import           DataCon (dataConName)
 import           Development.IDE.GHC.Compat
 import           GHC.Generics
 import           GHC.LanguageExtensions.Type (Extension (LambdaCase))
@@ -80,7 +80,9 @@ commandProvider UseDataCon =
     requireFeature FeatureUseDataCon $
       filterTypeProjection
           ( guardLength (<= cfg_max_use_ctor_actions cfg)
-          . useCtorFilter
+          . fromMaybe []
+          . fmap fst
+          . tacticsGetDataCons
           ) $ \dcon ->
         provide UseDataCon
           . T.pack
@@ -230,14 +232,3 @@ destructFilter :: Type -> Type -> Bool
 destructFilter _ (algebraicTyCon -> Just _) = True
 destructFilter _ _                          = False
 
-
-------------------------------------------------------------------------------
--- | Only show data cons in "Use constructor" if they can unify with the goal
-useCtorFilter :: Type -> [DataCon]
-useCtorFilter ty
-  | Just (dcs, apps) <- tacticsGetDataCons ty = do
-      dc <- dcs
-      guard $ not $ dataConCannotMatch apps dc
-      pure dc
-useCtorFilter _ = []
-

From 4a5e7b6fb450d5f2cd691816e0c18002a5bab2e4 Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 13:43:03 -0800
Subject: [PATCH 09/10] Implement a refine tactic for Reed

---
 .../src/Ide/Plugin/Tactic.hs                  |  1 +
 .../src/Ide/Plugin/Tactic/FeatureSet.hs       |  4 +++-
 .../src/Ide/Plugin/Tactic/GHC.hs              |  3 ++-
 .../Tactic/LanguageServer/TacticProviders.hs  |  4 ++++
 .../src/Ide/Plugin/Tactic/Tactics.hs          | 24 +++++++++++++++++++
 .../src/Ide/Plugin/Tactic/TestTypes.hs        |  2 ++
 plugins/hls-tactics-plugin/test/GoldenSpec.hs | 11 +++++++++
 .../test/golden/RefineCon.hs                  |  3 +++
 .../test/golden/RefineCon.hs.expected         |  3 +++
 .../test/golden/RefineGADT.hs                 |  9 +++++++
 .../test/golden/RefineGADT.hs.expected        |  9 +++++++
 .../test/golden/RefineIntro.hs                |  2 ++
 .../test/golden/RefineIntro.hs.expected       |  2 ++
 .../test/golden/RefineReader.hs               |  5 ++++
 .../test/golden/RefineReader.hs.expected      |  5 ++++
 15 files changed, 85 insertions(+), 2 deletions(-)
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineCon.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineGADT.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineIntro.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineReader.hs
 create mode 100644 plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
index 011315dd8b..a936838f0a 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic.hs
@@ -144,6 +144,7 @@ mkWorkspaceEdits
     -> Either ResponseError (Maybe WorkspaceEdit)
 mkWorkspaceEdits span dflags ccs uri pm rtr = do
   for_ (rtr_other_solns rtr) $ traceMX "other solution"
+  traceMX "solution" $ rtr_extract rtr
   let g = graftHole (RealSrcSpan span) rtr
       response = transform dflags ccs uri g pm
    in case response of
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
index 394e688f73..ce2901b7a6 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
@@ -21,7 +21,9 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = FeatureUseDataCon
+data Feature
+  = FeatureUseDataCon
+  | FeatureRefineHole
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index e5644cebae..549dd5f4b1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -84,11 +84,12 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty =
+tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
   splitTyConApp_maybe ty <&> \(tc, apps) ->
     ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
     , apps
     )
+tacticsGetDataCons _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index d082e4441f..3ebf91de23 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -51,6 +51,7 @@ commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic UseDataCon             = userSplit
+commandTactic Refine                 = const refine
 
 
 ------------------------------------------------------------------------------
@@ -89,6 +90,9 @@ commandProvider UseDataCon =
           . occNameString
           . occName
           $ dataConName dcon
+commandProvider Refine =
+  requireFeature FeatureRefineHole $
+    provide Refine ""
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
index c85b4104f3..b388a4cee9 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs
@@ -207,6 +207,19 @@ splitAuto = requireConcreteHole $ tracing "split(auto)" $ do
             splitDataCon dc
 
 
+------------------------------------------------------------------------------
+-- | Like 'split', but only works if there is a single matching data
+-- constructor for the goal.
+splitSingle :: TacticsM ()
+splitSingle = tracing "splitSingle" $ do
+  jdg <- goal
+  let g = jGoal jdg
+  case tacticsGetDataCons $ unCType g of
+    Just ([dc], _) -> do
+      splitDataCon dc
+    _ -> throwError $ GoalMismatch "splitSingle" g
+
+
 ------------------------------------------------------------------------------
 -- | Allow the given tactic to proceed if and only if it introduces holes that
 -- have a different goal than current goal.
@@ -268,6 +281,17 @@ localTactic t f = do
     runStateT (unTacticT t) $ f jdg
 
 
+refine :: TacticsM ()
+refine = go 3
+  where
+    go 0 = pure ()
+    go n = do
+      let try_that_doesnt_suck t = commit t $ pure ()
+      try_that_doesnt_suck intros
+      try_that_doesnt_suck splitSingle
+      go $ n - 1
+
+
 auto' :: Int -> TacticsM ()
 auto' 0 = throwError NoProgress
 auto' n = do
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index 219731fbc2..638fda6311 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -20,6 +20,7 @@ data TacticCommand
   | DestructLambdaCase
   | HomomorphismLambdaCase
   | UseDataCon
+  | Refine
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -31,6 +32,7 @@ tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
 tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
+tacticTitle Refine _                 = "Refine hole"
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index 5e3fd4b9e5..e7a263814f 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -105,6 +105,17 @@ spec = do
       useTest "Left"  "UseConLeft.hs"  2 8
       useTest "Right" "UseConRight.hs" 2 8
 
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/refine/"'
+  describe "refine" $ do
+    let refineTest = mkGoldenTest allFeatures Refine ""
+    describe "golden" $ do
+      refineTest "RefineIntro.hs"  2 8
+      refineTest "RefineCon.hs"    2 8
+      refineTest "RefineReader.hs" 4 8
+      refineTest "RefineGADT.hs"   8 8
+
+
   describe "golden tests" $ do
     let autoTest = mkGoldenTest allFeatures Auto ""
 
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs
new file mode 100644
index 0000000000..dc611f6e93
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs
@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected
new file mode 100644
index 0000000000..e6e43592a4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineCon.hs.expected
@@ -0,0 +1,3 @@
+test :: ((), (b, c), d)
+test = ((), (_, _), _)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs
new file mode 100644
index 0000000000..04fa6ee1a4
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  One :: (b -> Int) -> GADT Int
+  Two :: GADT Bool
+
+test :: z -> GADT Int
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected
new file mode 100644
index 0000000000..c3c463b2c8
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineGADT.hs.expected
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+data GADT a where
+  One :: (b -> Int) -> GADT Int
+  Two :: GADT Bool
+
+test :: z -> GADT Int
+test z = One (\ b -> _)
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs
new file mode 100644
index 0000000000..afe7524957
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs
@@ -0,0 +1,2 @@
+test :: a -> Either a b
+test = _
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected
new file mode 100644
index 0000000000..4cacf9e17c
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineIntro.hs.expected
@@ -0,0 +1,2 @@
+test :: a -> Either a b
+test a = _
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineReader.hs b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs
new file mode 100644
index 0000000000..cf4df0cd91
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs
@@ -0,0 +1,5 @@
+newtype Reader r a = Reader (r -> a)
+
+test :: b -> Reader r a
+test = _
+
diff --git a/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected
new file mode 100644
index 0000000000..570bb31c33
--- /dev/null
+++ b/plugins/hls-tactics-plugin/test/golden/RefineReader.hs.expected
@@ -0,0 +1,5 @@
+newtype Reader r a = Reader (r -> a)
+
+test :: b -> Reader r a
+test b = Reader (\ r -> _)
+

From 4fbf5d2937e051ed16804964d9def858e8e3ce8a Mon Sep 17 00:00:00 2001
From: Sandy Maguire <sandy@sandymaguire.me>
Date: Sun, 28 Feb 2021 13:43:03 -0800
Subject: [PATCH 10/10] Implement a refine tactic for Reed

---
 .../src/Ide/Plugin/Tactic/FeatureSet.hs               |  4 +++-
 .../hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs   |  3 ++-
 .../Plugin/Tactic/LanguageServer/TacticProviders.hs   |  4 ++++
 .../src/Ide/Plugin/Tactic/TestTypes.hs                |  2 ++
 plugins/hls-tactics-plugin/test/GoldenSpec.hs         | 11 +++++++++++
 5 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
index 394e688f73..ce2901b7a6 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/FeatureSet.hs
@@ -21,7 +21,9 @@ import qualified Data.Text  as T
 ------------------------------------------------------------------------------
 -- | All the available features. A 'FeatureSet' describes the ones currently
 -- available to the user.
-data Feature = FeatureUseDataCon
+data Feature
+  = FeatureUseDataCon
+  | FeatureRefineHole
   deriving (Eq, Ord, Show, Read, Enum, Bounded)
 
 
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
index e5644cebae..549dd5f4b1 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/GHC.hs
@@ -84,11 +84,12 @@ tacticsThetaTy (tcSplitSigmaTy -> (_, theta,  _)) = theta
 ------------------------------------------------------------------------------
 -- | Get the data cons of a type, if it has any.
 tacticsGetDataCons :: Type -> Maybe ([DataCon], [Type])
-tacticsGetDataCons ty =
+tacticsGetDataCons ty | Just _ <- algebraicTyCon ty =
   splitTyConApp_maybe ty <&> \(tc, apps) ->
     ( filter (not . dataConCannotMatch apps) $ tyConDataCons tc
     , apps
     )
+tacticsGetDataCons _ = Nothing
 
 ------------------------------------------------------------------------------
 -- | Instantiate all of the quantified type variables in a type with fresh
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
index d082e4441f..3ebf91de23 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer/TacticProviders.hs
@@ -51,6 +51,7 @@ commandTactic Homomorphism           = useNameFromHypothesis homo
 commandTactic DestructLambdaCase     = const destructLambdaCase
 commandTactic HomomorphismLambdaCase = const homoLambdaCase
 commandTactic UseDataCon             = userSplit
+commandTactic Refine                 = const refine
 
 
 ------------------------------------------------------------------------------
@@ -89,6 +90,9 @@ commandProvider UseDataCon =
           . occNameString
           . occName
           $ dataConName dcon
+commandProvider Refine =
+  requireFeature FeatureRefineHole $
+    provide Refine ""
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
index 219731fbc2..638fda6311 100644
--- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
+++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/TestTypes.hs
@@ -20,6 +20,7 @@ data TacticCommand
   | DestructLambdaCase
   | HomomorphismLambdaCase
   | UseDataCon
+  | Refine
   deriving (Eq, Ord, Show, Enum, Bounded)
 
 -- | Generate a title for the command.
@@ -31,6 +32,7 @@ tacticTitle Homomorphism var         = "Homomorphic case split on " <> var
 tacticTitle DestructLambdaCase _     = "Lambda case split"
 tacticTitle HomomorphismLambdaCase _ = "Homomorphic lambda case split"
 tacticTitle UseDataCon dcon          = "Use constructor " <> dcon
+tacticTitle Refine _                 = "Refine hole"
 
 
 ------------------------------------------------------------------------------
diff --git a/plugins/hls-tactics-plugin/test/GoldenSpec.hs b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
index 5e3fd4b9e5..e7a263814f 100644
--- a/plugins/hls-tactics-plugin/test/GoldenSpec.hs
+++ b/plugins/hls-tactics-plugin/test/GoldenSpec.hs
@@ -105,6 +105,17 @@ spec = do
       useTest "Left"  "UseConLeft.hs"  2 8
       useTest "Right" "UseConRight.hs" 2 8
 
+  -- test via:
+  -- stack test hls-tactics-plugin --test-arguments '--match "Golden/refine/"'
+  describe "refine" $ do
+    let refineTest = mkGoldenTest allFeatures Refine ""
+    describe "golden" $ do
+      refineTest "RefineIntro.hs"  2 8
+      refineTest "RefineCon.hs"    2 8
+      refineTest "RefineReader.hs" 4 8
+      refineTest "RefineGADT.hs"   8 8
+
+
   describe "golden tests" $ do
     let autoTest = mkGoldenTest allFeatures Auto ""