Error on type inference

[flomebul]

Compiler version

3.1.3

Minimized code

A similar issue (#11556) was already corrected several month ago (#12847)

object Issue15864:
  type Traverser[-I, +O] = I => LazyList[(O)]
  extension[I, O](ta: Traverser[I, O])
    def ~[P](tb: Traverser[O, P]): Traverser[I, P] = ???

  class Graph { class Node; class Link }
  
  case class Path[+E](e: E)
  type Query[-U, +V] = Traverser[Path[U], Path[V]]

  def nodesQ(using g: Graph): Query[Nothing, g.Node] = ???
  def outsQ(using g: Graph): Query[g.Node, g.Node] = ???

  object aGraph extends Graph
  import aGraph._
  given aGraph.type = aGraph

  val q1: Query[Nothing, Node] = nodesQ ~ (outsQ ~ outsQ)
  implicitly[q1.type <:< Query[Nothing, Node]]

  val q2 = nodesQ ~ (outsQ ~ outsQ)
  implicitly[q2.type <:< Query[Nothing, Node]]

  val q3: Query[Nothing, Node] = q2
end Issue15864

Output

Cannot prove that (asuivre.Issue15864.q2 : 
  asuivre.Issue15864.Traverser[asuivre.Issue15864.Path[Nothing], 
    asuivre.Issue15864.Path[Any]
  ]
) <:< asuivre.Issue15864.Query[Nothing, asuivre.Issue15864.aGraph.Node].
  implicitly[q2.type <:< Query[Nothing, Node]]

Expectation

Supposed to compile without error.

[flomebul]

I take some time to try to minimize at maximum the case :

object Issue15864:
  def op[O, P](ta: List[O], tb: List[P]): List[P] = ???

  class Graph { class Node }
  
  def outsQ(using g: Graph): List[List[g.Node]] = ???

  object aGraph extends Graph
  given aGraph.type = aGraph

  val q1: List[List[aGraph.Node]] = op(outsQ, op(outsQ, outsQ))
  implicitly[q1.type <:< List[List[aGraph.Node]]]

  val q2 = op(outsQ, op(outsQ, outsQ))
  implicitly[q2.type <:< List[List[aGraph.Node]]]

  val q3: List[List[aGraph.Node]] = q2
end Issue15864

And the unexpected error is now

Cannot prove that (asuivre.Issue15864.q2 : List[List[Any]]) <:< List[List[asuivre.Issue15864.aGraph.Node]].
  implicitly[q2.type <:< List[List[aGraph.Node]]]

I hope this can help

[odersky]

I had a closer look at this. What goes on here is that a dependent type variable (param)4 introduced by constrainResult does not occur in the type List[List[Test.implA.Node]]> of Test.outsQ(Test.implA) and therefore is arbitrarily instantiated to the upper bound. But the type variable does appear in the remaining constraint. I see:

interpolate non-occurring (param)4 in TS[72, 12, 1, 0] in Test.outsQ(Test.implA): List[List[Test.implA.Node]], fromBelow = false, qualifying = (param)3, (param)4,  uninstantiated variables: O, P, O, P, (param)3, (param)4
 constrained types: [O, P](ta: List[O], tb: List[P]): List[P], 
  [O, P](ta: List[O], tb: List[P]): List[P]
, [(param)3]: Any, [(param)4]: Any
 bounds: 
     O >: List[Test.implA.Node]
     P >: List[(param)4]
     O >: List[Test.implA.Node]
     P >: List[(param)3]
     (param)3
     (param)4
 ordering: 
     P <: P

We should instantiate the type variable to Nothing instead, since that keeps the constraint as general as possible. But to see that we have to look at all other bindings of the constraint. This can get very expensive.

It does seem to have a lot to do with level checking and I see some code that uses a variable's name to decide interpolation direction in interpolateTypeVars:

              val fromBelow =
                name.is(AvoidNameKind.UpperBound) ||
                !name.is(AvoidNameKind.LowerBound) && tvar.hasLowerBound

But the problem persists even if I turn Config.checkLevelsOnConstraints on. @smarter Do you have a suggestion how to proceed here?

[odersky]

Maybe should bite the bullet and introduce reverse indices in constraints. By this I mean two maps

val coDeps, contraDeps: Map[TypeVar, Set[TypeVar]]

• coDeps(x) contains all type variables of level smaller than x.nestingLevel where x occurs covariantly or invariantly in their bound.
• contraDeps(x) contains all type variables of level smaller than x.nestingLevel where x occurs contravariantly or invariantly in their bound.

The sets would have to be maintained in constraints. We can use these sets to make decisions about instantiation directions.