Inference of union type instead of Seq

In following code the compiler infers the type of c as a List of union type:

val c = if (true)
  List((Seq.empty, Seq.empty[Seq[String]]))
else
  List.empty[(Seq[String], List[Seq[String]])]

This is what Metals show me as a type of c:

List[(Seq[Nothing], Seq[Seq[String]]) | (Seq[String], List[Seq[String]])]

While this is technically correct, why is compiler not inferring it as a simpler form below?

List[(Seq[String], Seq[Seq[String]])]
1 Like

If you provide a type parameter for the first Seq.empty then it does what you want:

But yeah that’s not the point I guess :smiley:

To answer the question… I don’t know either. Here’s my guess:

I guess it’s because it doesn’t want to automatically choose the wider type.
It’s true that Nothing <: String; and Seq is covariant,
so Seq[Nothing] <: Seq[String].
Also Tuple2 is covariant in both arguments. Therefore:
(Seq[Nothing], Seq[Seq[String]]) <: (Seq[String], Seq[Seq[String]]).

But in the true branch, the type is narrower / more specific, so maybe it doesn’t want to lose that “sharper” (more specific) type information?

That would be my reasoning :wink:

It also works if both 2nd elems of the tuples are Seq[Seq[...]]:

I believe the reason is that:

Seq[Nothing] <: Seq[String] // and not >:
// but
Seq[T] >: List[T] // and not <:, true in general, but in this case, T = Seq[String]

We can therefore simplify the relation to:

type B      // Seq[String]
type A <: B // Seq[Nothing]

type Y      //  Seq[Seq[String]]
type X <: Y // List[Seq[String]]

The question then becomes:

(A, Y) | (B, X)
=?=
(B, Y)

And the answer is no, because (B, Y) is a strict supertype of (A, Y) | (B, X):

  • (B, Y) is a strict supertype of (A, Y), as B is a strict supertype of A
  • (B, Y) is a strict supertype of (B, X), as Y is a strict supertype of X
  • It is therefore a strict supertype of their union

I believe the substitution seems so intuitively true (even though it is false) stems from the following:

(T, U) | (Z, V) =/= ( (T | Z), (U | V) )

(But the former is a subtype of the latter)

2 Likes

Oh and the type-checker should in general only replace things which are equivalent (=:=), as otherwise it becomes either unsound or imprecise

1 Like

Ah, it’s the List in the second one! I see. :+1: