Container type constructors drop static parts of gradual element types

[lukaszsamson]

Elixir and Erlang/OTP versions

Erlang/OTP 28 [erts-16.2] [source] [64-bit] [smp:12:12] [ds:12:12:10] [async-threads:1] [jit]

Interactive Elixir (1.20.0-rc.4)

Operating system

any

Current behavior

tuple/1, closed_map/1, open_map/1, non_empty_list/1,2 discard the static component of gradual element types, producing dynamic-only containers. This breaks subtype relation
Repro:

import Module.Types.Descr

# NOTE static and dynamic part
x = union(atom([:ok]), dynamic(integer()))                                                                                                                                                                   
%{atom: {:union, %{ok: []}}, dynamic: %{atom: {:union, %{ok: []}}, bitmap: 8}}

# subtype holds
subtype?(atom([:ok]), x)
true

# NOTE only dynamic
tuple([x])
%{dynamic: %{tuple: {:closed, [%{atom: {:union, %{ok: []}}, bitmap: 8}]}}}
closed_map(a: x)
%{dynamic: %{map: {:closed, [a: %{atom: {:union, %{ok: []}}, bitmap: 8}]}}}
open_map(a: x)
%{dynamic: %{map: {:open, [a: %{atom: {:union, %{ok: []}}, bitmap: 8}]}}}
non_empty_list(x)
%{dynamic: %{list: {%{atom: {:union, %{ok: []}}, bitmap: 8}, %{bitmap: 4}}}}

# subtype does not hold
subtype?(tuple([atom([:ok])]), tuple([x]))
false
subtype?(closed_map(a: atom([:ok])), closed_map(a: x))
false
subtype?(open_map(a: atom([:ok])), open_map(a: x))
false
subtype?(non_empty_list(atom([:ok])), non_empty_list(x))
false

Cause: All three constructors call :maps.take(:dynamic, value) on element types and use only the dynamic part, discarding _static:

• tuple_descr/3

  elixir/lib/elixir/lib/module/types/descr.ex

  Line 4931 in 03b45e5

  {dynamic, _static} ->

• map_descr_pairs/4

  elixir/lib/elixir/lib/module/types/descr.ex

  Line 4827 in 03b45e5

  fields_fetch!: 2,

• list_pop_dynamic/1

  elixir/lib/elixir/lib/module/types/descr.ex

  Line 4224 in 03b45e5

Expected behavior

Constructors should split the element into static and dynamic parts, building both a static container and a dynamic container. There are tests asserting existing dynamic hoisting behavior:

dynamic(open_map(a: integer())) == open_map(a: dynamic(integer()))

[josevalim]

I believe this is expected. Yes, the subtyping relationship is no longer respected but we are supposed to use the compatible relationship in a gradually typed language. What we should do, instead, is to make sure we are not using subtype when we are supposed to be using compatible. I will double check that.

@gldubc can you please confirm this is expected?

[josevalim]

I have confirmed all uses of subtype were correct, I added further checks and comments.

[josevalim]

Oops, I was not planning to close with the previous PR, just cross-reference.

[lukaszsamson]

@josevalim Your answer is partially correct. All current subtype? call sites are sound for the current type checker behaviour. It will not lead to false positive warnings. However, the current code is not semantically correct. It is loosely widening the lower bound and it will likely become a problem with redundancy/exhaustiveness checks later.

Elixir type theory in descr.ex says a gradual type is:
(dynamic_component and dynamic()) or static_component
with invariant:
dynamic_component >= static_component

The system tracks lower static bound and upper dynamic bound.

For a covariant constructor C like tuple/list/map-value formation, the gradual lifting is:
C([L, U]) = [C(L), C(U)]
not
[∅, C(U)]
unless L = ∅.
Current code does the later.

Upper bound alone does not suffice for all checking. compatible?/2 also uses the static part when it exists, e.g.

upper_only = %{dynamic: %{list: {union(atom([:ok]), integer()), empty_list()}}}
lower_upper = %{
  list: {atom([:ok]), empty_list()},
  dynamic: %{list: {union(atom([:ok]), integer()), empty_list()}}
}
expected = non_empty_list(integer())
compatible?(upper_only, expected)     # true
compatible?(lower_upper, expected)   # false

Once elixir starts using lower bounds then these constructors will under-approximate the static guarantees of common container shapes leading to missed/incorrect warnings

[gldubc]

I agree, this is actually a bug! Constructors should preserve their static part when it is non empty. The issue comes from an incorrect assumption of mine, forgetting there would be lower bounds in constructor arguments. I'm reading your PR.

[josevalim]

However, the current code is not semantically correct. It is loosely widening the lower bound and it will likely become a problem with redundancy/exhaustiveness checks later.

Redundancy/exhaustiveness is already checked today and it is not issue because we check for it using the upper bound (which is the most conservative approach).

There are scenarios where this bug can show up though, so as Guillaume said above we need to address it, but I believe they cannot happen at the moment because: 1. we infer mostly dynamic types (so all components are dynamic) and 2. treating everything as dynamic makes the types more relaxed, which matches the current stage of no false warnings. Thanks for the report!

[lukaszsamson]

I think we can surface the bug (in a form of a false negative) with the current code

typecheck!([x], (fn [n] when is_integer(n) -> n + 1 end).([:ok, x]))
%{dynamic: :term}

where the same code on #15275 branch emits a type error

typeerror!([x], (fn [n] when is_integer(n) -> n + 1 end).([:ok, x])) |> IO.puts

incompatible types given on function call:

    (fn [n] when is_integer(n) -> n + 1 end).([:ok, x])

given types:

    dynamic(non_empty_list(term()) and not non_empty_list(:ok)) or non_empty_list(:ok)

but function has type:

    (non_empty_list(integer()) -> dynamic(integer()))

where "x" was given the type:

    # type: dynamic()
    # from: types_test.ex:11
    x

[josevalim]

Yup, that makes sense, good find! It will be good to add as a test case too!

[josevalim]

Actually, now that I think about it, I don't think the example above is correct. If you swap the elements in the list, you don't want a warning. If you take a tuple {:ok, x}, the tuple should only have a static part if all elements in the tuple have a non-empty static part. The same should apply for lists.

@gldubc if we represented lists as pairs, we would require all elements to have non-empty statics, so that should also be the case here.

PS: Finally, keep in mind the tests run a static version of the type system which does not introduce dynamic in a few places.