Encapsulate effects in QuickCheck function arguments

[MajaRet]

Issue

Closes #211

Description of the Change

Effects are now encapsulated in the arguments of QuickCheck functions.
Previously, for example, the following program

prop x = x + x === x + x

would have been transformed by the SharingAnalysisPass as follows.

prop x = let x@0 = x in x@0 + x@0 === x@0 + x@0

However, this led to prop becoming impure when the lets were transformed to shares and call-by-need evaluation was used. An impure property cannot be translated to a Coq Prop by the compiler, so it became unprovable.

Instead, QuickCheck functions now encapsulate generated let bindings (created by the SharingAnalysisPass or the FlattenExprPass). So the function above is transformed to

prop x = (let x@0 = x in x@0 + x@0) === (let x@0 = x in x@0 + x@0)

With this, the property itself remains pure.

Explicit lets in a Haskell module are not modified. Neither are regular predicates, so

p x = x == x

is still unprovable when translated to Coq. One way to mitigate this somewhat would be to write a property prop_p x1 ... xn = p x1 ... xn === True for a predicate p that takes n arguments, or to write a lemma manually in Coq that handles p.