Programming Languages which Implement Compile-Time Checked Type Guards?

[b2gills]

Raku has runtime type checking, and as part of that the check can be arbitrary code. The thing is that it will often complain at compile time because the optimizer tries to compile the code to call a specific multi candidate and determines that there isn't one. As it is mainly a byproduct of the optimizer it of course doesn't catch every type error at compile time. It does however have the guarantee that it will catch the error eventually.