DepTyCheck derives fuel-consuming generators for provably (mutually) decreasing types.

[GlebChili]

Consider the following project: https://github.com/GlebChili/DtcRecursive/tree/bfbe23a4216c11aac9fc6d36ad82ed3309b99aa6

We derive generator for type Literal (https://github.com/GlebChili/DtcRecursive/blob/bfbe23a4216c11aac9fc6d36ad82ed3309b99aa6/src/DtcRecursive/Types.idr#L32) given index Form (https://github.com/GlebChili/DtcRecursive/blob/bfbe23a4216c11aac9fc6d36ad82ed3309b99aa6/src/DtcRecursive/Types.idr#L12)`.

Expected behavior

The derived generator is able to produce a Literal for any Form without consuming any fuel, since Literal and LiteralVec are provably mutually decreasing as shown by hand-written generators genLiteralHW and genLiteralVecHW (https://github.com/GlebChili/DtcRecursive/blob/bfbe23a4216c11aac9fc6d36ad82ed3309b99aa6/src/DtcRecursive/Types.idr#L54-L70).

Actual behavior

DepTyCheck derivator fails to recognize strictly decreasing recursion and resulting generator extensively spend fuel, making it is almost impossible to populate type Literal f for relatively simple f on small amounts of fuel. (See project's module Main for a benchmark between derived and hand-written generator).

Pack collection used

nightly-251214