[rtpg]

Totally agree. I think that something that has some sort of "partial" evaluation and basically merging values and types would be so powerful and crush many interesting bugs.

Instead of having to do type-level programming, how about relying on the fact that the type checker is also running on a computing machine? The fact that we don't even have super simple stuff like first-class union types (let alone nice type manipulation logic) in most stuff is really painful.

An aside: I think one way Typescript gets away with this (beyond soundness stuff), is that it doesn't have to actually build some high performance evaluation model for its type system. It doesn't care, it's here to check the validity of your code, not to run it! It's a very powerful concept that opened up so much without having to futz about with like... how to efficiently represent all these unions.

How many times have you stared at a thing, think "if I could open up the compiler/type checker at the end, I could totally verify some property of my code, but it is not expressible in the type system"?