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 ?

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

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.