Type refinement

When checking the a case clause, a function clause, a receive clause and a clause in try and catch, we make use of information from the previous clauses to make the type checking more exact. When the type checker knows exactly what must have mismatched in the previous clauses for the execution to be able to reach the following clauses, those types can be excluded when checking the the rest of the clauses. This is called type refinement.

-spec foo(apa | hest | 42) -> 42.
foo(apa)  -> 42;  %% if this mismatches, apa is excuded
foo(hest) -> 42;  %% if this mismatches, hest is excluded
foo(X)    -> X.   %% here, X can only be 42, so no type error here

When can type refinement happen?

Type refinement can only be applied when the type checker knows exactly why a clause mismatches and those values can be excluded from the types. That means that we can refine types that consists of unions of singleton types. Singleton types are single integers, atoms, the empty list, the empty tuple and tuples consisting of singletons. Empty maps and empty binaries are singleton types too, but currently Gradualizer is not capable of using these for refinement. Free variables and _ (match all) can also be part of pattern. We know that these can never cause a pattern to mismatch.

What prevents type refinement?

1. Guards. If there is any uncertainty to why a clause mismatches, such as a guard that depends on values unknown at compile time, we can not exclude any values. We cannot exclude the possibility that the clause mismatches just because of the guard. Currently, Graudalizer can only do type refinement for clauses without guards.

%% This gives a type error
-spec guard_prevents_refinement(apa | bepa) -> bepa.
guard_prevents_refinement(X) ->
    Y = receive Message -> Message end,
    case X of
        apa when Y /= yellow -> bepa;
        Other                -> Other  %% Here, Gradualizer cannot exclude apa
    end.

2. Imprecision. If a type or a part of a type in a clause is matched against a pattern that we cannot remove from the type, we cannot refine.

-spec imprecision_prevents_refinement(float(), a|b) -> b.
imprecision_prevents_refinement(3.14, a) -> b;
imprecision_prevents_refinement(_,    X) -> X. %% 'a' cannot be excluded