API for reduction-insenstive constr traversal #46
Description
I'm reviewing rocq-prover/rocq#12218, and seeing a lot of code that I believe will be wrong in the presence of casts, let-ins, and reducible matches (if true then ... else ...) in surprising places (like at top-level in the types of constructors). Coq also has a number of performance issues in the presence of nested let ... in ...s, e.g., around computation of implicit arguments.
This suggests to me that Coq should have a term-traversal API which is insensitive to some sorts of reduction, much like EConstr is insensitive to evar-normalization. Ideally it would not incur overhead (it should add let-binders to the context rather than substituting them, it should, perhaps, perform beta-reduction by binding the argument in a let binder and going under the binder), and be much more light-weight than EConstr. For example, it might just be a kind function which updates the local environment and returns both the context and the kind of term modulo whatever you ask it to be modulo.
Said another way, this would be an API for traversing fully reduced terms (or perhaps βιζ-normal terms) without having to perform expensive substitutions in parts of the terms that you don't care about.
I haven't turned this into an actual CEP because I don't have a good enough sense of this, but I'd be interested in comments and/or starting a discussion here.