Type inference difficulties with UndefOr[A | B]

[armanbilge]

Compiler version

3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY

Minimized code

UndefOr is based on the Scala.js concept:

https://github.com/scala-js/scala-js/blob/058532aa8c504b76431b40e3e1b51b2cdef87643/library/src/main/scala/scala/scalajs/js/package.scala#L85

The minimized example below demonstrates a common situation when working with Scala.js facades.

//> using scala "3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY"

type UndefOr[A] = A | Unit

extension [A](maybe: UndefOr[A])
  def foreach(f: A => Unit): Unit =
    maybe match
      case () => ()
      case a: A => f(a)

trait Foo
trait Bar

object Baz:
  var booBap: Foo | Bar = _

def z: UndefOr[Foo | Bar] = ???

@main
def main =
  z.foreach(x => Baz.booBap = x)

Output

$ scala-cli compile test.scala 
Compiling project (Scala 3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY, JVM)
[error] ./test.scala:21:31: Found:    (x : Object)
[error] Required: Foo | Bar
[error]   z.foreach(x => Baz.booBap = x)
[error]                               ^
Error compiling project (Scala 3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY, JVM)
Compilation failed

Expectation

If we add an explicit type annotation to the last line:

- z.foreach(x => Baz.booBap = x)
+ z.foreach((x: Foo | Bar) => Baz.booBap = x)

then it compiles ok:

$ scala-cli compile test.scala 
Compiling project (Scala 3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY, JVM)
[warn] ./test.scala:9:12: the type test for A cannot be checked at runtime
[warn]       case a: A => f(a)
[warn]            ^
Compiled project (Scala 3.1.3-RC1-bin-20220323-fb7f900-NIGHTLY, JVM)

Is it possible for the compiler to make this inference by itself?

[rmgk]

Basically it does not seem to infer sub parts of a union. Smaller example:

scala> def test[A](v: A | Unit): A | Unit =  v
 
scala> test(5: Int | Unit)
val res7: Int | Unit = 5

scala> test(5: String | Int | Unit)
val res8: Matchable | Unit = 5

[odersky]

That's by design. Too much would break otherwise. We are still looking for a way to make precise type variable inference an opt-in feature. But it won't work for existing library functions such as foreach.

[smarter]

I'm not sure if this is according to design actually:

scala> def id[A](v: A): A =  v
def id[A](v: A): A

scala> id(5: Int | Unit)
val res0: Int | Unit = 5

scala> id(5: String | Int | Unit)
val res1: String | Int | Unit = 5

scala> def test[A](v: A | Unit): A | Unit =  v
def test[A](v: A | Unit): A | Unit

scala> test(5: Int | Unit)
val res2: Int | Unit = 5

scala> test(5: String | Int | Unit)
val res3: Matchable | Unit = 5

we manage to keep the hard union when instantiating the type variable of id, but not when instantiating the type variable of test. I assume this has something to do with the order in which we do subtyping checks, but it doesn't seem like a conscious choice.

[armanbilge]

Polite bump on this. No promises/timelines of course, but any gut feelings whether this might be fixed/improved? Have to decide between rewriting some large facades to workaround this or deferring the Scala 3 migration for now. Thanks!

[smarter]

I don't personally have the time to work on anything for the next few months.

[armanbilge]

Right, I don't expect anyone to work on this anytime soon. More the heart of my question is, is this "by-design" as suggested in #14770 (comment)? Because if so then we should just cut our losses :)

[smarter]

I don't think it's by design, we have some logic to try to preserve hard unions (that is: unions written by the user rather than inferred) through type inference already:
https://github.com/lampepfl/dotty/blob/6540ad9154797164561281080b6a4e24a191691d/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L470-L478
But this is fragile: it only kicks in when the rhs of the type comparison is a type variable or an intersection type, whereas here the rhs is a union type (but one side of the union is also part of the lhs union, and the other is a type variable). More generally, I think this code is problematic since it means we record unions in lower bounds of type variables which violates the precondition of addConstraint:
https://github.com/lampepfl/dotty/blob/6540ad9154797164561281080b6a4e24a191691d/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala#L651-L658
A possible alternative would be to add a Mode flag (or boolean var) we would set in TypeComparer to tell the ConstraintHandling logic to create hard unions instead of soft unions when refining a lower bound:
https://github.com/lampepfl/dotty/blob/6540ad9154797164561281080b6a4e24a191691d/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala#L266
(Type#| creates soft unions by default)

(This might also help with other issues where we currently don't preserve unions: #14494)
/cc @mbovel