Fix a bug in tactics preventing split of split (#520)

The `auto` tactic attempts to prune unhelpful branches in order to avoid an exponential blowup of search space. On one these optimizations is to not build a data constructor if it doesn't result in new types to solve. For example, we're trying to avoid the following pathological example:

```haskell
data Tree a = Leaf a | Branch (Tree a) (Tree a)

-- given the following hole:
pureTree :: a -> Tree a
pureTree a = _

-- we DO NOT want to fill it with
pureTree a = Branch _ _
```

The reasoning here is that both goals in `Branch _ _` have type `Tree a`, which is already the type we're trying to solve, so introducing `Branch` doesn't make any progress.

This check is performed in the `splitAuto` tactic, but I got it backwards and it wasn't explicitly tested for. The only code which hit it was `pure @[]` --- but because `[]` doesn't have any subgoals, this hit a vacuous case and flipped the result of the bad logic. Two wrongs made a hard to find bug.

This PR:

1. Fixes the reversed logic in `splitAuto`
2. Has a special case for nullary data constructors, fixing the bug cause by vacuousness.
3. Adds property tests ensuring we can `auto` our way through any permutation of a tuple (which is where we originally noticed the bug)
4. Prevents `unsafeRender` from crashing when `unsafeGlobalDynFlags` is unset, such as during testing.
5. Moves tactic solution tracing into the plugin, so it won't run during tests.

Author: isovector

.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:tests --dump-logs --test-arguments="-j1"
+        no_output_timeout: 30m
+
     - store_test_results:
         path: test-results
 

hie.yaml.stack

@@ -21,9 +21,13 @@ cradle:
 
             - path: "./plugins/default/src"
               component: "haskell-language-server:exe:haskell-language-server"
+
             - path: "./plugins/tactics/src"
               component: "hls-tactics-plugin:lib:hls-tactics-plugin"
 
+            - path: "./plugins/tactics/test"
+              component: "hls-tactics-plugin:test:tests"
+
             - path: "./exe/Arguments.hs"
               component: "haskell-language-server:exe:haskell-language-server"
 

plugins/tactics/hls-tactics-plugin.cabal

@@ -75,6 +75,28 @@ library
     , syb
     , text
     , transformers
+    , deepseq
 
   default-language: Haskell2010
 
+test-suite tests
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  other-modules:
+    AutoTupleSpec
+  hs-source-dirs:
+      test
+  ghc-options: -Wall -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      QuickCheck
+    , base
+    , checkers
+    , hspec
+    , mtl
+    , hls-tactics-plugin
+    , hls-plugin-api
+    , hie-bios
+    , ghc
+    , containers
+  default-language: Haskell2010
+

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

@@ -296,8 +296,9 @@ tacticCmd tac lf state (TacticParams uri range var_name)
               pure $ (, Nothing)
                 $ Left
                 $ ResponseError InvalidRequest (T.pack $ show err) Nothing
-            Right (_, ext) -> do
-              let g = graft (RealSrcSpan span) ext
+            Right rtr -> do
+              traceMX "solns" $ rtr_other_solns rtr
+              let g = graft (RealSrcSpan span) $ rtr_extract rtr
                   response = transform dflags (clientCapabilities lf) uri g pm
               pure $ case response of
                 Right res -> (Right Null , Just (WorkspaceApplyEdit, ApplyWorkspaceEditParams res))

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

@@ -1,3 +1,7 @@
+{-# LANGUAGE BangPatterns     #-}
+{-# LANGUAGE CPP              #-}
+{-# LANGUAGE TypeApplications #-}
+
 module Ide.Plugin.Tactic.Debug
   ( unsafeRender
   , unsafeRender'
@@ -9,17 +13,36 @@ module Ide.Plugin.Tactic.Debug
   , traceMX
   ) where
 
+import Control.DeepSeq
+import Control.Exception
 import Debug.Trace
 import DynFlags (unsafeGlobalDynFlags)
 import Outputable hiding ((<>))
+import System.IO.Unsafe (unsafePerformIO)
+
+#if __GLASGOW_HASKELL__ >= 808
+import PlainPanic (PlainGhcException)
+type GHC_EXCEPTION = PlainGhcException
+#else
+import Panic (GhcException)
+type GHC_EXCEPTION = GhcException
+#endif
+
 
 ------------------------------------------------------------------------------
 -- | Print something
 unsafeRender :: Outputable a => a -> String
 unsafeRender = unsafeRender' . ppr
 
+
 unsafeRender' :: SDoc -> String
-unsafeRender' = showSDoc unsafeGlobalDynFlags
+unsafeRender' sdoc = unsafePerformIO $ do
+  let z = showSDoc unsafeGlobalDynFlags sdoc
+  -- We might not have unsafeGlobalDynFlags (like during testing), in which
+  -- case GHC panics. Instead of crashing, let's just fail to print.
+  !res <- try @GHC_EXCEPTION $ evaluate $ deepseq z z
+  pure $ either (const "<unsafeRender'>") id res
+{-# NOINLINE unsafeRender' #-}
 
 traceMX :: (Monad m, Show a) => String -> a -> m ()
 traceMX str a = traceM $ mappend ("!!!" <> str <> ": ") $ show a

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

@@ -63,7 +63,7 @@ runTactic
     :: Context
     -> Judgement
     -> TacticsM ()       -- ^ Tactic to use
-    -> Either [TacticError] (Trace, LHsExpr GhcPs)
+    -> Either [TacticError] RunTacticResults
 runTactic ctx jdg t =
     let skolems = tyCoVarsOfTypeWellScoped $ unCType $ jGoal jdg
         tacticState = defaultTacticState { ts_skolems = skolems }
@@ -73,16 +73,15 @@ runTactic ctx jdg t =
           $ runTacticT t jdg tacticState of
       (errs, []) -> Left $ take 50 $ errs
       (_, fmap assoc23 -> solns) -> do
-        let sorted = sortBy (comparing $ Down . uncurry scoreSolution . snd) $ solns
-        -- TODO(sandy): remove this trace sometime
-        traceM
-            $ mappend "!!!solns: "
-            $ intercalate "\n"
-            $ reverse
-            $ take 5
-            $ fmap (show . fst) sorted
+        let sorted =
+              sortBy (comparing $ Down . uncurry scoreSolution . snd) solns
         case sorted of
-          (res : _) -> Right $ fst res
+          (((tr, ext), _) : _) ->
+            Right
+              . RunTacticResults tr ext
+              . reverse
+              . fmap fst
+              $ take 5 sorted
           -- guaranteed to not be empty
           _ -> Left []
 

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

@@ -217,9 +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) $ fmap jGoal jdgs of
-              False -> Nothing
-              True  -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
+            case null jdgs || any (/= jGoal jdg) (fmap jGoal jdgs) of
+              True  -> Nothing
+              False -> Just $ UnhelpfulSplit $ nameOccName $ dataConName dc
 
 
 ------------------------------------------------------------------------------

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

@@ -219,3 +219,12 @@ 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
 
+
+------------------------------------------------------------------------------
+-- | The results of 'Ide.Plugin.Tactic.Machinery.runTactic'
+data RunTacticResults = RunTacticResults
+  { rtr_trace       :: Trace
+  , rtr_extract     :: LHsExpr GhcPs
+  , rtr_other_solns :: [(Trace, LHsExpr GhcPs)]
+  } deriving Show
+

plugins/tactics/test/AutoTupleSpec.hs

@@ -0,0 +1,58 @@
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
+module AutoTupleSpec where
+
+import           Data.Either (isRight)
+import qualified Data.Map as M
+import           Ide.Plugin.Tactic.Debug
+import           Ide.Plugin.Tactic.Judgements (mkFirstJudgement)
+import           Ide.Plugin.Tactic.Machinery
+import           Ide.Plugin.Tactic.Tactics (auto')
+import           Ide.Plugin.Tactic.Types
+import           OccName (mkVarOcc)
+import           Test.Hspec
+import           Test.QuickCheck
+import           Type (mkTyVarTy)
+import           TysPrim (alphaTyVars)
+import           TysWiredIn (mkBoxedTupleTy)
+
+
+instance Show Type where
+  show = unsafeRender
+
+
+spec :: Spec
+spec = describe "auto for tuple" $ do
+  it "should always be able to discover an auto solution" $ do
+    property $ do
+      -- Pick some number of variables
+      n <- choose (1, 7)
+      let vars = fmap mkTyVarTy $ take n alphaTyVars
+      -- Pick a random ordering
+      in_vars  <- shuffle vars
+      -- Randomly associate them into tuple types
+      in_type  <- mkBoxedTupleTy
+                . fmap mkBoxedTupleTy
+              <$> randomGroups in_vars
+      out_type <- mkBoxedTupleTy
+                . fmap mkBoxedTupleTy
+              <$> randomGroups vars
+      pure $
+          -- We should always be able to find a solution
+          runTactic
+            (Context [] [])
+            (mkFirstJudgement
+              (M.singleton (mkVarOcc "x") $ CType in_type)
+              True
+              mempty
+              out_type)
+            (auto' $ n * 2) `shouldSatisfy` isRight
+
+
+randomGroups :: [a] -> Gen [[a]]
+randomGroups [] = pure []
+randomGroups as = do
+  n <- choose (1, length as)
+  (:) <$> pure (take n as)
+      <*> randomGroups (drop n as)
+

plugins/tactics/test/Main.hs

@@ -0,0 +1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover -optF --module-name=Main #-}

test/functional/Tactic.hs

@@ -101,6 +101,7 @@ tests = testGroup
   , goldenTest "GoldenGADTDestruct.hs"      7 17 Destruct "gadt"
   , goldenTest "GoldenGADTAuto.hs"          7 13 Auto ""
   , goldenTest "GoldenSwapMany.hs"          2 12 Auto ""
+  , goldenTest "GoldenBigTuple.hs"          4 12 Auto ""
   ]
 
 

test/testdata/tactic/GoldenBigTuple.hs

@@ -0,0 +1,4 @@
+-- There used to be a bug where we were unable to perform a nested split. The
+-- more serious regression test of this is 'AutoTupleSpec'.
+bigTuple :: (a, b, c, d) -> (a, b, (c, d))
+bigTuple = _

test/testdata/tactic/GoldenBigTuple.hs.expected

@@ -0,0 +1,4 @@
+-- There used to be a bug where we were unable to perform a nested split. The
+-- more serious regression test of this is 'AutoTupleSpec'.
+bigTuple :: (a, b, c, d) -> (a, b, (c, d))
+bigTuple = (\ pabcd -> case pabcd of { (a, b, c, d) -> (a, b, (c, d)) })