Improve back-propagation for pairs

[MaximilianAlgehed]

We have this example, which is a simplified version of something that's going wrong when trying to bump ledger:

complicatedEither :: Specification (Either Int Int, (Either Int Int, Int, Int))
complicatedEither = constrained' $ \ [var| i |] [var| t |] ->
  [ caseOn i
      (branch $ \ a -> a `elem_` lit [1..10])
      (branch $ \ b -> b `elem_` lit [1..10])
  , match t $ \ [var| k |] _ _ ->
    [ k ==. i
    , not_ $ k `elem_` lit [ Left j | j <- [1..9] ]
    ]
  ]

We get the following issue:

*** Failed! Falsified (after 3 tests):  
Failed to step the plan
  Relevant parts of the original plan:
    SolverPlan
      i_5 :: Either Int Int <-
        TypeSpec
          (SumSpec type=Either Int Int
             | 1 MemberSpec [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ]
             | 1 MemberSpec [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ])
          [ ]
      t_4 :: ((Either Int Int),Int,Int) <-
        TypeSpec
          (Cartesian
             , TypeSpec
               (SumSpec | 1 TrueSpec @(Int) | 1 TrueSpec @(Int))
               [ Left 1, Left 2, Left 3, Left 4, Left 5, Left 6, Left 7, Left 8, Left 9 ]
             , TrueSpec @(Prod Int Int))
          [ ]
        ---
        assert $ sel @0 t_4 ==. i_5
  Already generated variables:
    i_5 -> Left 4
  Current stage:
    t_4 :: ((Either Int Int),Int,Int) <-
      ErrorSpec
        cartesian left
        The two Either Int Int Specifications are inconsistent.
          MemberSpec [ Left 4 ]
          TypeSpec
          (SumSpec | 1 TrueSpec @(Int) | 1 TrueSpec @(Int))
          [ Left 1, Left 2, Left 3, Left 4, Left 5, Left 6, Left 7, Left 8, Left 9 ]

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

This is essentially because the cant set isn't back-propagated from t_4 to i_5.

It even fails with in a simpler setting:

pairCant :: Specification (Int, (Int, Int))
pairCant = constrained' $ \ [var| i |] [var| p |] ->
  [ assert $ i `elem_` lit [1..10]
  , match p $ \ [var| k |] _ ->
    [ k ==. i
    , not_ $ k `elem_` lit [1..9]
    ]
  ]

with:

Failed to step the plan
  Relevant parts of the original plan:
    SolverPlan
      i_4 :: Int <- MemberSpec [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 ]
      p_3 :: (Int,Int) <-
        TypeSpec
          (Cartesian , TypeSpec [..] [ 1, 2, 3, 4, 5, 6, 7, 8, 9 ] , TrueSpec @(Int))
          [ ]
        ---
        assert $ sel @0 p_3 ==. i_4
  Already generated variables:
    i_4 -> 9
  Current stage:
    p_3 :: (Int,Int) <-
      ErrorSpec
        cartesian left
        The two Int Specifications are inconsistent.
          MemberSpec [ 9 ]
          TypeSpec [..] [ 1, 2, 3, 4, 5, 6, 7, 8, 9 ]

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

[MaximilianAlgehed]

In this particular special case we could actually use mapSpec here, because all the functions used in sel @0 are unary, and mapSpec works on unary functions.

It would be nice to have a generalization of mapSpec to contexts. That would allow us to do other similar things.

We could do the first thing to implement this by implementing the context-wide version but only do something non-trivial when the applications are unary (i.e. use mapSpec).