Nothing is inferred as the narrower type for unions in contravariant position

[neko-kai]

Minimized code

trait Rec[-K <: String] { self =>
  protected val map: Map[String, Any]
  type ValueOf[A <: K]
  def get(k: K): ValueOf[k.type] = map(k).asInstanceOf

  def +[K0 <: K, K1 <: String](that: Rec[K1]): Rec[K0 | K1] {
    type ValueOf[A <: K0 | K1] = A match {
      case K0 => self.ValueOf[A]
      case K1 => that.ValueOf[A]
    }
  } = new Rec[K0 | K1] {
    protected val map = self.map ++ that.map
    type ValueOf[A <: K0 | K1] = A match {
      case K0 => self.ValueOf[A]
      case K1 => that.ValueOf[A]
    }
  }
}

object Rec {
  def field[V](s: String & Singleton)(v: V): Rec[s.type] {
    type ValueOf[K <: s.type] = K match {
      case s.type => V
    }
  } = new Rec[s.type] {
    protected val map = Map(s -> v)
    type ValueOf[K <: s.type] = K match {
      case s.type => V
    }
  }
}

def getZ(r: Rec["z"]): r.ValueOf["z"] = r.get("z")

@main def Test = {
  val rec = Rec.field("k")("Str") + (Rec.field("v")(0)) + (Rec.field("z")(true))
//  val rec = Rec.field("k")("Str").+["k", "v"](Rec.field("v")(0)).+["k" | "v", "z"](Rec.field("z")(true)) // this works
  def res1: String  = rec.get("k")
  def res2: Int     = rec.get("v")
  def res3: Boolean  = getZ(rec)

  println((res1, res2, res3))
}

Output

Error:(129, 31) Found:    ("k" : String/T)
Required: Nothing/T |/T ("z" : String/T)
  def res1: String  = rec.get("k")
Error:(130, 31) Found:    ("v" : String/T)
Required: Nothing/T |/T ("z" : String/T)
  def res2: Int     = rec.get("v")

Expectation

Expected it to compile without explicit annotations. This may be related to the deliberate restrictions on inferrence of unions in Dotty.

[smarter]

Minimized example:

trait Rec[-K] {
  def foo[K0 <: K, K1]: Rec[K0] { type Foo[A <: K0] = Int } = ???
}

object Rec {
  val r1: Rec[Int] = ???
  val r2 = r1.foo
  val r3: Rec[Int] = r2 // error: found Rec[Nothing], required: Req[Int]
}

It works if the result type of foo is changed to use a type lambda explicitly:

  def foo[K0 <: K, K1]: Rec[K0] { type Foo <: [A <: K0] =>> Int } = ???

These two definitions should be equivalent but it looks like the first one is actually translated to:

  def foo[K0 <: K, K1]: Rec[K0] { type Foo >:  [A <: K0] =>> Int <: [A <: K0] =>> Int } = ???

which means K0 appears both in covariant and contravariant positions, so type inference decides to minimize it instead of maximizing it.

[smarter]

These two definitions should be equivalent

Wait no, they aren't, I confused it with the case where we only have an upper-bound: https://github.com/lampepfl/dotty/blob/c5a76f0db4c2908520a297414cf59a9a207fb11f/compiler/src/dotty/tools/dotc/core/Types.scala#L3629-L3633 In fact, trying to write this type in the definition of Rec itself leads to a variance error:

trait Rec[-K] {
  type Foo[A <: K] = Int // contravariant type K occurs in invariant position in type [A] = Int of type Foo
}

So unless our handling of variance is incorrect, there's nothing we can do here.

[smarter]

there's nothing we can do here.

I mean, we could come up with some more complicated inference heuristics that would make the compiler choose the other bound when instantiating K0, but I can't think of any reasonable one (other than "avoid picking Nothing" which is an heuristic we try to avoid since it can also lead to issues)

[LPTK]

@smarter any reason Dotty thinks K is in invariant position here?

Both intuition and scalac seem to disagree:

@ class A[-K]{type T[U<:K]}
defined class A

@ class A[-K]{type T[U>:K]}
cmd1.sc:1: contravariant type K occurs in covariant position in type  >: K of type U
class A[-K]{type T[U>:K]}
                   ^
Compilation Failed

[smarter]

scalac agrees if you add a lower-bound or type alias for T:

scala> class A[-K]{ type T[U >: K] = Int }
                           ^
       error: contravariant type K occurs in invariant position in type  >: K of type U

For Dotty, this expands to type T >: [U >: K] =>> Int <: [U >: K] =>> Int

[LPTK]

scalac agrees if you add a lower-bound or type alias for T

What do you mean by "scalac agrees"? The program in question had an upper bound, not a lower bound.

The example you show was already in my message, to make a contrast with the lower bound case, which is accepted by scalac.

My point is that scalac certainly does not agree that this is an invariant position for K, regardless if it's an upper or lower bound.

[smarter]

herm sorry, I meant to post:

scala> class A[-K]{ type T[U <: K] = Int }
                           ^
       error: contravariant type K occurs in invariant position in type  <: K of type U