A most harrowing collection of Julia WATs

EDIT: this is now fixed (in a PR, soon to be merged, I guess). See Intransitivities in subtyping

It’s AFAIK not possible, even in theory, to implement the subtyping (<:) so that it always returns true when a human would expect that.

The discussion in this issue is relevant: suboptimal subtyping for `UnionAll` and `Union` · Issue #52818 · JuliaLang/julia · GitHub

Quoting vtjnash, emphasis mine:

The type system is generally permitted to return false whenever it wants to, provided only that it preserves transitivity.

You might also be interested in the Julia subtyping paper:

Julia Subtyping: A Rational Reconstruction . Proceedings of the ACM on Programming Languages, 2018, 27, ⟨10.1145/3276483⟩. ⟨hal-01882137


Unprovable judgments. Julia’s subtype algorithm, and in turn our formalization, cannot prove all judgments expected to hold.

This is actually a recent bug, introduced in v1.10, see "Tuple field type cannot be Union{}" error in 1.10rc · Issue #52385 · JuliaLang/julia · GitHub