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
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
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.