Discover skolems in the hypothesis, not just goal

plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs

@@ -1,22 +1,25 @@
 module Ide.Plugin.Tactic.Auto where
 
+import Control.Monad.State (gets)
 import Ide.Plugin.Tactic.Context
 import Ide.Plugin.Tactic.Judgements
 import Ide.Plugin.Tactic.KnownStrategies
+import Ide.Plugin.Tactic.Machinery (tracing)
 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 = do
   jdg <- goal
+  skolems <- gets ts_skolems
   current <- getCurrentDefinitions
   traceMX "goal" jdg
   traceMX "ctx" current
+  traceMX "skolems" skolems
   commit knownStrategies
     . tracing "auto"
     . localTactic (auto' 4)

plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs

@@ -27,9 +27,10 @@ import           Control.Monad.State.Class (gets, modify)
 import           Control.Monad.State.Strict (StateT (..))
 import           Data.Coerce
 import           Data.Either
+import           Data.Foldable
 import           Data.Functor ((<&>))
 import           Data.Generics (mkQ, everything, gcount)
-import           Data.List (sortBy)
+import           Data.List (nub, sortBy)
 import           Data.Ord (comparing, Down(..))
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
@@ -70,7 +71,10 @@ runTactic
     -> TacticsM ()       -- ^ Tactic to use
     -> Either [TacticError] RunTacticResults
 runTactic ctx jdg t =
-    let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
+    let skolems = nub
+                $ foldMap (tyCoVarsOfTypeWellScoped . unCType)
+                $ jGoal jdg
+                : (toList $ jHypothesis jdg)
         tacticState = defaultTacticState { ts_skolems = skolems }
     in case partitionEithers
           . flip runReader ctx

test/functional/Tactic.hs

@@ -8,22 +8,26 @@ module Tactic
   )
 where
 
+import Control.Lens hiding ((<.>))
+import Language.Haskell.LSP.Types.Lens hiding
+  (id, capabilities, message, executeCommand, applyEdit, rename)
 import           Control.Applicative.Combinators ( skipManyTill )
+import           Control.Monad (unless)
 import           Control.Monad.IO.Class
 import           Data.Foldable
 import           Data.Maybe
 import           Data.Text (Text)
 import qualified Data.Text as T
 import qualified Data.Text.IO as T
 import           Ide.Plugin.Tactic.TestTypes
-import           Language.Haskell.LSP.Test
-import           Language.Haskell.LSP.Types (ApplyWorkspaceEditRequest, Position(..) , Range(..) , CAResult(..) , CodeAction(..))
+import Language.Haskell.LSP.Test
+import           Language.Haskell.LSP.Types (ExecuteCommandParams(ExecuteCommandParams), ClientMethod (..), Command, ExecuteCommandResponse, ResponseMessage (..), ApplyWorkspaceEditRequest, Position(..) , Range(..) , CAResult(..) , CodeAction(..))
+import           System.Directory (doesFileExist)
+import           System.FilePath
 import           Test.Hls.Util
 import           Test.Tasty
 import           Test.Tasty.HUnit
-import           System.FilePath
-import System.Directory (doesFileExist)
-import Control.Monad (unless)
+import Data.Aeson
 
 
 ------------------------------------------------------------------------------
@@ -107,6 +111,7 @@ tests = testGroup
   , goldenTest "GoldenShowMapChar.hs"       2 8  Auto ""
   , goldenTest "GoldenSuperclass.hs"        7 8  Auto ""
   , goldenTest "GoldenApplicativeThen.hs"   2 11 Auto ""
+  , expectFail "GoldenFish.hs"              5 18 Auto ""
   ]
 
 
@@ -157,6 +162,30 @@ goldenTest input line col tc occ =
       liftIO $ edited @?= expected
 
 
+expectFail :: FilePath -> Int -> Int -> TacticCommand -> Text -> TestTree
+expectFail input line col tc occ =
+  testCase (input <> " (golden)") $ do
+    runSession hlsCommand fullCaps tacticPath $ do
+      doc <- openDoc input "haskell"
+      _ <- waitForDiagnostics
+      actions <- getCodeActions doc $ pointRange line col
+      Just (CACodeAction (CodeAction {_command = Just c}))
+        <- pure $ find ((== Just (tacticTitle tc occ)) . codeActionTitle) actions
+      resp <- executeCommandWithResp c
+      liftIO $
+        either
+          (const $ pure ())
+          (const $ assertFailure "didn't fail, but expected one")
+            $ _result resp
+
+
 tacticPath :: FilePath
 tacticPath = "test/testdata/tactic"
 
+
+executeCommandWithResp :: Command -> Session ExecuteCommandResponse
+executeCommandWithResp cmd = do
+  let args = decode $ encode $ fromJust $ cmd ^. arguments
+      execParams = ExecuteCommandParams (cmd ^. command) args Nothing
+  request WorkspaceExecuteCommand execParams
+

test/testdata/tactic/GoldenFish.hs

@@ -0,0 +1,5 @@
+-- There was an old bug where we would only pull skolems from the hole, rather
+-- than the entire hypothesis. Because of this, the 'b' here would be
+-- considered a univar, which could then be unified with the skolem 'c'.
+fish :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
+fish amb bmc a = _