Do not spend fuel when given index is structurally decreasing

[AlgebraicWolf]

Currently whenever derived generator recursively calls itself with a structurally smaller given parameter, the fuel is spent nonetheless. Consider the following example:

data NatVect : Nat -> Type where
  Nil : NatVect 0
  (::) : Nat -> NatVect n -> NatVect (S n)

genNatVect : (Fuel -> Gen Nat) => Fuel -> (n : Nat) -> Gen $  NatVect n
genNatVect = deriveGen

In that case, if desired length is greater than fuel, no output would be produced, because the generator would run out of fuel before producing anything. Decrease of fuel, however, is not required here -- generator calls itself with decreasing given parameter, hence ensuring termination.

Perhaps it would be better to avoid spending fuel in such cases?

[buzden]

The main problem here (at least now) is preserving good (or even better) distribution. Consider Fin n: now it's evenly distibuted between values from 0 to left fuel (when left fuel is less than n). If we don't spend fuel, we cannot use it adequately fuel for frequency of recursive constructors (BTW, we seemingly cannot do this adequately when fuel is more than n).

The solution I see is having an interface returning max depth by given value and its indices, i.e. e.g. returning n by {n : Nat} -> Fin n, and using this as a frequency measure in for types when it's implemented, and using (and spending) fuel as it is done now for other types.