`gen_tree` should use `positive` instead of `nat`

I have a rose-tree-like datatype that I am generating a Countable instance for by giving an injection into gen_tree:

Inductive vty : Set :=
  | vty_int : vty
  | vty_real : vty
  | vty_var: typevar -> vty
  | vty_cons: typesym -> list vty -> vty.

And I wrote the following injection:

Definition vty_nonind := ((unit + unit)%type + typevar)%type.
Fixpoint vty_to_gen_tree (v: vty) : countable.gen_tree vty_nonind :=
  match v with
  | vty_int => countable.GenLeaf (inl (inl tt))
  | vty_real => countable.GenLeaf (inl (inr tt))
  | vty_var v => countable.GenLeaf (inr v)
  | vty_cons ts tys => countable.GenNode (Pos.to_nat (countable.encode ts)) (map vty_to_gen_tree tys)
  end.

It is straightforward to prove that this is an injection.

The problem is that I cannot compute with this; since the encoding of typesym often happens to produce a positive whose nat representation causes a stack overflow in Coq. Is there a reason that gen_tree takes a nat argument rather than positive, as it seems better for computation to avoid natural numbers entirely? Or is there a better way to inject into gen_tree?