If the compiler/runtime are capable of passing the types down to the CPU, then aren't they are capable of emitting equivalent checks in assembly?
It could be done, but then
- we move those checks from compile time to run time, impacting performance
- we detect type errors at runtime instead of compile time, losing all the benefits of a type system
Bloating an instruction set with high-level primitives increases the complexity of the assembler
True, but this instruction set may still be different from the CPU one, so it's just another (intermediate) language, not something the CPU needs to follow.
and slows down execution time because the assembler is busy doing the compiler's job.
No, the assembler does not run at run time. At compile time, the assembler emits machine code. Compile time may get longer, but the runtime performance should not be affected.
It sounds like this would make a compiler writer's job easier but expands the TCB without any real gains in speed or safety.
Expanding the TCB is not always detrimental to safety. Assume a nuclear power plant with some software to check that the temperature is kept in the safe range. Removing that software would make the TCB smaller, but the plant would hardly be more safe.
Adding a type system to a TCB puts more safety checks in the system. As long as the type system is not allowed to modify the program code, but only to report "well-typed / ill-typed", it can not harm safety. If it passes ill-behaved programs, say because of some bugs in the type checker, those would be executed anyway without the type system. If it fails some well-behaved programs, that's unfortunate, but preventing the deployment of a new program is always a safe choice -- this impacts productivity but not safety.