`UnionAll` types violate observational equivalence for `egal` (`===`) objects

[topolarity]

julia> T1 = TypeVar(:T);
julia> T2 = TypeVar(:T);
julia> TT1 = UnionAll(T1, Tuple{T1})
Tuple{T} where T

julia> TT2 = UnionAll(T2, Tuple{T2})
Tuple{T} where T

julia> TT1 === TT2
true

For these types, Base.unwrap_unionall is clearly non consistent but is marked as such:

julia> Base.unwrap_unionall(TT1) === Base.unwrap_unionall(TT2)
false

julia> Base.infer_effects(Base.unwrap_unionall, (Type{TT1},))
(+c,+e,+n,+t,+s,+m,+u)

[oscardssmith]

it's much weirder than that.

julia> objectid(TT1)
0xda12ac8fd4db99e3

julia> objectid(TT2)
0xda12ac8fd4db99e3

julia> objectid(TT2.body)
0x0d495eccbd8d7532

julia> objectid(TT1.body)
0xa84320db54f6eb75

[topolarity]

That behavior seems required by the doc-comment for objectid:

help?> Base.objectid
  objectid(x) -> UInt

  Get a hash value for x based on object identity.

  If x === y then objectid(x) == objectid(y), and usually when x !== y, objectid(x) != objectid(y).

  See also hash, IdDict.

So your observation is just that:

julia> TT1 === TT2 && TT1.body !== TT2.body
true

which I do find intuitively very surprising as a definition for egality.

It certainly disagrees with the statement that "no program can distinguish x and y, if x === y", and it seems to imply that === is not sufficient for inlining/substituting an object in IR - you have to also prove that it is used only :consistent-ly.

But the effects are at least correct in that case:

julia> Base.infer_effects(Core.getfield, (Type{TT1}, Symbol))
(!c,+e,!n,+t,+s,+m,+i)

[oscardssmith]

those effects are just because you haven't told it what the symbol is.

julia> f(x) = x.body
f (generic function with 1 method)

julia> Base.infer_effects(f, (Type{TT1},))
(+c,+e,!n,+t,+s,+m,+u)