Comparing Refined Types can lead to invalid subtype reconstruction

[abgruszecki]

Originally posted by @Linyxus in https://github.com/lampepfl/dotty/issues/15175#issuecomment-1152619492

Regarding the soundness holes caused by resetting approx state: yes, we have more soundness holes caused by this. Each time isSubType(S, T) (instead of recur(S, T)) is called inside isSubType, the approx state is reset, and it will be a potential soundness hole. For example, I find another callsite of isSubType here, and we can make a counter-example showing the unsoundness brought by this:

enum SUB[-A, +B]:
  case Refl[C]() extends SUB[C, C]

trait Tag { type T }

def foo[A, B, X <: Tag{type T <: A}](e: SUB[X, Tag{type T <: B}], x: A): B = e match {
  case SUB.Refl() =>
    // unsound GADT constr because of approx state resetting: A <: B
    x
}

def bad(x: Int): String =
  foo[Int, String, Tag{type T = Nothing}](SUB.Refl(), x)  // cast Int to String

In this example, we are trying to extract necessary constraint from X <: Tag{type T <: B}, where X is known to be a subtype of Tag{type T <: A}. During this we will try upcasting LHS and compare Tag{type T <: A} <: Tag{type T <: B} with LHS approximated. Since when comparing the refinement info the approx state is reset, we derive the unsound constraint A <: B.

[Linyxus]

More explanation: after having a closer inspection of the issue, the call site mentioned in the original comment is incorrect and misleading. What actually happens:

• We are trying to reconstruct subtyping from X <: Tag{T <: B},
• When comparing this relation, TypeComparer will end up calling hasMatchingMember(T, X, Tag{T<:B}), which asks whether the type member T or LHS is a subtype of the RHS.
• Here in hasMatchingMember queries the member T of X, which implicitly upcasts X to its upper bound Tag{T <: A}, leading to the unsoundness.

[Linyxus]

To verify, I added the tracing expression trace.force(i"$tp1 . $name", show = true) { tp1.member(name) }. This is what it prints:

==> X . T?
<== X . T = type T

The query returns the type member T of the upper bound of X. This implicitly upcasts X.

[ValeriePe]

This issue was picked for the Issue Spree n° 19 of August 16th which takes place in a week from now. @dwijnand @nmcb will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.