Regression in GADT type inference inside polymorphic function

[TomasMikula]

Compiler version

3.4.0-RC3
(regressed since 3.3.1)

Minimized code

enum Op[A, B]:
  case Dup[T]() extends Op[T, (T, T)]
    
def foo[R](f: [A, B] => (o: Op[A, B]) => R): R =
    f(Op.Dup())

foo([A, B] => (o: Op[A, B]) => {
  o match
    case o: Op.Dup[t] =>
      summon[A =:= t]      // ERROR: Cannot prove that A =:= t.
      summon[B =:= (t, t)] // ERROR: Cannot prove that B =:= (t, t).
      42
})

https://scastie.scala-lang.org/PvLamiXMQXaEIWEf18kGXQ

Output

Cannot prove that A =:= t.
Cannot prove that B =:= (t, t).

Expectation

The code should compile. It does compile with Scala 3.3.1

[EugeneFlesselle]

A perhaps minimised but more confusing version:

enum Op[A]:
  case Dup[T]() extends Op[(T, T)]

def foo[R](f: [A] => Op[A] => R): R = ??? 

def test =
  foo[Unit]([A] => (o: Op[A]) =>
    o match
      case o: Op.Dup[u] =>
        summon[A =:= (u, u)] // Ok
        ()
  )
  foo/*[Unit]*/([A] => (o: Op[A]) =>
    o match
      case o: Op.Dup[u] =>
        summon[A =:= (u, u)] // Error: Cannot prove that A =:= (u, u)
        ()
  )
  foo/*[Unit]*/(
    {
      val f1 = [B] => (o: Op[B]) =>
        o match
          case o: Op.Dup[u] =>
            summon[B =:= (u, u)] // Also ok
            ()
      f1
    }
  )