If you want to play with a powerful type system check out Raku. It offers gradual types that are a hybrid of dynamic and statically checked.
Basically, you can define a `subset` of a type with a validation predicate. Subsets can be named or anonymous and inline in function signatures.
Another thing that made me think of Raku was your discussion of NULLs. Any type container can be defined or undefined, an undefined Array container `isa` Array. But you can specify whether your annotation means to be specifically only defined or undefined members of the type. So `Int:D` is a defined integer, whereas `Int:U` is undefined, and `Int` is either.
The type specifications combined with multiple dispatch cam make for pretty code.
It's a really interesting language and, in my opinion, worth checking out. It would be great to hear your thoughts on it.