Under explicit nulls, remove the rule Null <:< x.type.

The specified rule that `Null <:< x.type` when the underlying type
`U` of `x` is nullable is dubious to begin with. Under explicit
nulls, it becomes decidedly out of place. We now disable that rule
under `-Yexplicit-nulls`.

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -912,7 +912,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
                 // scala.AnyRef [Scala 3: which scala.Null conforms to], the type denotes the set of values consisting
                 // of null and the value denoted by p (i.e., the value v for which v eq p). [Otherwise,] the type
                 // denotes the set consisting of only the value denoted by p.
-                isNullable(tp.underlying) && tp.isStable
+                !ctx.explicitNulls && isNullable(tp.underlying) && tp.isStable
               case tp: RefinedOrRecType => isNullable(tp.parent)
               case tp: AppliedType => isNullable(tp.tycon)
               case AndType(tp1, tp2) => isNullable(tp1) && isNullable(tp2)

tests/explicit-nulls/neg/i17467.check

@@ -0,0 +1,31 @@
+-- [E007] Type Mismatch Error: tests/explicit-nulls/neg/i17467.scala:4:22 ----------------------------------------------
+4 |    val a2: a1.type = null // error
+  |                      ^^^^
+  |                      Found:    Null
+  |                      Required: (a1 : String)
+  |                      Note that implicit conversions were not tried because the result of an implicit conversion
+  |                      must be more specific than (a1 : String)
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/explicit-nulls/neg/i17467.scala:7:22 ----------------------------------------------
+7 |    val b2: b1.type = null // error
+  |                      ^^^^
+  |                      Found:    Null
+  |                      Required: (b1 : String | Null)
+  |                      Note that implicit conversions were not tried because the result of an implicit conversion
+  |                      must be more specific than (b1 : String | Null)
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E172] Type Error: tests/explicit-nulls/neg/i17467.scala:8:28 -------------------------------------------------------
+8 |    summon[Null <:< b1.type] // error
+  |                            ^
+  |                            Cannot prove that Null <:< (b1 : String | Null).
+-- [E007] Type Mismatch Error: tests/explicit-nulls/neg/i17467.scala:14:22 ---------------------------------------------
+14 |    val c2: c1.type = null // error
+   |                      ^^^^
+   |                      Found:    Null
+   |                      Required: (c1 : Null)
+   |                      Note that implicit conversions were not tried because the result of an implicit conversion
+   |                      must be more specific than (c1 : Null)
+   |
+   | longer explanation available when compiling with `-explain`

tests/explicit-nulls/neg/i17467.scala

@@ -0,0 +1,16 @@
+object Test:
+  def test(): Unit =
+    val a1: String = "foo"
+    val a2: a1.type = null // error
+
+    val b1: String | Null = "foo"
+    val b2: b1.type = null // error
+    summon[Null <:< b1.type] // error
+
+    /* The following would be sound, but it would require a specific subtyping
+     * rule (and implementation code) for debatable value. So it is an error.
+     */
+    val c1: Null = null
+    val c2: c1.type = null // error
+  end test
+end Test