## 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 Edsko's large-records blog post for a wonderfully detailed exposition of the problem.

The problem is that type applications force a quadratic representation of, say, heterogeneous lists. Here is an example:

```
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

```
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

```
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?