Type inference for Nothing does not always follow the usual rules. According to Martin Odersky:
If a type variable
Xwith an upper bound needs to be instantiated, and the lower bound isNothing, the upper bound is taken instead.
The quote above comes from the discussion on the issue I opened about it because I thought it was a compiler bug.
I do not know the use cases for the exceptional treatment of Nothing when it comes to type inference. However, my language design sense tells me that such ad-hoc rules usually do more harm than good.
It superficially reminds me of void in Java that has to be treated differently from other types, rather than being recognized as the regular Unit type. The latter is of course much worse, as it does not only affect type inference.
Still, I hope it is not too late to fix this irregularity in the Scala 3 type inference logic.
Below is a motivating toy example (already mentioned in this discussion) illustrating how the ad-hoc inference rule for Nothing can be detrimental in practice:
// This code represents part of the HOAS of an object language
// (let's call it OL) using Scala types.
// Upper bound of all Scala types used to represent syntactic sorts of OL
sealed trait CodeType
// Upper bound of all Scala types used to represent types in OL
sealed trait ValTop
// Lower bound of all Scala types used to represent types in OL
type ValBot = Nothing
// Note that Nothing is the only expressible valid lower bound.
// Scala type to represent OL expressions
sealed trait Expr[+T <: ValTop] extends CodeType
// Scala type to represent OL patterns
sealed trait Ptrn[+P <: N, -N <: ValTop] extends CodeType
// Scala type to represent OL values
// Values are expressions, and can also be used in patterns.
sealed trait Val[+T <: ValTop] extends Expr[T], Ptrn[T, ValTop]
// Scala type to represent OL cell references
// Example of a higher-kinded type with an invariant parameter
final case class CellRef[T <: ValTop](name: String) extends ValTop, Val[CellRef[T]]
// Due to invariance, no other lower bound is expressible.
// Scala type to represent OL pairs
final case class Pair[+T1 <: ValTop, +T2 <: ValTop](
t1: Val[T1],
t2: Val[T2],
) extends ValTop, Val[Pair[T1, T2]]
// Scala type to represent an OL wildcard pattern
case object Ignore extends Ptrn[ValBot, ValTop]
type Ignore = Ignore.type
// Scala type to represent OL pair patterns
final case class MatchPair[
+P1 <: N1,
+P2 <: N2,
-N1 <: ValTop,
-N2 <: ValTop,
+L <: Pair[P1, P2],
-U >: Pair[N1, N2] <: ValTop,
](
t1: Ptrn[P1, N1],
t2: Ptrn[P2, N2],
)(using
// This additional constraint represents the unification
// equation L | Pair[ValBot, ValBot] == Pair[P1, P2],
// meant to define the variable L.
Pair[P1, P2] <:< (L | Pair[ValBot, ValBot]),
// This additional constraint represents the unification
// equation U & Pair[ValTop, ValTop] == Pair[N1, N2],
// meant to define the variable U.
(U & Pair[ValTop, ValTop]) <:< Pair[N1, N2],
) extends Ptrn[L, U]
// Because of the abnormal treatment of Nothing by Scala, this pattern cannot be
// expressed without explicitly specifying the type arguments.
val pattern: Ptrn[ValBot, ValTop] = MatchPair[
ValBot, // Boilerplate due to irregular type inference
ValBot, // Boilerplate due to irregular type inference
ValTop, // Boilerplate due to irregular type inference
ValTop, // Boilerplate due to irregular type inference
ValBot, // Boilerplate due to irregular type inference
ValTop, // Boilerplate due to irregular type inference
](Ignore, Ignore)
