Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 48 additions & 4 deletions lib/elixir/lib/module/types/descr.ex
Original file line number Diff line number Diff line change
Expand Up @@ -584,22 +584,33 @@ defmodule Module.Types.Descr do
defp numberize(:bitmap, bitmap), do: bitmap

defp numberize(:map, bdd) do
bdd_map(bdd, fn bdd_leaf(tag, fields) ->
bdd_map_positive(bdd, fn bdd_leaf(tag, fields) ->
bdd_leaf_new(
tag,
numberize_map_tag(tag),
fields_map(fn _key, {value, optional?} -> {numberize(value), optional?} end, fields)
)
end)
end

defp numberize(:tuple, bdd) do
bdd_map(bdd, fn bdd_leaf(tag, fields) -> bdd_leaf_new(tag, Enum.map(fields, &numberize/1)) end)
bdd_map_positive(bdd, fn bdd_leaf(tag, fields) ->
bdd_leaf_new(tag, Enum.map(fields, &numberize/1))
end)
end

defp numberize(:list, bdd) do
bdd_map(bdd, fn bdd_leaf(head, tail) -> bdd_leaf_new(numberize(head), numberize(tail)) end)
bdd_map_positive(bdd, fn bdd_leaf(head, tail) ->
bdd_leaf_new(numberize(head), numberize(tail))
end)
end

# Map keys are compared exactly by `==`, only their values coerce, so the
# domain keys are kept as is and only the types they point to are widened.
defp numberize_map_tag(domains) when is_list(domains),
do: fields_map(fn _key, value -> numberize(value) end, domains)

defp numberize_map_tag(tag), do: tag

@doc """
Returns if the type is a singleton.
"""
Expand Down Expand Up @@ -6167,6 +6178,39 @@ defmodule Module.Types.Descr do
end
end

# Like `bdd_map/2`, but only rewrites leaves in *positive* position.
#
# `bdd_map/2` is polarity-blind: on `A and not B` it rewrites `B` too, so a
# widening `fun` shrinks the result instead of enlarging it (`numberize/1`
# replacing `not {float()}` by `not {number()}` would drop `{1}` from the
# result even though `{1} == {1.0}`). Whenever `fun` changes a negated leaf,
# we drop the negation altogether: over-approximating is the safe direction
# for widening callers. Negations left untouched by `fun` are preserved,
# so the common negation-free case keeps its exact shape.
defp bdd_map_positive(bdd, fun) do
case bdd do
:bdd_bot ->
:bdd_bot

:bdd_top ->
:bdd_top

bdd_leaf(_, _) = leaf ->
fun.(leaf)

{_, leaf, left, union, right} ->
left = bdd_map_positive(left, fun)
union = bdd_map_positive(union, fun)
right = bdd_map_positive(right, fun)

case fun.(leaf) do
^leaf -> bdd_node_new(leaf, left, union, right)
new_leaf when right == :bdd_bot -> bdd_node_new(new_leaf, left, union, :bdd_bot)
new_leaf -> bdd_union(bdd_intersection(new_leaf, left), bdd_union(union, right))

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Now I am thinking... isn't our bdd_map inherently wrong because it may rewrite the leafs which means they have a different ordering? I am thinking everything needs to be written as in this formula... which would also make numberize too expensive...

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I recall one of AI reviews flagged the order not being preserved as an issue. I wasn’t able to produce code where it would surface as an evident bug. I dismissed the proposed fix with BDD rebuilds everywhere as a bad tradeoff

end
end
end

defp bdd_reduce(bdd, acc, fun) do
case bdd do
:bdd_bot ->
Expand Down
34 changes: 34 additions & 0 deletions lib/elixir/test/elixir/module/types/descr_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -2737,6 +2737,40 @@ defmodule Module.Types.DescrTest do
assert dynamic(list(binary(), float())) |> numberize() ==
dynamic(list(binary(), number()))
end

test "with domain keys" do
# `==` compares map keys exactly but coerces values, so only the types
# the domain keys point to are widened.
assert closed_map([{domain_key(:integer), integer()}]) |> numberize() ==
closed_map([{domain_key(:integer), number()}])

assert open_map([{domain_key(:tuple), tuple([float()])}, {:a, {integer(), false}}])
|> numberize() ==
open_map([{domain_key(:tuple), tuple([number()])}, {:a, {number(), false}}])
end

test "with negations" do
# Negations must not be widened: `{1}` belongs to `term() and not {float()}`
# and `{1} == {1.0}`, so both must survive numberize.
negated = opt_difference(term(), tuple([float()]))
assert subtype?(tuple([integer()]), numberize(negated))
assert subtype?(tuple([float()]), numberize(negated))

negated = opt_difference(non_empty_list(integer(), atom()), non_empty_list(float(), atom()))
assert subtype?(non_empty_list(integer(), atom()), numberize(negated))
assert subtype?(non_empty_list(float(), atom()), numberize(negated))

negated = opt_difference(open_map(a: {integer(), false}), open_map(a: {float(), false}))
assert subtype?(open_map(a: {integer(), false}), numberize(negated))
assert subtype?(open_map(a: {float(), false}), numberize(negated))

# Negations untouched by numberize are kept as is
type = opt_difference(tuple(), tuple([binary()]))
assert numberize(type) == type

type = opt_difference(list(integer(), atom()), list(binary(), atom()))
assert numberize(type) == opt_difference(list(number(), atom()), list(binary(), atom()))
end
end

describe "map_get" do
Expand Down
43 changes: 43 additions & 0 deletions lib/elixir/test/elixir/module/types/expr_test.exs
Original file line number Diff line number Diff line change
Expand Up @@ -2094,6 +2094,49 @@ defmodule Module.Types.ExprTest do
atom([:non_empty_map, :maybe_empty_map])
end

test "does not discard equal values when narrowing against negated types" do
# `other` carries a negation (`... and not {float()}`) from the clause
# subtraction. Widening integers/floats inside that negation would wrongly
# remove `{1}`, even though `{1} == {1.0}` at runtime.
assert typecheck!(
[v, q],
(
other =
case v do
{a} when is_float(a) -> {:float, a}
other -> other
end

w = if q, do: {1}, else: {1.5}

case w do
x when x == other -> {:matched, x}
_ -> :nomatch
end
)
)
|> to_quoted_string() ==
"dynamic({:matched, {float() or integer()}}) or :nomatch"
end

test "does not discard equal values when narrowing against domain keys" do
# `==` coerces map values, so narrowing `x` from `x == y` must widen the
# `integer() => integer()` domain value to `integer() => number()`.
assert typecheck!(
(
y = %{1 => 1}
w = %{1 => 1.0}

case w do
x when x == y and map_size(x) == 1 -> {:eq, x}
_ -> :ne
end
)
)
|> to_quoted_string() ==
":ne or {:eq, %{integer() => float()} and not empty_map()}"
end

test "consider external variables as not precise" do
assert typecheck!(
[x],
Expand Down
Loading