Spurious pattern exhaustivity warning when one type parameter lower-bounds another

[OlivierBlanvillain]

This example:

sealed trait Parent
final case class Leaf[A, B >: A](a: A, b: B) extends Parent

def run(x: Parent): Unit = x match {
  case Leaf(a, b) =>
}

Leads to the following spurious warning:

-- [E029] Pattern Match Exhaustivity Warning:
6 |def run(x: Parent): Unit = x match {
  |                           ^
  |                           match may not be exhaustive.
  |
  |                           It would fail on pattern case: Leaf(_, _)
  |
  | longer explanation available when compiling with `-explain`
1 warning found

I suspect the issue to be different from #15522, since it is present on both main and 3.1.2.

[dwijnand]

My money is on instantiateToSubType, which might ring a bell. 😄 But I haven't even tried this yet.

[SethTisue]

Some rough notes from Dale's and my digging so far:

• It's helpful to add a second version of Leaf that omits the lower bound on B, to help understand how the behavior changes when the lower bound is added.
• The type parameters on the unapply are getting maximized to [Nothing, Nothing] which is wrong.
• In maximizeType, changing the bounds.hi <:< bounds.lo check to use frozen_<:< prevents the bad maximization from happening and seems like a plausible change.
• We're working with a form of the test case where the rhs is a instead of () because that brings type avoidance into play, and type avoidance goes into an infinite loop because we have both versions of the bound, the original B >: A and the reversed A <: B.
• But Dale thinks that the data structures we have before type avoidance even starts are wrong, it's not that the type avoidance needs to be changed to deal with them.
• ConstraintHandling.scala says "We don't allow recursive lower bounds when defining a type, so we shouldn't allow them as constraints either" — note the asymmetry. To support F-bounds we only allow recursion in upper bounds.

(As I say, rough notes, but they'll help jog our memory when we come back to this.)

We're going to do at least one more round of digging tomorrow, then decide whether to stay on it or bail.

[smarter]

note the asymmetry. To support F-bounds we only allow recursion in upper bounds.

Related: I realized recently that despite our best effort we could still get recursion in lower bounds: https://github.com/lampepfl/dotty/issues/15280 and I have no idea how to deal with that properly

[SethTisue]

Perhaps surprisingly, it matters whether we write [A, B >: A] or [B >: A, A]. The latter still fails, but without the bound getting flipped to A <: B, so it seems like a bit simpler case to investigate.

We have one provisional fix that involves two changes: the bounds.hi frozen_<:< bounds.lo change already mentioned above, plus a change where when instantiating an invariant type variable (e.g. replacing A with A$1), we add code to update the GADT constraints to reflect the replacement, which wasn't happening before.

Together that's enough to fix this ticket, but then a bunch of other test cases fail and it isn't clear which failure to dig into to get insight into what might be wrong with the changes. t14739 (#14739) is one possibility; it's pretty simple, but it's also something that only recently got fixed so maybe it's that not that fundamental (and thus perhaps less diagnostic). It might be better to dig into an older test case that started failing, e.g. overconstrained-type-variables-gadt.scala. 🤷

The frozen_<:< change itself isn't enough to break overconstrained-type-variables-gadt.scala; the GADT constraint replacement is the culprit there. It isn't clear yet whether that change is a bad idea, or a good idea we just haven't implemented properly yet.

[SethTisue]

It isn't clear yet whether that change is a bad idea, or a good idea we just haven't implemented properly yet.

Dale has a new, perhaps more promising implementation of this idea... stay tuned

[SethTisue]

Upon further digging, Dale realized that when instantiating an invariant type variable, we aren't free to remove the original and keep only the instantiation, because that same original type variable might need to be constrained a second time if we go into a nested pattern match. That actually happens in i4471-gadt.scala.

That solution path might not be dead; perhaps we can only replace the original type parameter with its instantiation wherever it appears in constraints without removeing it.

But now we're also considering an alternate solution path that would involve fixing fullBounds (which we are calling from both maximizeType and indexPattern) to not output (in this case, at least) bounds which contain a cycle. (Namely, the cycle that's causing trouble downstream during type avoidance.) Or, not a cycle that runs through a lower bound, anyway, since cycles are allowed in upper bounds, because F-bounds.

Note that fullBounds isn't called over the place; it's basically just us (as in, there are only a handful of call sites and they're within the exact code that we're studying and considering changing).

[SethTisue]

With the change to fullBounds, t6084.scala started failing (in Ycheck) and we dug into it and achieved some understanding of why (to make a long story short: instead of d being typed as T => U we end up with a GADT cast from f => g to T => U, but then after typer finishes, f and g no longer exist so the check that the target type of the cast conforms to the expected type goes haywire). But we were left without a clear intuition of what direction to go next. 😕

[SethTisue]

Also in cycles-in-bounds territory: #14287

[SethTisue]

Note that the original test case is fixable just with the frozen_<:< change.

So perhaps there's yet another possible solution path here, namely:

Prevent the type avoidance crash (which only arises when we change the rhs of the pattern from () to a) by making type avoidance (or whatever relevant piece of machinery that type avoidance is employing) not choke on the cycle.