regression: ensuring on ???

[olhotak]

My use case is to give students a method with an empty body and a postcondition, and to ask them to complete the body so it satisfies the postcondition:

object test {
   def m(x: Int): Int = {
     ???
   } ensuring(ans => ans == x)
}

This compiles with Dotty 0.7.0 but Dotty master gives:

-- [E008] Member Not Found Error: inferEnsuring.scala:4:5 ----------------------
2 |   def m(x: Int): Int = {
3 |     ???
  |                        ^
  |                        value `ensuring` is not a member of Nothing
one error found

Since ensuring is a member of Int and since Nothing <: Int, ensuring should also be a member of Nothing.

Although the member is injected by an implicit conversion to Ensuring, the same reasoning applies: the implicit conversion applies to every subtype of Any, and Nothing <: Any.

[liufengyun]

Since ensuring is a member of Int and since Nothing <: Int, ensuring should also be a member of Nothing.

This is not the case for Scala when it is related to Null, Nothing.

scala> def f(x: Nothing): Int = x + 3
<console>:11: error: value + is not a member of Nothing
       def f(x: Nothing): Int = x + 3
                                  ^

scala> def f(x: Null): Int = x + 3
<console>:11: error: value + is not a member of Null
       def f(x: Null): Int = x + 3
                               ^

And in some cases GADT bounds:

case class One[T](fst: T)

object Test {
  def bad[T](e: One[T])(x: T): Int = e match {
    case foo: One[Int] =>
      x + 4
  }
}

/cc: @AleksanderBG The code above compiles in Scalac, but not in Dotty.

[odersky]

The behavior on Null and Nothing is as expected. I leave to @AleksanderBG to decide whether the GADT example should compile or not.

[abgruszecki]

Closing as a duplicate of #7044 - we do infer GADT bound T := Int (and we do want to infer it), but member selection on x.+ fails.