Type inference issue: No ClassTag available for Nothing

[allanrenucci]

import scala.reflect.ClassTag

class Test {
  def foo[T <: String: ClassTag](f: T => Int) = 1
  def bar(f: String => Int) = foo(f)
}

-- Error: tests/allan/Test.scala:27:36 -----------------------------------------
27 |  def bar(f: String => Int) = foo(f)
   |                                    ^
   |                                    No ClassTag available for Nothing
one error found

[smarter]

This isn't specific to ClassTag:

trait Inv[T]

class Test {
  implicit def inv[T]: Inv[T] = ???
  
  def foo[T <: String](f: T => Int)(implicit ev: Inv[T]) = 1
  def bar(f: String => Int) = foo(f) // Infer T := Nothing in Dotty, T := String in Scala 2
}

When we do the implicit search we need to either pick the lower or upper bound of T >: Nothing <: String, since neither of these bounds is more precise than the declared bounds, and since T appears invariantly in Inv[T] we pick the lower bound. This can be fixed by adding more special cases to type inference, though that's not very satisfying, e.g. "prefer the upper bound when inferring a ClassTag".

[smarter]

Turns out that Inferencing#interpolateTypeVars already has logic to avoid instantiating to the lower bound when it's Nothing: b4805bf, but the same logic is not used for Inferencing#IsFullyDefinedAccumulator. Just for consistency it'd make sense to do the same, that would solve this issue.

More generally we may want to revisit how we do instantiation for the variables present in the type of an implicit parameter, right now the following give different results (rest of the code is in the previous comment):

// ...
def bar(f: String => Int) = foo(f)
def bar2(f: String => Int) = foo(f)(implicitly)

I can't think of a good rule of thumb that wouldn't have this behavior right now.

[smarter]

I can't think of a good rule of thumb that wouldn't have this behavior right now.

So here's the current rule, more or less: "Before doing an implicit search for a type I, find all type variables that occur in I and that have appeared in the type of a prefix of the current tree, then instantiate them using the normal rules for instantiation", currently the rules are:

  /** The accumulator which forces type variables using the policy encoded in `force`
   *  and returns whether the type is fully defined. The direction in which
   *  a type variable is instantiated is determined as follows:
   *   1. T is minimized if the constraint over T is only from below (i.e.
   *      constrained lower bound != given lower bound and
   *      constrained upper bound == given upper bound).
   *   2. T is maximized if the constraint over T is only from above (i.e.
   *      constrained upper bound != given upper bound and
   *      constrained lower bound == given lower bound).
   *  If (1) and (2) do not apply:
   *   3. T is maximized if it appears only contravariantly in the given type.
   *   4. T is minimized in all other cases.

If a type variable has appeared in the type of a prefix, rule 1. or 2. usually apply. But they don't always unfortunately, e.g in:

trait Inv[T]

class Test {
  implicit val x: String = ""

  def foo[T <: String](f: T => Int)(implicit g: T): T => Int = f 
  def foo2[T](f: T => Int)(implicit g: T): T => Int = f
  def bar(f: String => Int) = foo(f)
    // We will instantiate T because it appears in the type of foo[T]
    // T := Nothing because constrained upper bound (String) == given upper bound (String), rule 2 does not apply.

  def bar2(f: String => Int) = foo2(f)
    //  We will instantiate T because it appears in the type of foo2[T]
    // T := String because constrained upper bound (String) != given upper bound (Any), rule 2 does apply.

Given more precise bounds to a type parameter can make type inference worse, this is pretty unintuitive.

I think this could be solved if we somehow recorded the fact that we did a comparison T <:< String (T upper bound has been "touched"). Even though it did not constraint T further, this still seems like a good reason to infer T := String. If we did this we could also simplify the way we look for type variables to instantiate before doing the implicit search, right now we need to do a tree traversal: https://github.com/lampepfl/dotty/blob/69b539c41585ee952dd88a6164c2a75c1b868a98/compiler/src/dotty/tools/dotc/typer/Inferencing.scala#L214-L222
But instead we could just collect all the type variables that have been "touched", this would also mean that we collect and solve the same type variables whether or not we write (implicitly) like in the example in my previous comment.

[smarter]

I think this could be solved if we somehow recorded the fact that we did a comparison T <:< String

Here's how this could be implemented: instead of using a TypeBounds to store the bounds of a constraint, use a MemoryTypeBounds that remembers if one if its bound has been touched, and instead of derivedTypeBounds use updateLo and updateHi:

  class MemoryTypeBounds(lo: Type, hi: Type, loTouched: Boolean = false, hiTouched: Boolean = false)
      extends TypeBounds(lo, hi) {
    val touched = loTouched || hiTouched

    def updateLo(lo: Type) = {
      if (lo == this.lo && loTouched) this
      else new MemoryTypeBounds(lo, hi, loTouched = true, hiTouched)
    }
    def updateHi(hi: Type) = {
      if (hi == this.hi && hiTouched) this
      else new MemoryTypeBounds(lo, hi, loTouched, hiTouched = true)
    }
  }

[abeln]

def bar(f: String => Int) = foo(f)
def bar2(f: String => Int) = foo(f)(implicitly)

From what I understood, we infer foo[Nothing] in the first call because the compiler has to "complete" the type of foo before searching for the implicit parameter, which leads to the set of rules in IsFullyDefinedAccumulator applying and so we end up with Nothing (as opposed to "normally" inferring that the type parameter X in foo is bounded by Nothing <: X <: String, so we should choose X = String because X appears contravariantly).

Does that sound right?

What's different in the bar2 call, though? How does implicitly affect things?

[abeln]

@smarter I tried implementing your first suggestion (changing IsFullyDefinedAccumulator to not pick the lower bound when it's Nothing) like so:

           else {
-            val minimize =
-              force.minimizeAll ||
-              variance >= 0 && !(
-                !force.allowBottom &&
-                defn.isBottomType(ctx.typeComparer.approximation(tvar.origin, fromBelow = true)))
+            val minimize = {
+              val isLowerBoundBot = defn.isBottomType(ctx.typeComparer.approximation(tvar.origin, fromBelow = true))
+              val invAndBot = variance == 0 && isLowerBoundBot
+              lazy val invOrCov = variance >= 0 && !(!force.allowBottom && isLowerBoundBot)
+              !invAndBot && (force.minimizeAll || invOrCov)
+            }
             if (minimize) instantiate(tvar, fromBelow = true)
             else toMaximize = true
           }

However, tests/run/typelevel3.scala fails because we infer the type Typed[Any] (as opposed to Typed[Nothing]) for the non-existing element of an HList:

    def zs5: Typed[Any] = 
      /* inlined from Test.index(Test.zsv, 5) */ 
        {
          Typed.apply[Any](
            {
              val xs: 
                
                  HCons[String, 
                    HCons[String, HCons[Boolean, HCons[Double, HNil$]]]
                  ]
                
               = Test.zsv.tail
              val xs: HCons[String, HCons[Boolean, HCons[Double, HNil$]]] = 
                xs.tail
              val xs: HCons[Boolean, HCons[Double, HNil$]] = xs.tail
              val xs: HCons[Double, HNil$] = xs.tail
              val xs: HNil$ = xs.tail
              xs.head
            }
          )
        }

Which I think happens because Typed is in invariant and index returns an existential: https://github.com/lampepfl/dotty/blob/master/tests/run/typelevel3.scala#L38

Does this seem like a case where we should choose the lower bound, even if it's Nothing?

[abeln]

@smarter friendly ping

[Blaisorblade]

@abeln IMHO (FWIW) it does seem like you should infer Nothing there: if you call Typed.apply on Nothing you should get Typed.apply[Nothing]. index isn't quite returning an existential — the application is meant to be retypechecked after expansion, so that should be read as an unconstrained return type. But I don't think the code you're changing has enough info to perform the right choice, so it seems unfortunate that IsFullyDefinedAccumulator gets to pick the argument for Typed.apply. But no clue on what's the reason (if this only happens with transparent, maybe a bug there?).

[smarter]

index returns an existential

Don't be tricked by the type signature, on a transparent def it only serves as an upper bound (see https://github.com/lampepfl/dotty/blob/master/docs/docs/typelevel.md).

I haven't looked at it in details but the failing test looks weird. Do we really want to typecheck code that produces values of type Nothing? Shouldn't we get a compiler error when a transparent call expands to something like that instead?

In any case, I don't think my first suggestion was great. I would rather go in the other direction and drop all special cases involving Nothing in inference in favor of the second approach I outlined.

[odersky]

Is fixed in master