> Like a LLVM but for type systems instead of compilation / interpreters / JIT.

This would be a very cool project, but depending on what you actually want out of it is basically open research in programming languages. Racket #langs and their general approach to type-checking are one sort of answer to this: it's basically a "language-building lab" with an underlying philosophy that we should all be approaching programming in a language-oriented way, that is, by building domain-specific languages that raise the level of abstraction for what you're talking about. That's probably the most developed approach to this sort of thing, but it's still very much something that the Racket folks continue to iterate on and design further.

If you want more conventional _static_ type systems with a much harder delineation between "compile-time" and "runtime" than exists in Racket, you start getting into a sort of compiler-generator-framework territory with the type system, and you'd probably want a language for metatheory to program the type system in, and that starts to look like compiler-generator frameworks embedded into proof assistants like Agda or Rocq. There's some research in that space as well, but certainly nothing that has anything near universal agreement that it works well.

Right now, the state-of-the-art for designing type systems for any language is essentially "employ a bunch of people with very, very deep specialization in this subject matter to painstakingly design and implement the type system with careful consideration of the runtime semantics of the language it's being built for." It's not easy, and it's not cheap, which is why the successful instantiations of this kind of thing are all massive corporate-backed projects. As someone who is really a type system designer first and a corporate-tech-worker a very distant second, I'd love to be able to democratize building type systems more (or to see that be democratized), but it feels very, very far away from being solved.

I would want to go further and use domain specialized analyzers and type systems that are extensible with 'design time' information, ala F# type providers. It is indeed still a research level project that needs multi-national corporation level funding and I doubt that'll happen any time soon. I think it's more likely that a programming languages designed for use by LLMs will spur some investment there - type system ergonomics are often limited by latency and LLMs can be both be more patient as well as learn not to rely on it as often.

EDIT: Oh Hi! I didn't realize you're from the Luau team, cool, while Roblox isn't as big as Microsoft I wonder if it's a large enough multi-national to make a real dent in the research, I do hope you'll get your wish. I know I don't have the resources to take on such a project myself. I do type directed code generation which is about as close to the sun as I can safely fly.