To let or not to let

[JacquesCarette]

Right now, let in Agda generates substitutions (as confirmed by Andreas here amongst other places). The attempted fix for this has stalled even though it is an extremely old issue.

The advice is to favour where over let.

The question is: do we program stdlib to current Agda or some optimistic future Agda that will have a better implementation of let?

Given just how long this has been a wart, I'm of the opinion that being optimistic would be ill-placed (even though I'm actually normally fairly optimistic!)

[gallais]

FTR, these cannot be turned into where definitions because these get lifted to the
toplevel and that is not done in a modality-respecting way. In other words: turning
these into where definitions leads to errors about irrelevant values being used in
a relevant context.

https://github.com/gallais/agda-stdlib/blob/7947cd42ca813dfc9024bc50552c5cd5ea35f221/src/System/Random.agda#L119-L133

[JacquesCarette]

Good point: indeed there are times when we have no choice, because the implementation scheme for where is also sub-optimal.

[jespercockx]

Unfortunately, Agda currently does not have any way to create a local shared closure: let bindings are inlined, while where declarations are lifted to the top level.