Add GADT symbols when typing typing-ahead lambda bodies

Author: dwijnand

compiler/src/dotty/tools/dotc/typer/Namer.scala

@@ -1733,8 +1733,14 @@ class Namer { typer: Typer =>
         val tpe = (paramss: @unchecked) match
           case TypeSymbols(tparams) :: TermSymbols(vparams) :: Nil => tpFun(tparams, vparams)
           case TermSymbols(vparams) :: Nil => tpFun(Nil, vparams)
+        val rhsCtx = (paramss: @unchecked) match
+          case TypeSymbols(tparams) :: TermSymbols(_) :: Nil =>
+            val rhsCtx = ctx.fresh.setFreshGADTBounds
+            rhsCtx.gadtState.addToConstraint(tparams)
+            rhsCtx
+          case TermSymbols(_) :: Nil => ctx
         if (isFullyDefined(tpe, ForceDegree.none)) tpe
-        else typedAheadExpr(mdef.rhs, tpe).tpe
+        else typedAheadExpr(mdef.rhs, tpe)(using rhsCtx).tpe
 
       case TypedSplice(tpt: TypeTree) if !isFullyDefined(tpt.tpe, ForceDegree.none) =>
         mdef match {

tests/pos/i19570.min1.scala

@@ -0,0 +1,23 @@
+enum Op[A]:
+  case Dup[T]() extends Op[(T, T)]
+
+def foo[R](f: [A] => Op[A] => R): R = ???
+
+def test =
+  foo([A] => (o: Op[A]) => o match
+    case o: Op.Dup[u] =>
+      summon[A =:= (u, u)] // Error: Cannot prove that A =:= (u, u)
+      ()
+  )
+  foo[Unit]([A] => (o: Op[A]) => o match
+    case o: Op.Dup[u] =>
+      summon[A =:= (u, u)] // Ok
+      ()
+  )
+  foo({
+    val f1 = [B] => (o: Op[B]) => o match
+      case o: Op.Dup[u] =>
+        summon[B =:= (u, u)] // Also ok
+        ()
+    f1
+  })

tests/pos/i19570.min2.scala

@@ -0,0 +1,24 @@
+sealed trait Op[A, B]                               { def giveA: A;     def giveB: B }
+final case class Dup[T](x: T) extends Op[T, (T, T)] { def giveA: T = x; def giveB: (T, T) = (x, x) }
+
+class Test:
+  def foo[R](f: [A, B] => (o: Op[A, B]) => R): R = ???
+
+  def m1: Unit =
+    foo([A, B] => (o: Op[A, B]) => o match
+      case o: Dup[t] =>
+        var a1: t = o.giveA
+        var a2: A = o.giveA
+        a1 = a2
+        a2 = a1
+
+        var b1: (t, t) = o.giveB
+        var b2: B      = o.giveB
+        b1 = b2
+        b2 = b1
+
+        summon[A =:= t]      // ERROR: Cannot prove that A =:= t.
+        summon[B =:= (t, t)] // ERROR: Cannot prove that B =:= (t, t).
+
+        ()
+    )

tests/pos/i19570.orig.scala

@@ -0,0 +1,14 @@
+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())
+
+def test =
+  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
+  })