julia
68b586a6 - subtype: Keep precise track of subtype meets (#61940)

Commit
3 days ago
subtype: Keep precise track of subtype meets (#61940) When subtyping accumulates its constraints on existential vars, it needs to union all lower bound constraints and intersect all upper bound constraints. Currently, this is done with simple_meet (or, if in intersection with the full intersection algorithm). The problem with simple_meet is that it can overapproximate the intersection, which as shown in #61917 can lose constraints and give wrong subtyping answers. The solution is simple: If `simple_meet` cannot compute an exact intersection, allocate a new object that keeps a list of all the constraints. This object is semantically an intersection type. However, our use here is very limited: It only ever occurs in the `ub` of a `varbinding` and thus only ever occurs on the RHS of a subtype query. Fortunately for us, that is the simple direction: `A <: Intersect{X, Y} <=> A <: X && A <: Y`. It's therefore mostly used as a bookkeeping device rather than being a full extention to the type system. However, this PR does style it in such a way that it could be extended to a full typesystem feature in the future if we were so inclined (though I have no present plans to do so). I should also note that the formation of `Intersect` is pretty rare. In the whole Compiler/Base bootstrap, it happens exactly twice out of millions of subtype queries. Fixes #61917. Code by Claude.
Author
Parents
Loading