From 82ec3efb91da8514860aab46a5f172c0dd22f4c4 Mon Sep 17 00:00:00 2001
From: Dale Wijnand <dale.wijnand@gmail.com>
Date: Mon, 11 Mar 2024 11:22:32 +0000
Subject: [PATCH] Allow poly-kinded GADT vars to infer constraints

Allowing the types to flow through in thirdTryNamed requires a tweak to
baseType.  Given "class C[T <: Int]" (from tests/pos-macros/i10864a) the
basetype of a TypeRef of just "C", with the Any class symbol, shouldn't
return Any because "C" is not a proper/value type.  That is, in
baseType, we need to short-circuit TypeProxy.superType (i.e.
underlying), which is returns resultType for a HKLambda.
---
 .../tools/dotc/core/SymDenotations.scala      |  3 +++
 .../dotty/tools/dotc/core/TypeComparer.scala  |  9 +++-----
 tests/pos/i19904.orig.scala                   | 21 +++++++++++++++++++
 tests/pos/i19904.scala                        | 15 +++++++++++++
 4 files changed, 42 insertions(+), 6 deletions(-)
 create mode 100644 tests/pos/i19904.orig.scala
 create mode 100644 tests/pos/i19904.scala

diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
index b3fe5757720e..10c7fccb6466 100644
--- a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
+++ b/compiler/src/dotty/tools/dotc/core/SymDenotations.scala
@@ -2287,6 +2287,9 @@ object SymDenotations {
           case CapturingType(parent, refs) =>
             tp.derivedCapturingType(recur(parent), refs)
 
+          case tp: HKLambda =>
+            NoType
+
           case tp: TypeProxy =>
             def computeTypeProxy = {
               val superTp = tp.superType
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 302ad7987889..44bfcdfd21b1 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -580,12 +580,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
           if (cls2.typeParams.isEmpty) {
             if (cls2 eq AnyKindClass) return true
             if (isBottom(tp1)) return true
-            if (tp1.isLambdaSub) return false
-              // Note: We would like to replace this by `if (tp1.hasHigherKind)`
-              // but right now we cannot since some parts of the standard library rely on the
-              // idiom that e.g. `List <: Any`. We have to bootstrap without scalac first.
-            if cls2 eq AnyClass then return true
-            if cls2 == defn.SingletonClass && tp1.isStable then return true
+            if tp1.hasSimpleKind then
+              if cls2 eq AnyClass then return true
+              if cls2 == defn.SingletonClass && tp1.isStable then return true
             return tryBaseType(cls2)
           }
           else if (cls2.is(JavaDefined)) {
diff --git a/tests/pos/i19904.orig.scala b/tests/pos/i19904.orig.scala
new file mode 100644
index 000000000000..07c599a6c6b1
--- /dev/null
+++ b/tests/pos/i19904.orig.scala
@@ -0,0 +1,21 @@
+sealed trait Wrap[A <: AnyKind]
+
+trait Foo[T <: AnyKind, X[_ <: T]]
+
+trait Bar[T <: AnyKind, X[_ <: T]] {
+
+  def foo: Foo[
+    Wrap[? <: T],
+    [x <: Wrap[? <: T]] =>> x match { case Wrap[a] => X[a] }
+  ]
+
+}
+
+object Qux extends Bar[Any, [_] =>> Unit] {
+
+  override def foo: Foo[
+    Wrap[? <: Any],
+    [x <: Wrap[? <: Any]] =>> x match { case Wrap[a] => Unit }
+  ] = ???
+
+}
diff --git a/tests/pos/i19904.scala b/tests/pos/i19904.scala
new file mode 100644
index 000000000000..2738697b88de
--- /dev/null
+++ b/tests/pos/i19904.scala
@@ -0,0 +1,15 @@
+sealed trait Bx[AK1 <: AnyKind]
+trait C1[AK2 <: AnyKind, X[_ <: AK2]]
+trait C2[AK3 <: AnyKind, Y[_ <: AK3]]:
+           def mm: C1[Bx[? <: AK3], [x <: Bx[? <: AK3]] =>> x match { case Bx[a] => Y[a] }]
+class C3 extends C2[Any, [_] =>> Unit]:
+  override def mm: C1[Bx[? <: Any], [y <: Bx[? <: Any]] =>> y match { case Bx[b] => Unit }] = ???
+
+/*
+C1[Bx[?], [y <: Bx[?]] =>> y match { case Bx[b] => Unit } <: Unit]  <:  C1[Bx[?], [x <: Bx[?]] =>> x match { case Bx[a] => Unit } <: Unit]
+          [x <: Bx[?]] =>> x match { case Bx[a] => Unit } <: Unit   <:            [y <: Bx[?]] =>> y match { case Bx[b] => Unit } <: Unit
+                           x match { case Bx[a] => Unit } <: Unit   <:                             x match { case Bx[b] => Unit } <: Unit
+                             [a] =>> case Bx[a] => Unit             <:                    [b <: AnyKind] =>> case Bx[b] => Unit
+                             [ <: AnyKind]                          <:                    []
+                                  AnyKind                           <:                          Any  = false
+*/