Type inference for `Nothing`

does not always follow the usual rules. According to Martin Odersky:

If a type variable

`X`

with an upper bound needs to be instantiated, and the lower bound is`Nothing`

, 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)
```