automatically generated counterexamples for <: transitivity

[nsajko]

Here's a Git repository containing a Julia package that generates counterexamples to the transitivity property that <: is supposed to satisfy:

https://gitlab.com/nsajko/SubtypingRelationExperiments.jl

So far I tested it on v1.10 and v1.11-DEV: the results between these two versions are the same and may be found under results/. I'll give just two of the counterexamples here, see the rest on my repo:

This is the first counterexample in the results:

counterexample triplet:  (Tuple{X, X} where X<:Union{}, Tuple{C, C}, Tuple{X, X, Vararg{Any}} where C<:X<:C)

In the REPL:

julia> struct C end

julia> const T1 = Tuple{X, X} where X<:Union{}
Tuple{X, X} where X<:Union{}

julia> const T2 = Tuple{C, C}
Tuple{C, C}

julia> const T3 = Tuple{X, X, Vararg{Any}} where C<:X<:C
Tuple{X, X, Vararg{Any}} where C<:X<:C

julia> T1 <: T2 <: T3
true

julia> T1 <: T3
false

This is the last counterexample in the results:

counterexample triplet:  (Tuple{A, X, Vararg{X}} where X<:C, Tuple{Any, Vararg{C}}, Tuple{Any, Vararg{X}} where X>:C)

In the REPL:

julia> abstract type A end

julia> struct C <: A end

julia> const T1 = Tuple{A, X, Vararg{X}} where X<:C
Tuple{A, X, Vararg{X}} where X<:C

julia> const T2 = Tuple{Any, Vararg{C}}
Tuple{Any, Vararg{C}}

julia> const T3 = Tuple{Any, Vararg{X}} where X>:C
Tuple{Any, Vararg{X}} where X>:C

julia> T1 <: T2 <: T3
true

julia> T1 <: T3
false

[nsajko]

Not a regression: the output is the same as above (true for T1 <: T2 <: T3, false for T1 <: T3) on all Julia versions since v0.6.1. EDIT: only checked this for the two examples above, there are much more examples in my repo that I didn't take a look at.

[vtjnash]

These appear to be variations on #24166

[nsajko]

After fixing a bug in my experiment, there are now 6035 counterexamples (before there were only 95).

[N5N3]

Looks similar to the 2nd problem mentioned in #24174 (comment).
The lb of ∃X get messed after simple_union (Union{C, ∀X<:C} or Union{C, ∀X<:Union{}} is not concrete).
We could add more normalization path for these cases. But at present Union doesn't do that.
So perhaps it should also be undated.

[nsajko]

@N5N3 said:

The remaining might no be caused by diagonal check.
I guess an assertation build is helpful here to figure out if some of these failure comes from obvious_subtype optimization.

I downloaded an assert build artifact, and, indeed, when I run my experiment, an assert, mentioning obvious_subtype, is triggered. I run this:

using SubtypingRelationExperiments
SubtypingRelationExperiments.Main.experiment()

While checking transitivity Julia crashes:

julia: /cache/build/builder-amdci5-1/julialang/julia-master/src/subtype.c:2103: ijl_subtype_env: Assertion `obvious_subtype == 3 || obvious_subtype == subtype || ijl_has_free_typevars(x) || ijl_has_free_typevars(y)' failed.

[48145] signal 6 (-6): Aborted
in expression starting at REPL[2]:1
unknown function (ip: 0x7c86c091083c)
raise at /usr/lib/libc.so.6 (unknown line)
abort at /usr/lib/libc.so.6 (unknown line)
unknown function (ip: 0x7c86c08a83db)
__assert_fail at /usr/lib/libc.so.6 (unknown line)
ijl_subtype_env at /cache/build/builder-amdci5-1/julialang/julia-master/src/subtype.c:2103
jl_f_issubtype at /cache/build/builder-amdci5-1/julialang/julia-master/src/builtins.c:557
default_subtyping_relation at /home/nsajko/src/gitlab.com/nsajko/SubtypingRelationExperiments/src/Main.jl:7 [inlined]
check_transitivity at /home/nsajko/src/gitlab.com/nsajko/SubtypingRelationExperiments/src/RelationChecking.jl:19
unknown function (ip: 0x7c86bf6a5ff3)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
report_preorder at /home/nsajko/src/gitlab.com/nsajko/SubtypingRelationExperiments/src/RelationChecking.jl:72
experiment at /home/nsajko/src/gitlab.com/nsajko/SubtypingRelationExperiments/src/Main.jl:15
unknown function (ip: 0x7c86bf6a274d)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
experiment at /home/nsajko/src/gitlab.com/nsajko/SubtypingRelationExperiments/src/Main.jl:12
unknown function (ip: 0x7c86bf6943bf)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
do_call at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:126
eval_value at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:223
eval_stmt_value at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:174 [inlined]
eval_body at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:657
jl_interpret_toplevel_thunk at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:815
jl_toplevel_eval_flex at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:941
jl_toplevel_eval_flex at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:884
ijl_toplevel_eval_in at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:992
eval at ./boot.jl:428 [inlined]
eval_user_input at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:224
repl_backend_loop at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:320
#start_repl_backend#48 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:305
start_repl_backend at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:302
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
#run_repl#61 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:461
run_repl at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:447
jfptr_run_repl_12782 at /home/nsajko/.julia/compiled/v1.11/REPL/u0gqU_0v1sL.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
#1096 at ./client.jl:440
jfptr_YY.1096_16880 at /home/nsajko/.julia/compiled/v1.11/REPL/u0gqU_0v1sL.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
jl_f__call_latest at /cache/build/builder-amdci5-1/julialang/julia-master/src/builtins.c:875
#invokelatest#2 at ./essentials.jl:1020 [inlined]
invokelatest at ./essentials.jl:1017 [inlined]
run_main_repl at ./client.jl:424
repl_main at ./client.jl:561 [inlined]
_start at ./client.jl:535
jfptr__start_65682.1 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/lib/julia/sys.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
true_main at /cache/build/builder-amdci5-1/julialang/julia-master/src/jlapi.c:947
jl_repl_entrypoint at /cache/build/builder-amdci5-1/julialang/julia-master/src/jlapi.c:1106
main at /cache/build/builder-amdci5-1/julialang/julia-master/cli/loader_exe.c:58
unknown function (ip: 0x7c86c08a9ccf)
__libc_start_main at /usr/lib/libc.so.6 (unknown line)
unknown function (ip: 0x4010b8)
Allocations: 3661979 (Pool: 3661825; Big: 154); GC: 5
Aborted (core dumped)

Version info:

Julia Version 1.11.0-DEV.1367
Commit 91ec2bb646c (2024-01-24 13:20 UTC)
Build Info:
  Official https://julialang.org/ release
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: 8 × AMD Ryzen 3 5300U with Radeon Graphics
  WORD_SIZE: 64
  LLVM: libLLVM-16.0.6 (ORCJIT, znver2)
Threads: 1 default, 0 interactive, 1 GC (on 8 virtual cores)
Environment:
  JULIA_NUM_PRECOMPILE_TASKS = 3
  JULIA_PKG_PRECOMPILE_AUTO = 0

[nsajko]

MRE:

julia> abstract type A end

julia> struct C <: A end

julia> const L = Tuple{Any, Any, Vararg{C}}
Tuple{Any, Any, Vararg{C}}

julia> const R = Tuple{Vararg{X}} where X>:A
Tuple{Vararg{X}} where X>:A

julia> L <: R
julia: /cache/build/builder-amdci5-1/julialang/julia-master/src/subtype.c:2103: ijl_subtype_env: Assertion `obvious_subtype == 3 || obvious_subtype == subtype || ijl_has_free_typevars(x) || ijl_has_free_typevars(y)' failed.

[48664] signal 6 (-6): Aborted
in expression starting at REPL[5]:1
unknown function (ip: 0x7dc39ddc183c)
raise at /usr/lib/libc.so.6 (unknown line)
abort at /usr/lib/libc.so.6 (unknown line)
unknown function (ip: 0x7dc39dd593db)
__assert_fail at /usr/lib/libc.so.6 (unknown line)
ijl_subtype_env at /cache/build/builder-amdci5-1/julialang/julia-master/src/subtype.c:2103
jl_f_issubtype at /cache/build/builder-amdci5-1/julialang/julia-master/src/builtins.c:557
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
do_call at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:126
eval_value at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:223
eval_stmt_value at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:174 [inlined]
eval_body at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:657
jl_interpret_toplevel_thunk at /cache/build/builder-amdci5-1/julialang/julia-master/src/interpreter.c:815
jl_toplevel_eval_flex at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:941
jl_toplevel_eval_flex at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:884
ijl_toplevel_eval_in at /cache/build/builder-amdci5-1/julialang/julia-master/src/toplevel.c:992
eval at ./boot.jl:428 [inlined]
eval_user_input at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:224
repl_backend_loop at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:320
#start_repl_backend#48 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:305
start_repl_backend at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:302
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
#run_repl#61 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:461
run_repl at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/share/julia/stdlib/v1.11/REPL/src/REPL.jl:447
jfptr_run_repl_12782 at /home/nsajko/.julia/compiled/v1.11/REPL/u0gqU_0v1sL.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
#1096 at ./client.jl:440
jfptr_YY.1096_16880 at /home/nsajko/.julia/compiled/v1.11/REPL/u0gqU_0v1sL.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
jl_f__call_latest at /cache/build/builder-amdci5-1/julialang/julia-master/src/builtins.c:875
#invokelatest#2 at ./essentials.jl:1020 [inlined]
invokelatest at ./essentials.jl:1017 [inlined]
run_main_repl at ./client.jl:424
repl_main at ./client.jl:561 [inlined]
_start at ./client.jl:535
jfptr__start_65682.1 at /home/nsajko/tmp/jl/jl/julia-91ec2bb646/lib/julia/sys.so (unknown line)
_jl_invoke at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:2905 [inlined]
ijl_apply_generic at /cache/build/builder-amdci5-1/julialang/julia-master/src/gf.c:3082
jl_apply at /cache/build/builder-amdci5-1/julialang/julia-master/src/julia.h:2154 [inlined]
true_main at /cache/build/builder-amdci5-1/julialang/julia-master/src/jlapi.c:947
jl_repl_entrypoint at /cache/build/builder-amdci5-1/julialang/julia-master/src/jlapi.c:1106
main at /cache/build/builder-amdci5-1/julialang/julia-master/cli/loader_exe.c:58
unknown function (ip: 0x7dc39dd5accf)
__libc_start_main at /usr/lib/libc.so.6 (unknown line)
unknown function (ip: 0x4010b8)
Allocations: 1 (Pool: 1; Big: 0); GC: 0
Aborted (core dumped)