What is the difference between the types Null and Null & T where T <: AnyRef?

Look at the following method

def toOption[T <: AnyRef](value: T | Null): Option[T] = 
    value match {
        case null => None
        case content: T => Some(content)
    }

If you inspect the content pattern variable, the type is T | T & Null, which I guess is the result of the the intersection of the type of the scrutinee value: T | Null and the type of the matched pattern element: T. What calls my attention is the second operand of the | operator. Shouldn't the T & Null part be simplified to Null by the compiler when T<:AnyRef leaving T | Null as the type of content? What is the difference between the types Null and T & Null?

If the definition of the intersection A & B was that it represents values that are members of both A and B then:

if the values represented by T included null then the set of values that are members of both T and Null would contain only the null value;
if the values represented by T did not include the null then the set of values that are members of both T and Null would be empty (Nothing).

Therefore, T & Null = Null | Nothing = Null when T <: AnyRef.

If the definition of the intersection A & B was that a value conforms to A & B implies that it conforms to both A and B then:

if null conforms to T then only null would conform to both T and Null;
if null does not conform to T then no value would conform to both T and Null.

Therefore T & Null = Null | Nothing = Null when T <: AnyRef.

Am I missing something or the compiler has a bug?

Edit: I forgot to mention that I was using intelliJ for the inspection. Later, to confirm, I used a macro to display which is the type of content according to the compiler, and the result was T. Very different from what the intelliJ inspection shows. I was blaming the compiler for a bug of the intelliJ inspector. Sorry.

Here is the macro:

inline def typeOf[A](a: A): String = ${typeOfMacro[A]('{a})}

def typeOfMacro[A : Type](a: Expr[A])(using q: Quotes): Expr[String] = 
    Expr(q.reflect.TypeRepr.of[A].show)

Anyway, the scala REPL is not simplifying A & Null to Null when A <: AnyRef.

scala> val text: String & Null = null
val text: String & Null = null

So the question still prevails.

Curiously REPL also does not simplify A & Nothing to Nothing either.

Edit 2: According to type theory there is no type X such that A & X is the same to X for any A. So the simplification I expected would be incorrect. REPL is giving the correct type. So the answer to my question is yes, I was missing something.

Solution

Quite a lot of questions, so I'll start from basics.

Scala is based on DOT calculus. In Scala every type T is a type segment [Lower, Upper]. Scala types is a lattice (with respect to <:, &, |): https://en.wikipedia.org/wiki/Lattice_(order)

T <: AnyRef doesn't imply T >: Null, nor vice versa.

T <: AnyRef means the type segment [Nothing, AnyRef]. T >: Null means [Null, Any].

(Nothing <: AnyVal <: Any, Nothing <: Null <: AnyRef <: Any, Nothing != Null != AnyRef != AnyVal != Any.)

AnyRef is the supertype of all reference types. Null is the subtype of all reference types. Null is inhabited only by null.

Nothing is the subtype of all types (including Null: Nothing <: Null, Nothing != Null). It's inhabited by no (normal) values. But being uninhabited by (normal) values doesn't mean that Nothing is uninhabited by anything at all. There are terms of this type: t: Nothing, there are abstract types/type parameters intersecting with this type: T >: Nothing (and in type-level programming types are more important, values, whether they exist or not, are less important), there are not so normal values (divergences, bottom values) like

@tailrec
def infiniteRecursion(): Nothing = infiniteRecursion()

def throwException(): Nothing = throw new RuntimeException("error")

def foo[T <: AnyRef](t: => T): Unit = ()

foo[Nothing](infiniteRecursion()) // compiles, runs, successfully finishes
foo[Nothing](throwException())  // compiles, runs, successfully finishes

def foo[T <: AnyRef](t: T): Unit = ()

foo[Nothing](infiniteRecursion()) // compiles, runs forever
foo[Nothing](throwException()) // compiles, runs, throws exception

If T <: AnyRef implied T >: Null, then foo[Nothing](infiniteRecursion()), foo[Nothing](throwException()) wouldn't compile.

If you want both T <: AnyRef and T >: Null then just specify both type bounds:

def foo[T >: Null <: AnyRef] = ...

Shouldn't the T & Null part be simplified to Null by the compiler when T <: AnyRef

No, it shouldn't. It should when T >: Null (including T >: Null <: AnyRef).

What is the difference between the types Null and T & Null?

If T = Nothing then T & Null = Nothing & Null = Nothing != Null. If T >: Null then T & Null = Null. If T <: Null (i.e. T belongs to the segment [Nothing, Null]) then T & Null = T. If T is just some type then T & Null is just some type <: T and <: Null (actually, the maximal such type), generally different from T and Null.

If the definition of the intersection ...

if the values...

if the values...

I guess we already discussed a year ago that types are not sets (of values):

Why does a self annotated trait is not assignable to the type of self?

https://cs.stackexchange.com/questions/91330/what-exactly-is-the-semantic-difference-between-set-and-type

https://math.stackexchange.com/questions/489369/difference-between-a-type-and-a-set

https://planetmath.org/11typetheoryversussettheory

If two types have equal sets of values of these types, this doesn't make types equal.

For example below types Nat, Succ[N], _0, _1, _2, ... are abstract and have no values. But they are quite different types. If types were sets then all these types Nat, Succ[N], _0, _1, _2, ... would be the same set (namely, the empty set).

type Nat
type _0 <: Nat
type Succ[N <: Nat] <: Nat

trait Add[N <: Nat, M <: Nat] {
  type Out <: Nat
}
object Add {
  type Aux[N <: Nat, M <: Nat, Out0 <: Nat] = Add[N, M] { type Out = Out0 }

  implicit def zeroAdd[M <: Nat]: Aux[_0, M, M] = null
  implicit def succAdd[N <: Nat, M <: Nat](implicit
    add: Add[N, M]
  ): Aux[Succ[N], M, Succ[add.Out]] = null
}

type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
type _5 = Succ[_4]

implicitly[Add.Aux[_2, _3, _5]] // compiles

trait ToInt[N <: Nat] {
  def apply(): Int
}
object ToInt {
  implicit val zeroToInt: ToInt[_0] = () => 0
  implicit def succToInt[N <: Nat](implicit toInt: ToInt[N]): ToInt[Succ[N]] =
    () => toInt() + 1
}

trait AddToInt[N <: Nat, M <: Nat] {
  def apply(): Int
}
object AddToInt {
  implicit def mkAddToInt[N <: Nat, M <: Nat, Sum <: Nat](implicit
    add: Add.Aux[N, M, Sum],
    toInt: ToInt[Sum]
  ): AddToInt[N, M] = () => toInt()
}

def addToInt[N <: Nat, M <: Nat](implicit addToInt: AddToInt[N, M]): Int =
  addToInt()

addToInt[_2, _3] // 5

According to type theory there is no type X such that A & X is the same to X for any A.

Actually, in Scala type system X is Nothing.