ArbitrarySizedSuchThat with higher-kinded types

[lastland]

The following definition and command work:

Inductive nonempty_nat_list : list nat -> Prop :=
| cons_nat_list : forall x xs, nonempty_nat_list (x :: xs).

Derive ArbitrarySizedSuchThat for (fun n => nonempty_nat_list n).

but they will no longer work if I make nat polymorphic:

Inductive nonempty_list {e} : list e -> Prop :=
| cons_list : forall x xs, nonempty_list (x :: xs).

Derive ArbitrarySizedSuchThat for (fun n => nonempty_list n).

and this does not work, either:

Derive ArbitrarySizedSuchThat for (fun n => @nonempty_list nat n).

Is this a bug? Or did I miss something?

[lemonidas]

Must be a bug with implicit arguments. I'll take a look.

[lemonidas]

After fixing a shallow parameter-related bug, the underlying reason this still fails is that the deriver won't put a "Gen e" argument to the derived class implementation. That needs a bit more thought to solve than a quick fix, but it should be fixable without major refactoring.