Treat So (f x y z) and f x y z = True arguments of constructors specially during derivation

[buzden]

If constructor's argument is of form So $ f x y z or f x y z = True or True = f x y z (for whatever function f and whatever count of its arguments), and if we can inspect this f, we can optimise generation to be more constructive, instead of filtering, during generation.

What we can do is to generate a special data type definition F so that if f : X -> Y -> Z -> Bool, F would be data F : X -> Y -> Z -> Type so that both

equivDir : (x : X) -> (y : Y) -> (z : Z) -> f x y z = True -> F x y z
equivRev : (x : X) -> (y : Y) -> (z : Z) -> F x y z -> f x y z = True

hold.

This means that we can replace So $ f x y z and/or f x y z = True argument by F x y z without any change in the meaning.

Thus, we can replace isJust m = True with IsJust m, and elem x xs with Elem x xs. Generators derived with such a trick would be much more performant, since they would not compute direct function, instead they would constructively generate appropriate values.

---

Beware of thoughts of general replacement of, say, functions like elem x xs to Elem x xs and corresponding getting the value out of this Elem! In the context of returning True this change seems to be appropriate, where in the general case the order of pattern-matching in a function is significant, whereas the order of generations of constructors in corresponding type is not. This approach is appropriate only for functions with non-overlaping clauses.