error in type inference, causes either a crash or silently wrong results depending on Julia version

[nsajko]

The bug:

• does not appear on v1.9
• manifests on v1.10 as a crash, like so:

  ERROR: LoadError: fatal error in type inference (type bound)
  Stacktrace:
   [1] from_base_rational_checked
     @ ~/reproducer/reproducer.jl:406 [inlined]
   [2] Main.LazyMinus.TypeDomainRational(x::Rational{Int64})
     @ Main.BaseOverloads ~/reproducer/reproducer.jl:409
   [3] top-level scope
     @ ~/reproducer/reproducer.jl:413
  

• manifests on v1.11 and up as a silently wrong result

For all Julia versions the correct behavior is obtained with --compile=min.

Reproducer:

module NonnegativeIntegers
export
    NonnegativeInteger, type_assert_nonnegative_integer,
    new_nonnegative_integer, NaturalNumberTuple
const NaturalNumberTuple = Tuple{Vararg{Nothing,N}} where {N}
struct NonnegativeInteger{
    N,
    NaturalNumberTuple{N} <: Tup <: NaturalNumberTuple,
} <: Integer
    global function new_nonnegative_integer(::Type{NonnegativeInteger{N}}) where {N}
        Tup = NaturalNumberTuple{N}
        new{N,Tup}()
    end
end
function new_nonnegative_integer(n::Int)
    new_nonnegative_integer(NonnegativeInteger{n})
end
function type_assert_nonnegative_integer(@nospecialize x::NonnegativeInteger)
    x
end
end

module PositiveIntegers
using ..NonnegativeIntegers
export
    PositiveInteger, type_assert_positive_integer,
    NonnegativeInteger, new_nonnegative_integer,
    natural_successor, natural_predecessor,
    PositiveIntegerUpperBound, NonnegativeIntegerUpperBound
const PositiveInteger = NonnegativeInteger{N,Tup} where {
    N,
    NaturalNumberTuple{N} <: Tup <: Tuple{Nothing,Vararg{Nothing}},
}
function type_assert_positive_integer(@nospecialize x::PositiveInteger)
    x
end
function natural_successor(::NonnegativeInteger{N}) where {N}
    new_nonnegative_integer(N + 1)
end
function natural_predecessor(::PositiveInteger{N}) where {N}
    new_nonnegative_integer(N - 1)
end
const PositiveIntegerUpperBound = PositiveInteger
const NonnegativeIntegerUpperBound = NonnegativeInteger
end

module IntegersGreaterThanOne
using ..NonnegativeIntegers, ..PositiveIntegers
export
    IntegerGreaterThanOne, IntegerGreaterThanOneUpperBound,
    type_assert_integer_greater_than_one
const IntegerGreaterThanOne = NonnegativeInteger{N,Tup} where {
    N,
    NaturalNumberTuple{N} <: Tup <: Tuple{Nothing,Nothing,Vararg{Nothing}},
}
const IntegerGreaterThanOneUpperBound = IntegerGreaterThanOne
function type_assert_integer_greater_than_one(@nospecialize x::IntegerGreaterThanOne)
    x
end
end

module NonintegralRationalsGreaterThanOne
module RecursiveStep
using ....IntegersGreaterThanOne
export recursive_step
function recursive_step(@nospecialize t::Type)
    Union{IntegerGreaterThanOne,t}
end
end
const NonintegralRationalGreaterThanOneUpperBound = Real
const NonintegralRationalGreaterThanOneUpperBoundTighter = Real
using .RecursiveStep, ..PositiveIntegers, ..IntegersGreaterThanOne
export
    NonintegralRationalGreaterThanOne, NonintegralRationalGreaterThanOneUpperBound,
    new_nonintegral_rational_greater_than_one,
    RationalGreaterThanOne, RationalGreaterThanOneUpperBound,
    type_assert_rational_greater_than_one
struct NonintegralRationalGreaterThanOne{  # regular continued fraction with positive integer part XXX
    IntegerPart<:PositiveInteger,
    FractionalPartDenominator<:recursive_step(NonintegralRationalGreaterThanOneUpperBoundTighter),
} <: NonintegralRationalGreaterThanOneUpperBoundTighter
    integer_part::IntegerPart
    fractional_part_denominator::FractionalPartDenominator
    global function new_nonintegral_rational_greater_than_one(i::I, f::F) where {
        I<:PositiveInteger,
        F<:recursive_step(NonintegralRationalGreaterThanOne),
    }
        r = new{I,F}(i, f)
        type_assert_nonintegral_rational_greater_than_one(r)
    end
end
function type_assert_nonintegral_rational_greater_than_one(@nospecialize x::NonintegralRationalGreaterThanOne)
    x
end
const RationalGreaterThanOne = Union{IntegerGreaterThanOne,NonintegralRationalGreaterThanOne}
const RationalGreaterThanOneUpperBound = Union{IntegerGreaterThanOneUpperBound,NonintegralRationalGreaterThanOneUpperBound}
function type_assert_rational_greater_than_one(@nospecialize x::RationalGreaterThanOne)
    x
end
end

module NonintegralRationalsBetweenZeroAndOne
using ..IntegersGreaterThanOne, ..NonintegralRationalsGreaterThanOne
export
    NonintegralRationalBetweenZeroAndOne, NonintegralRationalBetweenZeroAndOneUpperBound,
    new_nonintegral_rational_between_zero_and_one
struct NonintegralRationalBetweenZeroAndOne{  # regular continued fraction with zero integer part XXX
    Denominator<:RationalGreaterThanOne,
} <: Real
    denominator::Denominator
    global function new_nonintegral_rational_between_zero_and_one(d::D) where {
        D<:RationalGreaterThanOne,
    }
        new{D}(d)
    end
end
const NonintegralRationalBetweenZeroAndOneUpperBound = NonintegralRationalBetweenZeroAndOne{<:Any}
end

module PositiveNonintegralRationals
using ..PositiveIntegers, ..NonintegralRationalsGreaterThanOne, ..NonintegralRationalsBetweenZeroAndOne
export
    PositiveNonintegralRational, PositiveNonintegralRationalUpperBound, NonnegativeRational,
    PositiveRational, PositiveRationalUpperBound
const PositiveNonintegralRational = Union{NonintegralRationalBetweenZeroAndOne,NonintegralRationalGreaterThanOne}
const PositiveNonintegralRationalUpperBound = Union{NonintegralRationalBetweenZeroAndOneUpperBound,NonintegralRationalGreaterThanOneUpperBound}
const NonnegativeRational = Union{NonnegativeInteger,PositiveNonintegralRational}
const PositiveRational = Union{PositiveInteger,PositiveNonintegralRational}
const PositiveRationalUpperBound = Union{PositiveIntegerUpperBound,PositiveNonintegralRationalUpperBound}
end

module FractionalPartDenominator
using
    ..NonintegralRationalsGreaterThanOne,
    ..NonintegralRationalsBetweenZeroAndOne, ..PositiveNonintegralRationals
export fractional_part_denominator
function fractional_part_denominator_gt1(x::NonintegralRationalGreaterThanOne)
    type_assert_rational_greater_than_one(getfield(x, :fractional_part_denominator))
end
function fractional_part_denominator(x::PositiveNonintegralRational)
    if x isa NonintegralRationalBetweenZeroAndOne
        getfield(x, :denominator)
    else
        fractional_part_denominator_gt1(x)
    end
end
end

module LazyMinus
using ..PositiveIntegers, ..PositiveNonintegralRationals
export
    NegativeInteger, NegativeIntegerUpperBound,
    TypeDomainInteger, TypeDomainIntegerUpperBound,
    NonzeroInteger, NonzeroIntegerUpperBound,
    NegativeNonintegralRational, NegativeNonintegralRationalUpperBound,
    NegativeRational, NegativeRationalUpperBound,
    NonintegralRational, NonintegralRationalUpperBound,
    TypeDomainRational, TypeDomainRationalUpperBound,
    NonzeroRational, NonzeroRationalUpperBound,
    negated, absolute_value_of
struct NegativeInteger{X<:PositiveInteger} <: Integer
    x::X
    global function new_negative_integer(x::X) where {X<:PositiveInteger}
        new{X}(x)
    end
end
const NegativeIntegerUpperBound = NegativeInteger{<:Any}
struct NegativeNonintegralRational{X<:PositiveNonintegralRational} <: Real
    x::X
    global function new_negative_nonintegral_rational(x::X) where {X<:PositiveNonintegralRational}
        new{X}(x)
    end
end
const NegativeNonintegralRationalUpperBound = NegativeNonintegralRational{<:Any}
const NegativeRational = Union{NegativeInteger,NegativeNonintegralRational}
const NegativeRationalUpperBound = Union{NegativeIntegerUpperBound,NegativeNonintegralRationalUpperBound}
const NonintegralRational = Union{NegativeNonintegralRational,PositiveNonintegralRational}
const NonintegralRationalUpperBound = Union{NegativeNonintegralRationalUpperBound,PositiveNonintegralRationalUpperBound}
const TypeDomainInteger = Union{NonnegativeInteger,NegativeInteger}
const TypeDomainIntegerUpperBound = Union{NonnegativeIntegerUpperBound,NegativeIntegerUpperBound}
const TypeDomainRational = Union{TypeDomainInteger,NonintegralRational}
const TypeDomainRationalUpperBound = Union{TypeDomainIntegerUpperBound,NonintegralRationalUpperBound}
const NonzeroInteger = Union{NegativeInteger,PositiveInteger}
const NonzeroIntegerUpperBound = Union{NegativeIntegerUpperBound,PositiveIntegerUpperBound}
const NonzeroRational = Union{NonzeroInteger,NonintegralRational}
const NonzeroRationalUpperBound = Union{NonzeroIntegerUpperBound,NonintegralRationalUpperBound}
function new_negative(x::PositiveRational)
    if x isa Integer
        new_negative_integer(x)
    else
        new_negative_nonintegral_rational(x)
    end
end
function negated_nonnegative(n::NonnegativeRational)
    if n isa PositiveRationalUpperBound
        new_negative(n)
    else
        new_nonnegative_integer(0)
    end
end
function negated(n::TypeDomainRational)
    if n isa NegativeRational
        getfield(n, :x)
    else
        negated_nonnegative(n)
    end
end
function absolute_value_of(n::TypeDomainRational)
    if n isa NegativeRational
        getfield(n, :x)
    else
        n
    end
end
end

module MultiplicativeInverse
using
    ..PositiveIntegers, ..NonintegralRationalsGreaterThanOne,
    ..NonintegralRationalsBetweenZeroAndOne, ..PositiveNonintegralRationals,
    ..LazyMinus, ..FractionalPartDenominator
export multiplicative_inverse
function multiplicative_inverse_positive_integer(x::PositiveInteger)
    p = natural_predecessor(x)
    if p isa PositiveIntegerUpperBound
        new_nonintegral_rational_between_zero_and_one(x)
    else
        new_nonnegative_integer(1)
    end
end
function multiplicative_inverse_positive_noninteger(x::PositiveNonintegralRational)
    if x isa NonintegralRationalBetweenZeroAndOne
        fractional_part_denominator(x)
    else
        new_nonintegral_rational_between_zero_and_one(x)
    end
end
function multiplicative_inverse_positive(x::PositiveRational)
    if x isa Integer
        multiplicative_inverse_positive_integer(x)
    else
        multiplicative_inverse_positive_noninteger(x)
    end
end
function multiplicative_inverse(x::NonzeroRational)
    a = absolute_value_of(x)
    i = multiplicative_inverse_positive(a)
    if x isa NegativeRational
        negated(i)
    else
        i
    end
end
end

module RecursiveAlgorithms
using ..PositiveIntegers, ..IntegersGreaterThanOne
export
    added, from_abs_int, is_even_nonnegative, multiplied, is_less_nonnegative,
    subtracted_nonnegative,
    euclidean_division_quotient, euclidean_division_remainder
function is_less_nonnegative(::NonnegativeInteger{L}, ::NonnegativeInteger{R}) where {L,R}
    L < R
end
function from_abs_int(n::Int)
    new_nonnegative_integer(abs(n))
end
function subtracted_nonnegative(::NonnegativeInteger{L}, ::NonnegativeInteger{R}) where {L, R}
    new_nonnegative_integer(L - R)
end
Base.@assume_effects :foldable function euclidean_division_quotient(num::NonnegativeInteger, den::PositiveInteger)
    if is_less_nonnegative(num, den)
        new_nonnegative_integer(0)
    else
        let n = subtracted_nonnegative(num, den), quo = euclidean_division_quotient(n, den)
            natural_successor(quo)
        end
    end
end
function euclidean_division_remainder(::NonnegativeInteger{L}, ::PositiveInteger{R}) where {L, R}
    new_nonnegative_integer(L % R)
end
end

module DivisionForIntegers
using
    ..PositiveIntegers, ..IntegersGreaterThanOne, ..NonintegralRationalsGreaterThanOne,
    ..LazyMinus, ..MultiplicativeInverse, ..RecursiveAlgorithms
export division_for_integers
Base.@assume_effects :foldable function division_gt1(num::PositiveInteger, den::PositiveInteger)
    quo = euclidean_division_quotient(num, den)
    quo = type_assert_positive_integer(quo)
    rem = euclidean_division_remainder(num, den)
    if rem isa PositiveIntegerUpperBound
        let fdp = division_gt1(den, rem)
            new_nonintegral_rational_greater_than_one(quo, fdp)
        end
    else
        type_assert_integer_greater_than_one(quo)
    end
end
function division_between_0_and_1(num::PositiveInteger, den::PositiveInteger)
    i = division_gt1(den, num)
    multiplicative_inverse(i)
end
function division_nonnegative(num::NonnegativeInteger, den::PositiveInteger)
    z = new_nonnegative_integer(0)
    if num isa PositiveIntegerUpperBound
        if num === den
            natural_successor(z)
        else
            if is_less_nonnegative(num, den)
                division_between_0_and_1(num, den)
            else
                division_gt1(num, den)
            end
        end
    else
        z
    end
end
function division_for_integers(num::TypeDomainInteger, den::NonzeroInteger)
    anum = absolute_value_of(num)
    aden = absolute_value_of(den)
    cf = division_nonnegative(anum, aden)
    if (num isa NegativeInteger) === (den isa NegativeInteger)
        cf
    else
        negated(cf)
    end
end
end

module Conversion
using ..PositiveIntegers, ..LazyMinus, ..RecursiveAlgorithms
export
    tdi_to_int, tdi_from_int,
    tdi_to_x, tdi_from_x,
    tdi_to_x_with_extra
function tdi_from_int(i::Int)
    n = from_abs_int(i)
    if signbit(i)
        negated(n)
    else
        n
    end
end
function tdi_from_bool(i::Bool)
    z = new_nonnegative_integer(0)
    if i
        natural_successor(z)
    else
        z
    end
end
function tdi_to_x(x::Type, n::TypeDomainInteger)
    i = tdi_to_int(n)
    x(i)
end
function tdi_to_x_with_extra(x::Type, n::TypeDomainInteger, e)
    i = tdi_to_int(n)
    x(i, e)
end
function x_to_int(x)
    t = Int  # presumably wide enough for any type domain integer
    t(x)::t
end
function tdi_from_x(x)
    if x isa Bool
        tdi_from_bool(x)
    else
        let i = x_to_int(x)
            tdi_from_int(i)
        end
    end
end
end

module BaseOverloads
using
    ..PositiveIntegers, ..RecursiveAlgorithms, ..LazyMinus, ..MultiplicativeInverse,
    ..NonintegralRationalsGreaterThanOne,
    ..NonintegralRationalsBetweenZeroAndOne, ..DivisionForIntegers, ..Conversion
function identity_conversion(::Type{T}, x::TypeDomainRational) where {T<:TypeDomainRational}
    if x isa T
        x
    else
        throw(InexactError(:convert, T, x))
    end
end
function to_tdi(x::Number)
    if !isinteger(x)
        throw(InexactError(:convert, TypeDomainInteger, x))
    end
    tdi_from_x(x)
end
function from_base_rational(x::Rational)
    num = numerator(x)
    den = denominator(x)
    num_tdi = to_tdi(num)
    den_tdi = to_tdi(den)
    division_for_integers(num_tdi, den_tdi)
end
function from_base_rational_checked(::Type{T}, x::Rational) where {T<:TypeDomainRational}
    q = from_base_rational(x)
    identity_conversion(T, q)
end
function (::Type{T})(x::Rational) where {T<:TypeDomainRational}
    from_base_rational_checked(T, x)
end
end

n = LazyMinus.TypeDomainRational(5//1)
display(n)

[KristofferC]

On 1.10, this reduced to

const a = Tuple{Vararg{Nothing,d}} where d
struct b{d, a{d} <: e <: a}
    global function c(::Type{b{d}}) where d
        e = a{d}
        new{d,e}()
    end
end
c(f) = c(b{f})
h = b{d,e} where {d, e<:Tuple{Nothing}}
r(::b{t}) where t = t
function ae(an, ao::h)
    if an isa h
        an == a ? a : r(ao)
    end
end
ai(::aj, c) where aj = z
function ap(::aj, l) where aj
    an = ao = signbit(l) ? nothing : c(l)
    m = ae(an, ao)
    ai(aj, m)
end
function (::Type{aj})(l) where aj
    ap(aj, l)
end
h(1)

but the

function (::Type{aj})(l) where aj
    ap(aj, l)
end

signature is a bit fishy so not sure it is a 100% proper reduction. On 1.10 and 1.11 this gives

ERROR: LoadError: UndefVarError: `z` not defined in `Main`

[vtjnash]

Reduces more to this type intersect error (verified on master and v1.10), depending on the order of the typeintersect arguments to it:

julia> const a = Tuple{Vararg{Nothing,d}} where d
NTuple{d, Nothing} where d

julia> struct b{d, a{d} <: e <: a} end

julia> const h = b{d,e} where {d, e<:Tuple{Nothing}}

julia> typeintersect(b{t, e} where Tuple{Vararg{Nothing, t}}<:e<:(Tuple{Vararg{Nothing, d}} where d) where t, h)
b{1, Tuple{Nothing}}

julia> typeintersect(h, b{t, e} where Tuple{Vararg{Nothing, t}}<:e<:(Tuple{Vararg{Nothing, d}} where d) where t)
Union{}

[vtjnash]

Also confirmed this is not a new regression (last seen correct in v1.2), just an unwise way to write code in any version (the julia type system is not especially well-suited to proving arbitrary properties)

[nsajko]

Some other inaccurate typeintersect results:

julia> struct NonnegativeStrict{N, NTuple{N, Nothing} <: Tup <: NTuple{N, Nothing}} end

julia> const Positive = NonnegativeStrict{N, Tup} where {N, NTuple{N, Nothing} <: Tup <: Tuple{Nothing, Vararg{Nothing}}}
Positive{N} where N (alias for NonnegativeStrict{N, Tup} where {N, NTuple{N, Nothing}<:Tup<:Tuple{Nothing, Vararg{Nothing}}})

julia> typeintersect(NonnegativeStrict, Positive)  # buggy, see counterexample below
Union{}

julia> typeintersect(Positive, NonnegativeStrict)  # same
Union{}

julia> counterexample = NonnegativeStrict{1, Tuple{Nothing}}
NonnegativeStrict{1, Tuple{Nothing}}

julia> counterexample <: NonnegativeStrict
true

julia> counterexample <: Positive
true