Encode Invariant properties in the type system for quickcheck properties

[doyougnu]

Currently we have quickcheck/smallcheck properties like this:

plainBecomesUnit :: TestTree
plainBecomesUnit = QC.testProperty
  "For all plain formulas the found variational core is Unit"
  $ \p -> isPlain p QC.==> QCM.monadicIO $
          do (core, _) <- liftIO $ solveForCore p Nothing
             QCM.assert $ isUnit core

which generates random plain propositions and makes sure that any plain proposition is reduced to a Unit variational core. This works but has the following problem:

...
[GOOD] (assert false)
[Debug] Proposition:  : LitB False @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Core:  : VarCore Unit @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Is Core Unit:  : True @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
*** Solver   : Z3
*** Exit code: ExitSuccess
OK (0.49s)
        +++ OK, passed 100 tests; 213 discarded.

All 7 tests passed (0.54s)
Test suite VSMTTest: PASS
Test suite logged to: /store/Research/VSmt/haskell/vsmt/dist-newstyle/build/x86_64-linux/ghc-8.8.4/vsmt-0.0.1/t/VSMTTest/test/vsmt-0.0.1-VSMTTest.log
(END)

namely, that quickcheck discards 213 generated propositions because these propositions failed the isPlain check in the antecedent of QC.==>. A better way is to newtype the property of Plain, i.e.:

-- | Proof that a is Plain
newtype Plain a = Plain a

and then write a generate just for Plain. This avoids the generate -> test loop and will allow the property to be tested on much more than 100 test cases.

[doyougnu]

This places an upper limit on the quickcheck tests we are able to perform:

OK (4.66s)
        +++ OK, passed 1000 tests; 1967 discarded.

its about 2n where n is the number of generated tests. This leads to false positive failures such as:

...
[Debug] Proposition:  : OpBB Or (OpBB And (RefB "ytcceknau") (OpIB NEQ (RefI (ExRefTypeD "vpzcey")) (RefI (ExRefTypeD "rtbjs")))) (OpIB EQ (RefI (ExRefTypeI "ekefv")) (RefI (ExRefTypeD "ws"))) @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Core:  : VarCore Unit @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Is Core Unit:  : True @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
*** Solver   : Z3
*** Exit code: ExitSuccess
FAIL (7.05s)
        *** Failed! Assertion failed (after 1413 tests and 6 shrinks):
        OpBB Or (OpBB And (RefB "ytcceknau") (OpIB NEQ (RefI (ExRefTypeD "vpzcey")) (RefI (ExRefTypeD "rtbjs")))) (OpBB Eqv (RefB "ykgxzwyoxb") (OpIB EQ (RefI (ExRefTypeI "ekefv")) (RefI (ExRefTypeD "ws"))))
        Use --quickcheck-replay=411029 to reproduce.

where the debug log says this reduced to a Unit, yet quickcheck thinks it fails.

[doyougnu]

I tweaked the algorithm and we no longer have a strict upper limit:

*** Solver   : Z3
*** Exit code: ExitSuccess
OK (9.69s)
        +++ OK, passed 2000 tests; 3823 discarded.

All 4 tests passed (19.20s)
Test suite VSMTTest: PASS

But this should still be encoded in the type system