let-bind more types to save space
GHC Core has support for `let`-binding type variables. This feature is little used today. But a conversation at an HIW talk by @edsko, including @nomeata, @kosmikus, @christiaanb, and @sweirich made me wonder if it could be the answer to a problem.
See also
* #25381
* #21412
* #24462 (coercion lets)
* #25551
* #25923
* #27898
* #5642
See
* [Edsko's large-records blog post](https://well-typed.com/blog/2021/08/large-records/) for a wonderfully detailed exposition of the problem.
* [Type level sharing now](https://well-typed.com/blog/2021/12/type-level-sharing-now/)
The problem is that type applications force a quadratic representation of, say, heterogeneous lists. Here is an example:
```hs
type HList :: [Type] -> Type
data HList tys where
HNil :: HList '[]
HCons :: forall a as. a -> HList as -> HList (a : as)
```
Now, suppose I want a list `[42, True, 'x', 3.14]`. This would be
```hs
HCons @Int @((:) @Type Bool ((:) @Type Char ((:) @Type Double ('[] @Type)))) 42
(HCons @Bool @((:) @Type Char ((:) @Type Double ('[] @Type))) True
(HCons @Char @((:) @Type Double ('[] @Type)) 'x'
(HCons @Double @('[] @Type) 3.14
HNil)))
```
You can see that the tails of the type list are repeated. Using type-level `let`, we can rewrite this as
```hs
let t3 = '[] @Type in
let t2 = (:) @Type Double t3 in
let t1 = (:) @Type Char t2 in
let t0 = (:) @Type Bool t1 in
HCons @Int @t0 42 (HCons @Bool @t1 True (HCons @Char @t2 'x' (HCons @Double @t3 3.14 HNil)))
```
That's much better! It's not quadratic. There is still some redundancy, but at least it's not quadratic.
Implementing this seems relatively easy: instead of filling in metavariables in the solver, we just bind them in the `EvBindsVar`. I know it won't be quite that easy (we have to figure out which `EvBindsVar`(s) are associated with which variables), but I think we have the structure to experiment with this. (Another problem: it won't work in, say, type signatures, when we have no `EvBindsVar`.)
Open question: in the absence of -dcore-lint, will this speed up programs?
Open question: does the optimizer re-expand type-lets?
issue