A GADT type parameter throws off even a non-GADT one

[TomasMikula]

Compiler version

3.2.2

Minimized code

class Test[F[_]] {
  sealed trait Foo[A, B]

  // note that Foo's B param maps directly to U (i.e. no GADT involved on this type param)
  case class Bar[T, U]() extends Foo[F[T], U] {
    def get: Option[U] = None
  }
  
  def go[T, U](that: Foo[F[T], U]): Option[U] =
    that match
      case b: Bar[t, u] =>
        summon[U =:= u] // Error: Cannot prove that U =:= u.
        b.get           // Error: Found: Option[u], Required: Option[U]
}

Output

Compilation fails, see the errors in the comments.

Expectation

The code should compile.

[odersky]

This looks like a bug to me. @abgruszecki @Linyxus can you confirm?

[Linyxus]

This seems like a completeness issue to me too. The constraint U =:= u is not derived, because we do not assume the injectivity of this HK type F (which means that given F[a] =:= F[b] we can not show a =:= b). Specifically, when we infer GADT bounds from Foo[F[T], U] >:< Foo[F[t], u]:

1. We first try to derive bounds from F[T] =:= F[t].
2. Since F is non-injective, we won't derive the constraint T =:= t (which we shouldn't), and returns false in TypeComparer.
3. When the result of F[T] =:= F[t] is false, we would just rollback the GADT constraints, and won't even examine U >:< u (as seen here).

Rolling back GADT constraints when the type comparer returns false feels a bit too restrictive to me. Since as long as we are careful enough when adding constraints (only adding the really necessary ones), whether type comparer thinks a subtyping relation is absurd should not matter. Does the logic here have other considerations (like for some sort of interactions with type inference)? Shall we drop it for better completeness?

[abgruszecki]

As I remember it, this is actually a tricky issue. The problem is that with the way we implemented subtyping reconstruction, we do not properly distinguish between a subtype check that cannot possibly succeed and one that may succeed for some instantiation of abstract types.

In an Ideal World, while doing subtyping reconstruction, isSubtype would only return false if the desired subtyping relationship is contradictory, say Int <:< String. Note that this should mean that F[T] <:< F[t] should return true, because the relationship is clearly possible (for instance for type F[X] = Unit). In this Ideal World, we should roll back the constraints every time isSubtype returns false, and there would be cases where we could exploit that to reconstruct better bounds, but (!) only as long as we can trust that false means that the relationship is genuinely contradictory.

As we are right now, we roll back the constraint, but also return false too eagerly during subtyping recostruction. I think it's justifiable to never roll back the constraints, but IIRC it should be possible to construct examples where that gives us worse results, at least I recall that once Yichen implemented the rollback, we reconstructed better bounds in some cases.

[abgruszecki]

And to make it clear: we've been trying to fix the problems with reusing isSubtype for subtyping reconstruction and we keep finding new and new problems with it. I think it would take a dedicated project to clean things up on that front, and it might require separating subtyping reconstruction from isSubtype.