This means that each function and each variable will have a type assigned. And this type might be a complex expression, like or consisting of N clauses. To check that a type inferred from function body is a subtype of a type specified in the type spec of a function, compiler must compare these two expressions which is a turing-complete operation and can (and will) consume a lot of time.
Therefore compilers use different approaches like speculative complexity reduction (for example in dialyzer type expression @type enum() :: :x1 | :x2 | :x3 | :x4 | :x5 | :x6 is reduced to @type enum() :: atom()).
And in my honest opinion, this type precision aim taken by type system team will create a lot of complex types, and type-checking would either consume a lot of time or will make developers handle situations which are not going to happen, caused by complexity-reduction approach. This is the problem caused by “paper first” approach taken, where theoretical ideas were developed before the actual implementation.
We will start with option 1: we will fallback to dynamic. However, I can see us also doing option 3 in the future, if we can measure places where introducing the runtime checks will not decrease or will potentially improve performance.