draft: extend support for type lets in Core
While Core supports let-bound types to some extent, they are systematically inlined by the simplifier right after they are introduced. As #20264 shows, programs that make heavy use of the typing machinery are prone to size explosion when compiled to Core which is explicitly typed. This MR attempts to delay the inlining of the currently ephemeral type lets to maintain sharing for as long as possible in the core2core pipeline.
Disclaimer: this is completely work in progress, I am opening this draft MR to get some preliminary feedback and directions.
What's implemented: Instead of being substituted immediately, let-bound type are kept and other parts of the simplifier can look through a let-bound TyVar by inspecting its unfolding, just like Ids.
Until now, the occurrence analiser only computed precise occurrence of Ids (both syntactic occurrences and how many times they're used), while CoVars occurrences were simply gathered from coVarsOf{Co,Type}
, and therefore could only be IAmDead
or ManyOccs
.
This MR implements precise occurrence analysis for coercion and types, which lets us substitute let-bound types if they are used only once. For now this is not done because type-lets are scarce.
What's missing:
- Floating, ANF-isation & CSE: We also want type lets to float out, unlocking new sharing opportunities in conjunction with ANF-isation and CSE, which might ultimately help mitigate issues like #5642. I wasn't able to make floating work nicely, as it requires glomming top-level type variable bindings. Glomming is hard to get right because we can't even inspect a top-level binder to figure whether it's an Id or a TyVar, which forces the variable and can trigger infinite loops. Previously it didn't cause any problem because all top-level identifiers were Ids so it behaved more or less like a normal recursive group. It also raises the following question: how should top-level type lets behave across interfaces? Should they be exported?
- Just like types, coercions are also systematically inlined, and thus can lead to size explosion. We'd also want to delay the substitution of let-bound coercions as much as possible.
- More source of type-lets, particularly from the zonker which currently destroys the ANF-like structure of types in the typechecker.
Most of these were already implemented in my dirty fork for experiments (see wip/type-sharing-experiments for floating, ANF-isation & CSE, and wip/scoped-metas which introduces type-lets in the zonker), which is too unorthodox to include in this MR until glomming is figured out (which I currently circumvent by sorting bindings in core lint).