Solver: Improve error message by finding a minimal conflict set (issue …

…haskell#5647).

This commit improves the error message in the case where the solver finds no
solution after an exhaustive search.  Previously, cabal generated the error
message by rerunning the solver and having it prefer goals from the final
conflict set, so that the error message only mentioned conflicts between
packages from the final conflict set.  Conflicts relating to the final conflict
set are more likely to be relevant, because the conflict set contains all
variables that are involved in one conflict that makes the dependencies
unsatisfiable.  However, the conflict set can also include variables that led to
some conflicts but aren't relevant to the main conflict.  This commit improves
the error message further by first trying to reduce the size of the conflict
set.

The current algorithm for reducing the conflict set simply reruns the solver
with different goal orders, so it has some downsides:

- Reducing the conflict set can be slow.  It is also possible for the solver to
  reach the backjump limit on a rerun, even though the first run completed.  In
  that case, it uses the original conflict set.

- The function can fail to remove some unnecessary variables from the conflict
  set.  In the worst case, it returns the original conflict set.

I tested the feature on the example in
https://www.reddit.com/r/haskell/comments/9rmh9s/how_to_read_cabal_solver_failure_output/
and haskell#5647.  Both runs used the command
"cabal install --only-dependencies --enable-tests --force-reinstalls --index-state=2018-10-26T20:30:16Z".

Before:

    Resolving dependencies...
    cabal: Could not resolve dependencies:
    [__0] trying: opaleye-0.6.7003.0 (user goal)
    [__1] rejecting: opaleye:!test (constraint from config file, command line
    flag, or user target requires opposite flag selection)
    [__1] trying: opaleye:*test
    [__2] trying: dotenv-0.6.0.3 (dependency of opaleye *test)
    [__3] trying: transformers-0.5.5.0/installed-0.5... (dependency of opaleye)
    [__4] next goal: contravariant (dependency of opaleye)
    [__4] rejecting: contravariant-1.5 (conflict: opaleye => contravariant>=1.2 &&
    <1.5)
    [__4] rejecting: contravariant-1.4.1, contravariant-1.4 (conflict:
    transformers => base==4.12.0.0/installed-4.1..., contravariant => base<4.12)
    [__4] rejecting: contravariant-1.3.3, contravariant-1.3.2,
    contravariant-1.3.1.1, contravariant-1.3.1, contravariant-1.3,
    contravariant-1.2.2.1, contravariant-1.2.2, contravariant-1.2.1,
    contravariant-1.2.0.1, contravariant-1.2 (conflict:
    transformers==0.5.5.0/installed-0.5..., contravariant => transformers>=0.2 &&
    <0.5)
    [__4] rejecting: contravariant-1.1, contravariant-1.0, contravariant-0.6.1.1,
    contravariant-0.6.1, contravariant-0.6, contravariant-0.5.2,
    contravariant-0.5.1, contravariant-0.5, contravariant-0.4.4,
    contravariant-0.4.3, contravariant-0.4.1, contravariant-0.4,
    contravariant-0.3, contravariant-0.2.0.2, contravariant-0.2.0.1,
    contravariant-0.2, contravariant-0.1.3, contravariant-0.1.2.1,
    contravariant-0.1.2, contravariant-0.1.1, contravariant-0.1.0.1,
    contravariant-0.1.0 (conflict: opaleye => contravariant>=1.2 && <1.5)
    [__4] fail (backjumping, conflict set: contravariant, opaleye, transformers)
    After searching the rest of the dependency tree exhaustively, these were the
    goals I've had most trouble fulfilling: transformers, contravariant, opaleye,
    base, dotenv, opaleye:test

After:

    Resolving dependencies...
    cabal: Could not resolve dependencies:
    [__0] trying: opaleye-0.6.7003.0 (user goal)
    [__1] trying: transformers-0.5.5.0/installed-0.5... (dependency of opaleye)
    [__2] next goal: contravariant (dependency of opaleye)
    [__2] rejecting: contravariant-1.5 (conflict: opaleye => contravariant>=1.2 &&
    <1.5)
    [__2] rejecting: contravariant-1.4.1, contravariant-1.4 (conflict:
    transformers => base==4.12.0.0/installed-4.1..., contravariant => base<4.12)
    [__2] rejecting: contravariant-1.3.3, contravariant-1.3.2,
    contravariant-1.3.1.1, contravariant-1.3.1, contravariant-1.3,
    contravariant-1.2.2.1, contravariant-1.2.2, contravariant-1.2.1,
    contravariant-1.2.0.1, contravariant-1.2 (conflict:
    transformers==0.5.5.0/installed-0.5..., contravariant => transformers>=0.2 &&
    <0.5)
    [__2] rejecting: contravariant-1.1, contravariant-1.0, contravariant-0.6.1.1,
    contravariant-0.6.1, contravariant-0.6, contravariant-0.5.2,
    contravariant-0.5.1, contravariant-0.5, contravariant-0.4.4,
    contravariant-0.4.3, contravariant-0.4.1, contravariant-0.4,
    contravariant-0.3, contravariant-0.2.0.2, contravariant-0.2.0.1,
    contravariant-0.2, contravariant-0.1.3, contravariant-0.1.2.1,
    contravariant-0.1.2, contravariant-0.1.1, contravariant-0.1.0.1,
    contravariant-0.1.0 (conflict: opaleye => contravariant>=1.2 && <1.5)
    [__2] fail (backjumping, conflict set: contravariant, opaleye, transformers)
    After searching the rest of the dependency tree exhaustively, these were the
    goals I've had most trouble fulfilling: base, opaleye, contravariant,
    transformers

In this case, the feature found a minimal conflict set, {base, opaleye,
contravariant, transformers}, by removing dotenv and opaleye:test from the
original conflict set.

cabal-install/Distribution/Solver/Modular.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Distribution.Solver.Modular
          ( modularResolver, SolverConfig(..), PruneAfterFirstSuccess(..) ) where
@@ -15,7 +16,7 @@ import Prelude ()
 import Distribution.Solver.Compat.Prelude
 
 import qualified Data.Map as M
-import Data.Set (Set)
+import Data.Set (Set, isSubsetOf)
 import Data.Ord
 import Distribution.Compat.Graph
          ( IsNode(..) )
@@ -132,10 +133,27 @@ solve' sc cinfo idx pkgConfigDB pprefs gcs pns =
                    -> Maybe Int
                    -> SolverFailure
                    -> RetryLog String String (Assignment, RevDepMap)
-    createErrorMsg verbosity mbj failure@(ExhaustiveSearch cs _) =
-        fromProgress $ Fail $ rerunSolverForErrorMsg cs ++ finalErrorMsg verbosity mbj failure
+    createErrorMsg verbosity mbj failure@(ExhaustiveSearch cs cm) =
+        continueWith ("Found no solution after exhaustively searching the "
+                       ++ "dependency tree. Rerunning the dependency solver "
+                       ++ "to minimize the conflict set ({"
+                       ++ showConflictSet cs ++ "}).") $
+        retry (tryToMinimizeConflictSet (runSolver printFullLog) sc cs cm) $
+            \case
+               ExhaustiveSearch cs' cm' ->
+                   fromProgress $ Fail $
+                       rerunSolverForErrorMsg cs'
+                    ++ finalErrorMsg verbosity mbj (ExhaustiveSearch cs' cm')
+               BackjumpLimitReached ->
+                   fromProgress $ Fail $
+                       "Reached backjump limit while trying to minimize the "
+                    ++ "conflict set to create a better error message. "
+                    ++ "Original error message:\n"
+                    ++ rerunSolverForErrorMsg cs
+                    ++ finalErrorMsg verbosity mbj failure
     createErrorMsg verbosity mbj failure@BackjumpLimitReached    =
-        continueWith ("Backjump limit reached. Rerunning dependency solver to generate "
+        continueWith
+             ("Backjump limit reached. Rerunning dependency solver to generate "
               ++ "a final conflict set for the search tree containing the "
               ++ "first backjump.") $
         retry (runSolver printFullLog sc { pruneAfterFirstSuccess = PruneAfterFirstSuccess True }) $
@@ -147,8 +165,8 @@ solve' sc cinfo idx pkgConfigDB pprefs gcs pns =
                    -- This case is possible when the number of goals involved in
                    -- conflicts is greater than the backjump limit.
                    fromProgress $ Fail $ finalErrorMsg verbosity mbj failure
-                              ++ "Failed to generate a summarized dependency solver "
-                              ++ "log due to low backjump limit."
+                    ++ "Failed to generate a summarized dependency solver "
+                    ++ "log due to low backjump limit."
 
     rerunSolverForErrorMsg :: ConflictSet -> String
     rerunSolverForErrorMsg cs =
@@ -168,17 +186,122 @@ solve' sc cinfo idx pkgConfigDB pprefs gcs pns =
     messages :: Progress step fail done -> [step]
     messages = foldProgress (:) (const []) (const [])
 
+-- | Try to remove variables from the given conflict set to create a minimal
+-- conflict set.
+--
+-- Minimal means that no proper subset of the conflict set is also a conflict
+-- set, though there may be other possible conflict sets with fewer variables.
+-- This function minimizes the input by trying to remove one variable at a time.
+-- It only makes one pass over the variables, so it runs the solver at most N
+-- times when given a conflict set of size N. Only one pass is necessary,
+-- because every superset of a conflict set is also a conflict set, meaning that
+-- failing to remove variable X from a conflict set in one step means that X
+-- cannot be removed from any subset of that conflict set in a subsequent step.
+--
+-- Example steps:
+--
+-- Start with {A, B, C}.
+-- Try to remove A from {A, B, C} and fail.
+-- Try to remove B from {A, B, C} and succeed.
+-- Try to remove C from {A, C} and fail.
+-- Return {A, C}
+--
+-- This function can fail for two reasons:
+--
+-- 1. The solver can reach the backjump limit on any run. In this case the
+--    returned RetryLog ends with BackjumpLimitReached.
+--    TODO: Consider applying the backjump limit to all solver runs combined,
+--    instead of each individual run. For example, 10 runs with 10 backjumps
+--    each should count as 100 backjumps.
+-- 2. Since this function works by rerunning the solver, it is possible for the
+--    solver to add new unnecessary variables to the conflict set. This function
+--    discards the result from any run that adds new variables to the conflict
+--    set, but the end result may not be completely minimized.
+tryToMinimizeConflictSet :: forall a . (SolverConfig -> RetryLog String SolverFailure a)
+                         -> SolverConfig
+                         -> ConflictSet
+                         -> ConflictMap
+                         -> RetryLog String SolverFailure a
+tryToMinimizeConflictSet runSolver sc cs cm =
+    foldl (\r v -> retryNoSolution r $ tryToRemoveOneVar v)
+          (fromProgress $ Fail $ ExhaustiveSearch cs cm)
+          (CS.toList cs)
+  where
+    -- This function runs the solver and makes it prefer goals in the following
+    -- order:
+    --
+    -- 1. variables in 'smallestKnownCS', excluding 'v'
+    -- 2. 'v'
+    -- 3. all other variables
+    --
+    -- If 'v' is not necessary, then the solver will find that there is no
+    -- solution before starting to solve for 'v', and the new final conflict set
+    -- will be very likely to not contain 'v'. If 'v' is necessary, the solver
+    -- will most likely need to try solving for 'v' before finding that there is
+    -- no solution, and the new final conflict set will still contain 'v'.
+    -- However, this method isn't perfect, because it is possible for the solver
+    -- to add new unnecessary variables to the conflict set on any run. This
+    -- function prevents the conflict set from growing by checking that the new
+    -- conflict set is a subset of the old one and falling back to using the old
+    -- conflict set when that check fails.
+    tryToRemoveOneVar :: Var QPN
+                      -> ConflictSet
+                      -> ConflictMap
+                      -> RetryLog String SolverFailure a
+    tryToRemoveOneVar v smallestKnownCS smallestKnownCM =
+        continueWith ("Trying to remove variable " ++ varStr ++ " from the "
+                      ++ "conflict set.") $
+        retry (runSolver sc') $ \case
+            err@(ExhaustiveSearch cs' _)
+              | CS.toSet cs' `isSubsetOf` CS.toSet smallestKnownCS ->
+                  let msg = if not $ CS.member v cs'
+                            then "Successfully removed " ++ varStr ++ " from "
+                                  ++ "the conflict set."
+                            else "Failed to remove " ++ varStr ++ " from the "
+                                  ++ "conflict set."
+                  in failWith (msg ++ " Continuing with " ++ showCS cs' ++ ".") err
+              | otherwise ->
+                  failWith ("Failed to find a smaller conflict set. The new "
+                             ++ "conflict set is not a subset of the previous "
+                             ++ "conflict set: " ++ showCS cs') $
+                  ExhaustiveSearch smallestKnownCS smallestKnownCM
+            BackjumpLimitReached ->
+                failWith ("Reached backjump limit while minimizing conflict set.")
+                         BackjumpLimitReached
+      where
+        varStr = "\"" ++ showVar v ++ "\""
+        showCS cs' = "{" ++ showConflictSet cs' ++ "}"
+
+        sc' = sc { goalOrder = Just goalOrder' }
+
+        goalOrder' =
+            preferGoalsFromConflictSet (v `CS.delete` smallestKnownCS)
+         <> preferGoal v
+         <> fromMaybe mempty (goalOrder sc)
+
+    -- Like 'retry', except that it only applies the input function when the
+    -- backjump limit has not been reached.
+    retryNoSolution :: RetryLog step SolverFailure done
+                    -> (ConflictSet -> ConflictMap -> RetryLog step SolverFailure done)
+                    -> RetryLog step SolverFailure done
+    retryNoSolution lg f = retry lg $ \case
+        ExhaustiveSearch cs' cm' -> f cs' cm'
+        BackjumpLimitReached     -> fromProgress (Fail BackjumpLimitReached)
+
 -- | Goal ordering that chooses goals contained in the conflict set before
 -- other goals.
 preferGoalsFromConflictSet :: ConflictSet
                            -> Variable QPN -> Variable QPN -> Ordering
-preferGoalsFromConflictSet cs =
-    comparing $ \v -> not $ CS.member (toVar v) cs
-  where
-    toVar :: Variable QPN -> Var QPN
-    toVar (PackageVar qpn)    = P qpn
-    toVar (FlagVar    qpn fn) = F (FN qpn fn)
-    toVar (StanzaVar  qpn sn) = S (SN qpn sn)
+preferGoalsFromConflictSet cs = comparing $ \v -> not $ CS.member (toVar v) cs
+
+-- | Goal ordering that chooses the given goal first.
+preferGoal :: Var QPN -> Variable QPN -> Variable QPN -> Ordering
+preferGoal preferred = comparing $ \v -> toVar v /= preferred
+
+toVar :: Variable QPN -> Var QPN
+toVar (PackageVar qpn)    = P qpn
+toVar (FlagVar    qpn fn) = F (FN qpn fn)
+toVar (StanzaVar  qpn sn) = S (SN qpn sn)
 
 finalErrorMsg :: Verbosity -> Maybe Int -> SolverFailure -> String
 finalErrorMsg verbosity mbj failure =

cabal-install/Distribution/Solver/Modular/ConflictSet.hs

@@ -18,10 +18,12 @@ module Distribution.Solver.Modular.ConflictSet (
   , showCSSortedByFrequency
   , showCSWithFrequency
     -- Set-like operations
+  , toSet
   , toList
   , union
   , unions
   , insert
+  , delete
   , empty
   , singleton
   , member
@@ -98,6 +100,9 @@ showCS showCount cm =
   Set-like operations
 -------------------------------------------------------------------------------}
 
+toSet :: ConflictSet -> Set (Var QPN)
+toSet = conflictSetToSet
+
 toList :: ConflictSet -> [Var QPN]
 toList = S.toList . conflictSetToSet
 
@@ -137,6 +142,11 @@ insert var cs = CS {
 #endif
     }
 
+delete :: Var QPN -> ConflictSet -> ConflictSet
+delete var cs = CS {
+      conflictSetToSet = S.delete var (conflictSetToSet cs)
+    }
+
 empty ::
 #ifdef DEBUG_CONFLICT_SETS
   (?loc :: CallStack) =>