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)

See

• Edsko's large-records blog post for a wonderfully detailed exposition of the problem.
• Type level sharing now

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?