Yes, but a dynamic language might also perform type inferencing on expressions during the compilation phase to determine which code paths are unreachable, or to determine that certain runtime predicates may be replaced with compile time constants (such as true/false), determine which optimizations may be made, or to determine that a certain runtime error is sure to be triggered, thus complain at compile time. Even if the compiler makes those checks, I don’t know what “an expression type checks” means in that context.
Well, then it’s doing some static type checking too.
It means that the type checker attests the expression can be given a type according to the rules of the type system. Usually, that’s used to make sure that evaluating the expression will not result in runtime type errors.
My guess is that it means whether it is decidable wether a type is inhabited. In a type system which supports intersection and complement, the inhabited problem is equivalent to the subtype problem ( I believe). A <: B iff A&!B <: empty-type … If a type system does not support complementation, I’m not sure how the problems relate.
CLOS makes run-time dispatch decisions based on class (or identity), but not necessarily type. Every class is a type, but not all types are classes. So method dispatch does not need to answer a run-time subtype question, but rather a graph search (or several searches) in the class hierarchy.
It means you cannot invent an algorithm that always finds the most specific type possible for a given expression. Unions and intersections between known types are not the problem - we are assuming we know all declared type relationships and if two types are unrelated, it means the intersection is Nothing. The problem are type arguments to be filled in.