Match type bounded by type with argument(s) cannot be reduced to satisfy `=:=` check

[tribbloid]

Pointed out by @DmytroMitin in the following post:

https://stackoverflow.com/questions/75837775/in-scala-2-or-3-is-there-a-higher-kind-argument-extractor-without-using-match-t/75842531#75842531

  type Ext[S <: Seq[_]] = S match {
    case Seq[t] => t
  }

implicitly[Ext[Seq[Int]] =:= Int] // e.scala: Cannot prove that e.Ext[Seq[Int]] =:= Int

If I change the definition of Ext as follow, the consequence will differ:

  type Ext[S] = S match {
    case Seq[t] => t
  } // success!

  type Ext[S <: Any] = S match {
    case Seq[t] => t
  } // success!

  type Ext[S <: Seq[Any]] = S match {
    case Seq[t] => t
  } // same error

[Decel]

For some reason, we don't get a reduction:

adapt to subtype A =:= A !<:< Ext[Seq[Int]] =:= Int
>>>> StoredError: Found:    A =:= A
Required: Ext[Seq[Int]] =:= Int

where:    A is a type variable
adapt to subtype A =:= A !<:< Ext[Seq[Int]] =:= Int
>>>> StoredError: Found:    A =:= A
Required: Ext[Seq[Int]] =:= Int

if we use [S <: Seq[Int]] everything works, because during isSubType, we have an upper bound of Int, instead of Any, so for example:

==> isSubType Ext[Seq[Int]] <:< Nothing?
  ==> isSubType Int <:< Nothing?
  <== isSubType Int <:< Nothing = false

==> isSubType Ext[Seq[Int]] <:< Nothing?
 ==> isSubType Any <:< Nothing?
 <== isSubType Any <:< Nothing = false

So, this works:

type Ext[S <: Seq[Any]] = S match
  case Seq[t] => t

val a = summon[Ext[Seq[Int]] =:= Any]

[Decel]

And, unsurprisingly, works in 3.1.3 -- Looks like a duplicate of #15926.

[sjrd]

Also works in tasty-query 😁

[Decel]

The whole problematic tree looks like this:

==> S match case Seq[t] => t?
  ==> isSubType S <:< Seq[t]?
  <== isSubType S <:< Seq[t] = false
  ==> isSubType S <:< Seq[t]?
    ==> isSubType Seq[Any] <:< Seq[t] (left is approximated)?
      ==> isSubType Any <:< t?
        ==> isSubType Any <:< Nothing?
        <== isSubType Any <:< Nothing = false
        ==> isSubType Any <:< Any?
          ==> isSubType scala.type <:< (scala : scala.type)?
          <== isSubType scala.type <:< (scala : scala.type) = true
        <== isSubType Any <:< Any = true
      <== isSubType Any <:< t = true
    <== isSubType Seq[Any] <:< Seq[t] (left is approximated) = true
  <== isSubType S <:< Seq[t] = true
  ==> isSubType Any <:< Any?
    ==> isSubType (scala : scala.type) <:< scala.type?
    <== isSubType (scala : scala.type) <:< scala.type = true
  <== isSubType Any <:< Any = true
<== S match case Seq[t] => t = Reduced(Any)

So, in the end, we get:

type Ext = ([S <: Seq[Any]] =>> Any)

😢

[dwijnand]

Yeah, I looked at that trace again, from that duplicate. My original fix was to disallow, using your trace, S widening to Seq[Any]. But last week I was wondering whether the issue was the loss of approximation state that was to blame.

[Decel]

Yeah, I looked at that trace again, from that duplicate. My original fix was to disallow, using your trace, S widening to Seq[Any]. But last week I was wondering whether the issue was the loss of approximation state that was to blame.

Disallowing it seems too restrictive, -- and if we try to widen it to Any, then we may violate type bounds. I can't see a nice workaround here, it's a fascinatingly bad situation.

I am not sure about the approximation state -- what is it supposed to look like? Seems to me, the approximation is correct because anything other than Seq[Any] will be a bounds violation, but not sure if I understand you completely.

[dwijnand]

but not sure if I understand you completely.

ApproxState maintains whether the LHS has been widened and/or the RHS has been narrowed, and that affects, for instance, whether to consider it as a constraint bound. Here I'm thinking of the check if canConstrain(tp2) && !approx.low.

In the trace it (sometimes) appears as "(left is approximated)" (or right), and it disappears when checking args. I was wondering if that was the problem.

[Decel]

I looked into 3.1.3 trace:

==> isSubType S <:< Seq[t]?
<== isSubType S <:< Seq[t] = false
==> isSubType Any <:< Any?
  ==> isSubType scala.type <:< (scala : scala.type)?
  <== isSubType scala.type <:< (scala : scala.type) = true
<== isSubType Any <:< Any = true
==> isSubType Nothing <:< Any?
<== isSubType Nothing <:< Any = true

So it's widening to Any instead of Seq[Any] and in 3.1.3 the following code works:

type Ext[S <: Seq[Int]] = S match
  case Seq[t] => t

val a = summon[Ext[Seq[String]] =:= String]

UPD:

Ah, that's #17168. If we use implicitly instead we run into error.

  |val a = implicitly[Ext[Seq[String]] =:= String]
  |                                               ^
  |                            Cannot prove that Ext[Seq[String]] =:= String.

[dwijnand]

Yeah, not widening the abstract type S to its bounds Seq[Int] is what I meant by "my" original fix. But it was really to see whether reverting that part (back to how Olivier had it) fixed that issue, which it did. Seth did a good job attempting to narrate and crosslink this saga in #15926 (comment).

[dwijnand]

Disallowing it seems too restrictive

Going back to this comment, I think disallowing is correct: we don't want the match type to reduce to the upper bound, because then we lose the tie to the actually passed type. We want the String in Seq[String], not Any, even though Any is String's upper bound. The match type, as it's defined using an abstract type in the match alias's type lambda, should stay an unreduced match type (because reduction gets stuck).

[odersky]

I had a look at this with @Decel. The critical PR which led to this situation is #15423, which itself follows up on several previous PRs that go back and forth on the issue. Essentially, there are two interlinked questions

1. Are we allowed to widen an abstract type or type parameter to its bound when reducing a matchtype?
2. Is match type reduction allowed to instantiate variables in patterns?

Originally, the answer was yes to both, but one can easily show that that's unsound. Then #13780 disallowed (1), but that caused a lot of regressions of reasonable code that worked before. Then #15423 answered the question by trying two different strategies as shown in this snippet in TypeComparer#matchCases

      if caseLambda.exists && matches(canWidenAbstract = false) then
        redux(canApprox = true)
      else if matches(canWidenAbstract = true) then
        redux(canApprox = false)

So, we first say no to (1), and if that fails we try again saying yes to (1), but restricting how type variables get instantiated.
The necessary restriction is as follows:

If we widen a type S <: T to T then any type variables we instantiate would get exactly the same instantiations if we used some subtype of T for S.

But that's super hard to check, so we need an approximation. The approximation we used was that, if at the end of the comparison, a type variable was constrained to a single point, then we can instantiate the type variable to that point. Might look reasonable, but is unsound. The problem was in the example here. We have:

  S <: Seq[_]   in the scrutinee
  S <: Seq[t]    in the pattern match

We widen S to Seq[_] which gives us Seq[_] <: Seq[t], which gives us t = Any. The same result would be obtained if we hard started with the bound S <: Seq[Any]. But we could have instantiated S to the subtype Seq[Int] instead which would give t = Int. So we are not allowed to instantiate t to Any, after all, even though it is uniquely determined from Seq[_] <: Seq[t].

Not yet sure what to do about this.