Support arbitrary order of arguments for derived generators

[buzden]

Say, I have a type

data X : Fin n -> Fin m -> Type where ...

and want to derive generator for it with all arguments given. I'd like to write something like

genX : {n : Nat} -> (f : Fin n) -> {m : Nat} -> (g : Fin m) -> Gen MaybeEmpty $ X f g
genX = deriveGen

but now I'm beaten with an error that the order of arguments must be the same as in type, i.e. to be the following:

genX : {m : Nat} -> {n : Nat} -> (f : Fin n) -> (g : Fin m) -> Gen MaybeEmpty $ X f g

which is not logical, nor convenient. The first type of signature should be supported too.

[buzden]

Implementation detail: external generators, then, should be also allowed to have abritrary orders, thus we need to either store the signature of a generator, or permutation of its arguments in order to call them (including information of whether those arguments are explicit or implicit).

Additional advancement of being able to do this is that we would be able to use as externals arbitrary user %hint's, with any order of arguments.