UnionAll wrapper not eq anymore to free UnionAll when Type lifted - is it a bug or not?

General Usage
, ,
1

Let’s define

struct A{U,V} end

and observe some equalities on data

using Test

@test A == A{U,V} where {U,V}
@test Type{A} == Type{A{U,V} where {U,V}}

@test A === A{U,V} where {U,V}
@test Type{A} === Type{A{U,V} where {U,V}}

they are mapped to equalities on functions with those data instance argument

f(::A) = :a
@test methods(f) |> length == 1 # clean up your env if needed
@test f(A{:foo,:bar}()) == :a

f(::A{U,V}) where {U,V} = :a_u_v
@test methods(f) |> length == 1
@test f(A{:foo,:bar}()) == :a_u_v

But are not mapped to equalities on functions with those data type argument

F(::Type{A}) = :A
@test methods(F) |> length == 1 # clean up your env if needed

F(::Type{A{U,V}}) where {U,V} = :A_U_V
@test_broken methods(F) |> length == 1
@test_broken methods(F) |> length != 2

Shouldn’t they be undistinguished both at instance and type level ?

2

these are not needed, comparison between types is always ===.

the two F definitions are different, namely:

julia> F(A)
:A

julia> F(A{Float64, Int})
:A_U_V

by having {U, V}, you’re demanding the type A to be parameterized instead of left floating, this is basically:

julia> Vector{Int} == Vector{U} where U
false

you can even get more methods by only letting one of the parameters floating:

julia> F(::Type{A{U,Int}}) where {U} = :A_U_Int
F (generic function with 3 methods)

julia> length(methods(F))
3
3

OK for === trivial. Let’s forget it (that was a filler :slight_smile: )

You specialize thing to Int and try to generalize it again but awkwardly. Once you bind it, it’s not the same anymore. That do not follow logical construction. I don’t know what 's “left floating”. float @ More about types · The Julia Language only concerns Float32 and Float64

@test Vector{Int} != Vector{U} where U # of course
@test Vector{Int} != Vector # and also
@test Vector{Int} <: Vector{U} where U
@test Vector{Int} <: Vector

My point was not to demonstrate that you can not define more methods (your len==3), of course you can.
It is to assert the unicity of the one that is fully unbound. It’s constructed thru an iterated union, so finitely, and must be unique, either at the instance level (done) and at the type level (not already done) since every finite lattice is complete.

4

floating as oppose to “fixed”