[shrinking] does not always find the minimal counter example

[n-osborne]

Shrinking on a sequential STM test sometimes does not find the minimal example.

Here one output of this test.

generated error fail pass / total     time test name
579 [✗]    2    0    1    1 /  100     0.0s STM sequential tests
580
581 --- Failure --------------------------------------------------------------------
582
583 Test STM sequential tests failed (11 shrink steps):
584
585 [(Add 2078704297448381768); (Remove 2078704297448381768); (Mem 5022333781122650); Cardinal]
586
587 +++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
588
589 Messages for test STM sequential tests:
590
591   Results incompatible with model
592
593    (Add 2078704297448381768) : ()
594    (Remove 2078704297448381768) : Some (2078704297448381768)
595    (Mem 5022333781122650) : false
596    Cardinal : 1
597 ================================================================================
598 failure (1 tests failed, 0 tests errored, ran 1 tests)

[jmid]

This is surprising! I'm believe it is caused by the QCheck list shrinker:

# #require "qcheck";;
# open QCheck;;
# Shrink.list [0;1;2;3] (fun xs -> Printf.printf "%s - %!" (Print.(list int) xs));;
[0; 1] - [2; 3] - [0; 2; 3] - [1; 2; 3] - - : unit = ()

Here the possibilities [0;1;2] or [0;1;3] are never attempted...

Since we are operating over small lists (max size 20 IIRC) we might just want to go for a custom shrinker that attempts to remove one element at a time (from the back), like the recent multiple-ts shrinker in #112