Confusion about type constraints in where clauses

General Usage
,
1

Why this

julia> g(::Type{S}, ::Type{T}) where {T, S>:T} = (S,T)
g (generic function with 1 method)

julia> g(Integer, Int)
ERROR: UndefVarError: `S` not defined in static parameter matching
Suggestion: run Test.detect_unbound_args to detect method arguments that do not fully constrain a type parameter.
Stacktrace:
 [1] g(::Type{Integer}, ::Type{Int64})
   @ Main ./REPL[5]:1
 [2] top-level scope
   @ REPL[6]:1

julia> Test.detect_unbound_args(Main)
0-element Vector{Method}

yet what appears to be an equivalent definition produces the expected result?

julia> h(::Type{S}, ::Type{T}) where {S, T<:S} = (S,T)
h (generic function with 1 method)

julia> h(Integer, Int)
(Integer, Int64)

The documentation on UnionAll types allows both <: and >: in where clauses, but it’s not clear what will and won’t work. The syntax is a little confusing because in one where clause you’re both quantifying over a type variable and constraining it. In a where clause that contains two type variables like above, is there a syntactic rule about which is being quantified over and which is just there as the other side of the constraint? What about a where clause like where {S<:T<:U}?

2 Likes
2

The where {T, S>:T} clause in the first g imposes constraints on the type parameters:

  • T is an unconstrained type parameter.
  • S must be a supertype of T.

Integer is a supertype of Int64, which is why the second g works differently.

1 Like
3

Note: I’ve edited the original post so that “first g” is just g and “second g” is now h.

I don’t follow the explanation.

In g, T is unconstrained and S must be a supertype of T. The call g(Integer, Int) should bind T to Int and then S to Integer should it not? And then certainly Integer>:Int. So what’s wrong? Why am I getting an UndefVarError for S?

In h, S is unconstrained and T must be a subtype of S. The call h(Integer, Int) should bind S to Integer and then T to Int, and then certainly Int<:Integer.

g(Int,Integer) and h(Int,Integer) both correctly give a MethodError since Int>:Integer and Integer<:Int are both false. No UndefVarErrors occur.

How are the two formulations g and h different exactly? If I say S can be anything but T<:S, how is that different from saying T can be anything but S>:T? Don’t exactly the same pairs of types satisfy both statements?

If it has something to do with order of binding of type variables to types, e.g. it happens left-to-right across the method signature instead of outside to in according to the where clauses, then in g(Integer,Int) S would bind to Integer and then T is supposed to be unconstrained but we’ve also got a constraint on it S>:T so… some kind of problem happens.

But in that case g(Int,Integer) should fail in the same way shouldn’t it, with an UndefVarError for S, instead of giving a MethodError?

4

That looks symmetric, but it is not, because in g S is the free choice and T is restricted, whereas in h T is the free choice and S is restricted, so order matters. Although there is the same set, the procedure differs.

1 Like
5

To write out the implicit constraints, the logical conjunctions Union{}<:S<:Any ^ Union{}<:T<:S<:Any and Union{}<:T<:Any ^ Union{}<:T<:S<:Any both appear to result in Union{}<:T<:S<:Any. However, type constraints in where clauses aren’t logical constraints or sets being input into commutative operators. For one, order matters, e.g. where {T<:S, S} errors at definition.

Thing is, the nature of where clause constraints aren’t directly related to why S is undefined despite succesful dispatch (if it helps to evade the UndefVarError to illustrate that, return (@isdefined(S), @isdefined(T)) instead). My intuition would be that S = Integer must have been considered for dispatch, so I don’t know why it’s not in the method body, nor have I seen a rule for it.

1 Like