diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs index 0a22255e60..5ce8605e70 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs +++ b/plugins/tactics/src/Ide/Plugin/Tactic/Auto.hs @@ -1,12 +1,13 @@ 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) ------------------------------------------------------------------------------ @@ -14,9 +15,11 @@ import Ide.Plugin.Tactic.Machinery (tracing) 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) diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs index a9a56d290d..1621c36393 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Context.hs +++ b/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. diff --git a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs index 25bf3e5c62..f3e41c0061 100644 --- a/plugins/tactics/src/Ide/Plugin/Tactic/Machinery.hs +++ b/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 diff --git a/test/functional/Tactic.hs b/test/functional/Tactic.hs index 2f3b05d31a..a37474771b 100644 --- a/test/functional/Tactic.hs +++ b/test/functional/Tactic.hs @@ -9,8 +9,11 @@ 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) @@ -18,7 +21,8 @@ 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 + diff --git a/test/testdata/tactic/GoldenFish.hs b/test/testdata/tactic/GoldenFish.hs new file mode 100644 index 0000000000..ce38700b58 --- /dev/null +++ b/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 = _