Julia: Inference incorrectly infers `Nothing` and then incorrectly removes generated code

[blegat]

Consider the following two codes

using Polyhedra
h = HyperPlane([0, 1], 1) ∩ HyperPlane([0, 1], -1)
hh = hyperplanes(h)
let
    i = 0
    for a in hh
        i += 1
    end
    println(i)
end

and

using Polyhedra
h = HyperPlane([0, 1], 1) ∩ HyperPlane([0, 1], -1)
let
    i = 0
    for a in hyperplanes(h)
        i += 1
    end
    println(i)
end

They re equivalent however the first one prints 2 while the second one prints 0.
Note that when the first one is wrapped inside a function, it also prints 2.

I have tried to debug the second code with gdb and it seems that the error is in typeinf_ext.
The input of typeinf_ext is the following MethodInstance:

Main.<toplevel thunk> -> Core.CodeInfo(code=Array{Any, (17,)}[
  Core.SlotNumber(id=1) = 0,
  Expr(:call, Main.hyperplanes, Main.h),
  Core.SlotNumber(id=2) = Expr(:call, Base.iterate, SSAValue(2)),
  Expr(:call, Core.:(===), Core.SlotNumber(id=2), nothing),
  Expr(:call, Base.not_int, SSAValue(4)),
  Expr(:gotoifnot, SSAValue(5), 16),
  Core.SlotNumber(id=2),
  Core.SlotNumber(id=3) = Expr(:call, Core.getfield, SSAValue(7), 1),
  Expr(:call, Core.getfield, SSAValue(7), 2),
  Core.SlotNumber(id=1) = Expr(:call, Main.:(+), Core.SlotNumber(id=1), 1),
  Core.SlotNumber(id=2) = Expr(:call, Base.iterate, SSAValue(2), SSAValue(9)),
  Expr(:call, Core.:(===), Core.SlotNumber(id=2), nothing),
  Expr(:call, Base.not_int, SSAValue(12)),
  Expr(:gotoifnot, SSAValue(13), 16),
  goto 7,
  Expr(:call, Main.println, Core.SlotNumber(id=1)),
  Expr(:return, SSAValue(16))], codelocs=Array{Int32, (17,)}[1, 2, 2, 2, 2, 2, 2, 2, 2, 3, 3, 3, 3, 3, 3, 4, 4], method_for_inference_limit_heuristics=nothing, ssavaluetypes=17, linetable=Array{Any, (4,)}[
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=4, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=5, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=6, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=8, inlined_at=0)], ssaflags=Array{UInt8, (0,)}[], slotflags=Array{UInt8, (3,)}[0x00, 0x00, 0x10], slotnames=Array{Any, (3,)}[
  :i,
  Symbol("#temp#"),
  :a], inferred=false, inlineable=false, propagate_inbounds=false, pure=false)

and the output is the following MethodInstance

Main.<toplevel thunk> -> Core.CodeInfo(code=Array{Any, (5,)}[
  Expr(:call, Main.hyperplanes, Main.h),
  Expr(:call, Base.iterate, SSAValue(1)),
  Core.PiNode(val=0, typ=Int64),
  Expr(:invoke, println(Int64), Main.println, SSAValue(3)),
  Expr(:return, SSAValue(4))], codelocs=Array{Int32, (5,)}[2, 2, 4, 4, 4], method_for_inference_limit_heuristics=nothing, ssavaluetypes=Array{Any, (5,)}[
  Polyhedra.RepIterator{_, _, _} where _ where _ where _,
  Nothing,
  Int64,
  Nothing,
  Any], linetable=Array{Core.LineInfoNode, (4,)}[
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=4, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=5, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=6, inlined_at=0),
  Core.LineInfoNode(mod=Main, method=Symbol("top-level scope"), file=Symbol("/home/blegat/.julia/dev/Polyhedra/ko.jl"), line=8, inlined_at=0)], ssaflags=Array{UInt8, (5,)}[0x00, 0x00, 0x00, 0x00, 0x00], slotflags=Array{UInt8, (0,)}[], slotnames=Array{Any, (0,)}[], inferred=true, inlineable=false, propagate_inbounds=false, pure=false)

What seems to happen is that the return type inferred for Expr(:call, Base.iterate, SSAValue(1)) is Nothing and then all the for the for loop is optimized out.
However, the inference is wrong, it does not always return nothing (otherwise, the first code wouldn't print 2).

I have tried debugging typeinf_ext as follows but the bug does not occur even if the input I give to typeinf_ext seems to be exactly the same.
Any idea ?

Cfr https://github.com/JuliaPolyhedra/Polyhedra.jl/issues/123

[blegat]

I have extracted a minimal failing example from the bug in Polyhedra. It does not require any packages:

abstract type A{T} end
abstract type B{T} end
const C{T} = Union{B{T}, A{T}}
struct MyVec <: B{Int}
    elements::Vector{Int}
end
function startindex(elements::Vector)
    if isempty(elements)
        return nothing
    else
        return 1
    end
end
struct Iterator{PT<:Tuple{C}}
    ps::PT
    function Iterator(ps::PT) where {PT}
        new{PT}(ps)
    end
end
element_and_index(it, idx::Nothing) = nothing
element_and_index(it::Iterator, idx::Int) = it.ps[1].elements[idx], idx
function Base.iterate(it::Iterator{Tuple{T}}) where {T}
    idx = startindex(it.ps[1].elements)
    return element_and_index(it, idx)
end

h = MyVec([1])
let
    i = 0
    for a in Iterator((h,))
        i += 1 # never gets executed
    end
    println(i) # Prints 0 instead of 1
end

It seems that every element is important in this example. Whenever I try to simplify it, the bug disappears :-P

[StefanKarpinski]

Thank you, @blegat, for reducing the example. That's tremendously helpful!

[martinholters]

Further reduction:

julia> struct Foo end

julia> struct Bar{PT<:Tuple{Foo}}
           function Bar(ps::PT) where {PT}
               new{PT}()
           end
       end

julia> baz(it::Bar) = "baz called"
baz (generic function with 1 method)

julia> bork1(it::Bar{Tuple{T}}) where {T} = return baz(it)
bork1 (generic function with 1 method)

julia> bork2(it::Bar{Tuple{T}}) where {T<:Foo} = return baz(it)
bork2 (generic function with 1 method)

julia> h = Foo()
Foo()

julia> bar = Bar((h,))
Bar{Tuple{Foo}}()

julia> # this is OK:
       code_warntype(bork1, Tuple{typeof(bar)})
Body::String
1 1 ─     return "baz called"                                                                       │

julia> # but if h could not be inferred in Bar((h,)), bar is inferred as
       T_bar = Core.Compiler.return_type(Bar, Tuple{Tuple{Any}})
Bar{_1} where _1

julia> bar isa T_bar
true

julia> # and this is not OK:
       code_warntype(bork1, Tuple{T_bar})
Body::Union{}
1 1 ─     (Main.baz)(it)                                                                            │
  └──     $(Expr(:unreachable))                                                                     │

julia> # although
       code_warntype(baz, Tuple{T_bar})
Body::String
1 1 ─     return "baz called"                                                                       │

julia> # OTOH, this is OK:
       code_warntype(bork2, Tuple{T_bar})
Body::String
1 1 ─     return "baz called"     

[martinholters]

As an aside, inference of apply_type in

julia> code_warntype(Bar, Tuple{Tuple{Any}})
Body::Bar{_1} where _1
3 1 ─ %1 = (Core.apply_type)(Main.Bar, $(Expr(:static_parameter, 1)))::Type{Bar{_1}} where _1       │
  │   %2 = %new(%1)::Bar{_1} where _1                                                               │
  └──      return %2  

could probably be improved to Type{Bar{T}} where T<:Tuple{Foo}, which would presumable also solve this particular example, but not the underlying issue.

[martinholters]

Hm, I have a branch where Bar(::Tuple{Any}) is inferred as Bar{_1} where _1<:Tuple{Foo} which looks good to me. But I noticed (and this is the case on master, too):

julia> methods(bork1, Tuple{Bar{_1} where _1<:Tuple{Foo}})
# 0 methods for generic function "bork1":

Huh?
OTOH:

julia> methods(bork1, Tuple{Bar{_1} where _1<:Tuple{Any}})
# 1 method for generic function "bork1":
[1] bork1(it::Bar{Tuple{T}}) where T in Main at REPL[5]:1

This is consistent with

julia> typeintersect(Bar{Tuple{T}} where T, Bar{_1} where _1<:Tuple{Foo})
Union{}

julia> typeintersect(Bar{Tuple{T}} where T, Bar{_1} where _1<:Tuple{Any})
Bar{Tuple{T}} where T

where I'd expect the former to yield Bar{Tuple{T}} where T<:Foo.

[martinholters]

I've dug a bit into the type intersection bug (which I suspect to be at least related to the underlying cause here) and when calling typeintersect(Bar{Tuple{T}} where T, Bar{_1} where _1<:Tuple{Foo}), after peeling off the outer stuff, we end up in intersect_invariant(Tuple{T}, _1<:Tuple{Foo}). Here, the recursive intersection correctly yields Tuple{Foo}, but only updates the environment to fix _1 at Tuple{Foo}, while T is left at Union{} <: T <: Any. Then the check that Tuple{T} is a subtype of Tuple{Foo} in the environment fails, and the intersection is assumed to be empty. Can you take a look at this, @JeffBezanson?

[martinholters]

Verified that when looking up matching methods during inference, the intersection between Tuple{typeof(baz), Bar{Tuple{T}} where T} and Tuple{typeof(baz), Bar{PT} where PT<:Tuple{Foo}} is wrongly computed as Union{}, making inference miss the method.

[JeffBezanson]

Should be fixed by #31747, but please confirm with the original example if possible.