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/Context.hs

@@ -3,19 +3,21 @@
 
 module Ide.Plugin.Tactic.Context where
 
-import Bag
-import Control.Arrow
-import Control.Monad.Reader
-import Development.IDE.GHC.Compat
-import Ide.Plugin.Tactic.Types
-import OccName
-import TcRnTypes
-import Ide.Plugin.Tactic.GHC (tacticsThetaTy)
-import Ide.Plugin.Tactic.Machinery (methodHypothesis)
-import Data.Maybe (mapMaybe)
-import Data.List
-import TcType (substTy, tcSplitSigmaTy)
-import Unify (tcUnifyTy)
+import           Bag
+import           Control.Arrow
+import           Control.Monad.Reader
+import           Data.List
+import           Data.Maybe (mapMaybe)
+import           Data.Set (Set)
+import qualified Data.Set as S
+import           Development.IDE.GHC.Compat
+import           Ide.Plugin.Tactic.GHC (tacticsThetaTy)
+import           Ide.Plugin.Tactic.Machinery (methodHypothesis)
+import           Ide.Plugin.Tactic.Types
+import           OccName
+import           TcRnTypes
+import           TcType (substTy, tcSplitSigmaTy)
+import           Unify (tcUnifyTy)
 
 
 mkContext :: [(OccName, CType)] -> TcGblEnv -> Context
@@ -33,7 +35,8 @@ mkContext locals tcg = Context
 -- | Find all of the class methods that exist from the givens in the context.
 contextMethodHypothesis :: Context -> [(OccName, CType)]
 contextMethodHypothesis ctx
-  = join
+  = excludeForbiddenMethods
+  . join
   . concatMap
       ( mapMaybe methodHypothesis
       . tacticsThetaTy
@@ -44,6 +47,20 @@ contextMethodHypothesis ctx
   $ ctxDefiningFuncs ctx
 
 
+------------------------------------------------------------------------------
+-- | Many operations are defined in typeclasses for performance reasons, rather
+-- than being a true part of the class. This function filters out those, in
+-- order to keep our hypothesis space small.
+excludeForbiddenMethods :: [(OccName, CType)] -> [(OccName, CType)]
+excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods  . fst)
+  where
+    forbiddenMethods :: Set OccName
+    forbiddenMethods = S.map mkVarOcc $ S.fromList
+      [ -- monadfail
+        "fail"
+      ]
+
+
 ------------------------------------------------------------------------------
 -- | Given the name of a function that exists in 'ctxDefiningFuncs', get its
 -- theta type.

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

@@ -71,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)
         unused_topvals = nub $ join $ join $ toList $ _jPositionMaps jdg
         tacticState =
           defaultTacticState

test/functional/Tactic.hs

@@ -9,16 +9,20 @@ module Tactic
 where
 
 import           Control.Applicative.Combinators ( skipManyTill )
+import           Control.Lens hiding ((<.>))
 import           Control.Monad (unless)
 import           Control.Monad.IO.Class
+import           Data.Aeson
+import           Data.Either (isLeft)
 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.Types (ExecuteCommandParams(ExecuteCommandParams), ClientMethod (..), Command, ExecuteCommandResponse, ResponseMessage (..), ApplyWorkspaceEditRequest, Position(..) , Range(..) , CAResult(..) , CodeAction(..))
+import           Language.Haskell.LSP.Types.Lens hiding (id, capabilities, message, executeCommand, applyEdit, rename)
 import           System.Directory (doesFileExist)
 import           System.FilePath
 import           Test.Hls.Util
@@ -110,6 +114,7 @@ tests = testGroup
   , ignoreTestBecause "It is unreliable in circleci builds"
       $ goldenTest "GoldenApplicativeThen.hs"   2 11 Auto ""
   , goldenTest "GoldenSafeHead.hs"          2 12 Auto ""
+  , expectFail "GoldenFish.hs"              5 18 Auto ""
   ]
 
 
@@ -160,6 +165,27 @@ 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 $ unless (isLeft $ _result resp) $
+        assertFailure "didn't fail, but expected one"
+
+
 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 = _