so, today I thought I found a way to enumerate only linear terms while still pruning dead branches lazily. that'd be a massive speedup on SupGen, but it didn't work :( so we're back to enumerating full λ-terms on the bright side, I learned we can enumerate all terms of arbitrary datatypes, without needing to split labels, by just building it as an accumulator with holes. doesn't seem very useful, but, anyway, here is the HVM3 source: