Improve debuggability when a plan fails

[MaximilianAlgehed]

TODO:

• Track what variables have actually impacted what other variables
• As soon as one stage in the solver plan is ErrorSpec, fail
• When we fail, print only the variables (and their plan) that have affected the failure - need to track this transitively
• Add some better tests of the functionality

[MaximilianAlgehed]

One tricky observation here is that when we track what variables have affected another variable, we also need to track backPropagation changes. If you have a plan where x -> y -> z is the generation order and x isn't mentioned in the constraints of y, but both x and y are mentioned in the constraints of z it's possible that the choice of generated value for x impacts y. Furthermore, it's probably wise to print the constraints for z also - as those impact how y is constrained.

Before doing a bunch of work on this it might make sense to spend a little bit of time figuring out how often narrowing down the plan actually matters. One example where it probably makes sense is if you're constraining a type with a bunch of fields x0, ..., xN where xN depends on x0 but all other fields are independent, x0 is generated first, and xN is generated last. Here you clearly don't want to see x1...xN-1 as these are irrelevant.

[MaximilianAlgehed]

On master:

$> quickCheck $ prop_complete overconstrainedSuffixes 
*** Failed! Falsified (after 1 test):  
Stepping the plan:

    SolverPlan

      Linearization:
      zs_0 :: [Int] <-
        ErrorSpec
          Solving var zs_0 fails.
          Merging the Specs
             1. ErrorSpec
            propagateSpecFun (append HOLE ys) with (MemberSpec xss)
            there are no elements in xss with suffix ys
             2. TrueSpec @([Int])
          propagateSpecFun (append HOLE ys) with (MemberSpec xss)
          there are no elements in xss with suffix ys
      xs_2 :: [Int] <-
        MemberSpec [ [1,2,3] ]
        ---
        assert $ xs_2 ==. append_ zs_0 3
        4
        5

      v_4 :: ([Int],[Int],[Int]) <-
        TypeSpec
          (Cartesian , TrueSpec @([Int]) , MemberSpec [ [] ] , TrueSpec @([Int]))
          []
        ---
        assert $ ProdFstW to v_4 ==. xs_2
        assert $ ProdSndW (ProdSndW to v_4) ==. zs_0
  Env
  ys_1 -> []


StepPlan for variable: zs_0::[Int] fails to produce Specification, probably overconstrained.PS = 
Original spec ErrorSpec
  Solving var zs_0 fails.
  Merging the Specs
     1. ErrorSpec
    propagateSpecFun (append HOLE ys) with (MemberSpec xss)
    there are no elements in xss with suffix ys
     2. TrueSpec @([Int])
  propagateSpecFun (append HOLE ys) with (MemberSpec xss)
  there are no elements in xss with suffix ys
Predicates
Solving var zs_0 fails.
Merging the Specs
   1. ErrorSpec
  propagateSpecFun (append HOLE ys) with (MemberSpec xss)
  there are no elements in xss with suffix ys
   2. TrueSpec @([Int])
propagateSpecFun (append HOLE ys) with (MemberSpec xss)
there are no elements in xss with suffix ys

On this branch:

$> quickCheck $ prop_complete overconstrainedSuffixes 
*** Failed! Falsified (after 1 test):  
Failed to step the plan
  Relevant parts of original plan:
    SolverPlan
      ys_1 :: [Int] <- _
      zs_0 :: [Int] <- _
      xs_2 :: [Int] <-
        assert $ xs_2 ==. append_ ys_1 [1,2,3]
        assert $ xs_2 ==. append_ zs_0 [3,4,5]
  Relevant parts of the env:
    Env ys_1 -> []
  Current stage:
    zs_0 :: [Int] <-
      ErrorSpec
        Solving var zs_0 fails.
        Merging the Specs
           1. ErrorSpec
          propagateSpecFun (append HOLE ys) with (MemberSpec xss)
          there are no elements in xss with suffix ys
           2. TrueSpec @([Int])
        propagateSpecFun (append HOLE ys) with (MemberSpec xss)
        there are no elements in xss with suffix ys

The specification in the current stage is unsatisfiable, giving up.

So already a big improvement. A possible TODO here is to make ErrorSpec take a Doc - as we're currently struggling a bit with the way we pretty-print and nest things here.

[MaximilianAlgehed]

A major improvement here. The following constraints (meant to mimick constraining large records) has an inconsistency between the first and the last variables (a and f):

manyInconsistent :: Specification (Int, Int, Int, Int, Int, Int)
manyInconsistent = constrained' $ \ [var| a |] b c d e [var| f |] ->
  [ assert $ a <. 10
  , assert $ b >. a
  , assert $ c >. b
  , assert $ d >. c
  , assert $ e >. d
  , f `dependsOn` e
  , assert $ f >. 10
  , assert $ f <. a
  ]

Before we would have gotten a huge error message with a bunch of output. Now we only get the relevant bits:

$> quickCheck $ prop_complete manyInconsistent 
*** Failed! Falsified (after 1 test):  
Failed to step the plan
  Relevant parts of the original plan:
    SolverPlan
      a_5 :: Int <- TypeSpec [..9] [ ]
      f_0 :: Int <-
        TypeSpec [11..] [ ]
        ---
        assert $ f_0 <. a_5
  Already generated variables:
    a_5 -> 0
  Current stage:
    f_0 :: Int <-
      ErrorSpec
        NumSpec has low bound greater than hi bound
           [11..-1]
        when combining two NumSpecs
           [11..]
           [..-1]

The specification in the current stage is unsatisfiable, giving up.

[Soupstraw]

Looks good!