Typing unsoundness

[chethega]

Sorry if dup. Tested on semi-recent 1.3 master and 1.1.

julia> tp1=Pair{T,S} where T<:S<:T where T
Pair{T,S} where T<:S<:T where T

julia> tp2 = Pair{T,T} where T
Pair{T,T} where T

julia> arr2=tp2{Int}[]; arr1=tp1{Int}[];

julia> typeof(arr1)==typeof(arr2)
true

julia> resize!(arr2, 5)
5-element Array{Pair{Int64,Int64},1}:
 139763282708144 => 1              
          561156 => 1              
               1 => 139763280596592
 139763282549136 => 139763282689552
              -1 => 139763289321360

julia> resize!(arr1, 5)
5-element Array{Pair{Int64,S} where Int64<:S<:Int64,1}:
 #undef
 #undef
 #undef
 #undef
 #undef

julia> arr1 .= arr2

signal (11): Segmentation fault

[chethega]

I think that the deeper issue is that we need to look at T===S, i.e. considering T==S is not enough. That is, we need to better distinguish between "weak/semantic equality" of types (x isa T1 provably equivalent to x isa T2 in some incomplete proof system hidden in the bowels of julia; this is almost useless for end-users) and "strong / representational equality" of types (e.g. typetag in invariant position compares equal under memcmp; this is what end-users care about). These should coincide for all concrete inhabited types, i.e. typeof(a)==typeof(b) should be equivalent to both having identical types. Further, Foo{t1} == Foo{t2} in invariant position should be equivalent to t1===t2, i.e. to strong / representational equality of t1 and t2.

Full normalization (i.e. making == and === coincide) would be very cool for this. Can we weaken the proof system (i.e. strengthen the subtype relation) such that this becomes feasible, without breaking too much stuff? Regarding performance, one would hope that normalization is only needed at compile time.

[chethega]

Ok, dup of #31696, sorry for not finding that issue before.

[JeffBezanson]

Full normalization would be great. It seems difficult though, and might require expanding tuples of unions. For now just normalizing out vars with equal bounds would help.