Explicit concrete type constraint in UnionAll

[martinholters]

We allow UnionAlls to constrain the bound type variable to concrete types, but only implicitly by the diagonal rule. E.g. in Tuple{T,T} where T, T can only be a concrete type. Sometimes, it would be helpful if this constraint could be enabled explicitly. Two examples from the top of my head:

1. Inference of typeof(x) if x could not be inferred exactly. Say, x is only inferred as Number, then typeof(x) is inferred as Type{T} where T<:Number. Obviously, T here could be constrained to a concrete type, if UnionAll allowed that. (I vaguely remember an issue where inference considering f(::Type{Union{}}) for f(typeof(x)) came as a bit of a surprise.)
2. Type intersection:

julia> T1 = Tuple{T,T,Ref} where T
Tuple{T,T,Ref} where T

julia> T2 = Tuple{T,T,Ref{T}} where T
Tuple{T,T,Ref{T}} where T

julia> R = typeintersect(T1, T2)
Tuple{T,T,Ref{T1}} where T1 where T

julia> R <: T2
false

There presently is no way to express the intersection (which would be Tuple{T,T,Ref{T}} where T with T concrete). (Expert question: would this and #29368 suffice to make our type system closed under intersection?)

Notably, it seems much less useful the other way round, i.e. to allow a typevar to take an abstract type, even if it falls under the diagonal rule. Nevertheless, I'd imagine this to be implemented by an extra Bool field in TypeVar or UnionAll, indicating whether abstract types are allowed.

We probably also would want to provide some syntax (in addition to directly calling the TypeVar or UnionAll constructor). However, if we choose the default behavior of the where clause to match the current diagonal rule, I'm not sure how often that would actually be needed in user code. So we might get away with a construct like foo(x::Ref{T}) where !abstract T.

[StefanKarpinski]

This type appears to be a subset of the intersection of T1 and T2:

julia> T3 = Tuple{T,T,Ref{>:T}} where T
Tuple{T,T,Ref{#s1} where #s1>:T} where T

julia> T3 <: T1
true

julia> T3 <: T2
true

That seems correct: if t = (a, b, c) isa T3 then the following facts hold:

1. c isa Ref{S} where S >: T
2. T == typeof(a) == typeof(b) since the T only appears in covariant positions.
3. a isa S and b isa S since S >: T

Therefore, we know that t isa T1 and t isa T2. In the other direction, given t = (a, b, Ref{S}(c)) such that t isa T1 and t isa T2 then we can take T = typeof(a) and #s1 = S and we can see that t isa T3. So I'm fairly sure that T3 is exactly the intersection of T1 and T2.

Note, however, that T3 is larger than the proposed T4 = Tuple{T,T,Ref{T}} where !abstract T since T3 allows the type parameter of the Ref to be abstract whereas T4 does not.

I'm not sure if this alleviates the need for this feature or not. It does, however, seem that typeintersect(T1, T2) should return T3 rather than R which is too big.

[martinholters]

Hm, yes, that seems correct. Amazing. Makes me wonder whether there is a case where intersection actually does need this feature.

[chethega]

I really like this. If we permit concreteness bounds, then this could be used to get internally rid of the diagonal rule, and simplify everything, right? I.e. the diagonal Tuple{T,T} where T<: AbstractS would become Tuple{T,T} where T<: concrete(AbstractS) during lowering. In other words, we would multiply the nondiagonal typelattice with a single bit for concreteness; or, in even different words, we allow limited multiple inheritance: One base can be arbitrary, and the other can be out of the hardcoded list [concrete].

If we are at it, I'd like to also multiply the type-lattice with singleton <: bitstype <: immutable and mutable. Dispatching on mutability is very natural, and dispatching on bitstype and singletons allows various optimizations.

I'm not sure about syntax; retiring the diagonal syntax for e.g. Tuple{T,T} where T<: concrete(AbstractS) would be massively breaking, but might be something for 2.0.

[goretkin]

Not having thought it through, here are two possible ideas:

• Instead of just TypeVar, introduce ConcreteTypeVar, with only an ub field?
• Introduce a kind of bottom type that is only a subtype of concrete types (unlike Union{}), and use that as the lb in a TypeVar

Syntax that would not require introducing any new identifiers or keywords or parsing support:
Type{T} where isconcretetype(T)

at the cost of possibly giving the impression that arbitrary predicates can take the role of isconcretetype.