Skip to content

Type checker unsoundly refines both operands of min/2 and max/2 from the result’s expected type #15833

Description

@lukaszsamson

Existing issue

  • I have searched existing issues and could not find a duplicate.

Elixir and Erlang/OTP versions

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

Interactive Elixir (1.21.0-dev)

Operating system

any

Current behavior

The implementation of max and min in Apply module passes result expected type into both args refinement. This is unsound because either argument can be discarded according to erlang term ordering. A consumer constrains only the selected result, not both operands.

Repro:

defmodule Example do
  def run(x) do
    :erlang.binary_part(max(x, ""), 0, 0)
    case x do
      a when is_integer(a) -> :integer
      a when is_binary(a) -> :binary
    end
  end
end

IO.inspect(Example.run(1))

Result: a false positive warning:

warning: the following clause will never match:

    a when is_integer(a) ->

because it attempts to match on the result of:

    x

which has type:

    binary()

where "a" was given the type:

    # type: integer()
    # from: iex:5
    is_integer(a)

└─ iex:5: Example.run/1

The code works and prints "integer"

Expected behavior

Type refinement should be applied to a union of both arguments

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions