Fix match type instantiation when not approximating

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -3095,17 +3095,18 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
     def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
       def apply(insts: Array[Type], t: Type) = t match
         case param @ TypeParamRef(b, n) if b eq caseLambda =>
+          def range1(tp: Type) = if variance == 0 || param.paramName.is(NameKinds.WildcardParamName) then tp else Range(tp, tp)
           insts(n) =
             if canApprox then
               approximation(param, fromBelow = variance >= 0, Int.MaxValue).simplified
             else constraint.entry(param) match
               case entry: TypeBounds =>
                 val lo = fullLowerBound(param)
                 val hi = fullUpperBound(param)
-                if isSubType(hi, lo) then lo.simplified else Range(lo, hi)
+                if isSubType(hi, lo) then range1(lo.simplified) else Range(lo, hi)
               case inst =>
                 assert(inst.exists, i"param = $param\nconstraint = $constraint")
-                inst.simplified
+                range1(inst.simplified)
           insts
         case _ =>
           foldOver(insts, t)

compiler/src/dotty/tools/dotc/core/tasty/TreeUnpickler.scala

@@ -1418,7 +1418,11 @@ class TreeUnpickler(reader: TastyReader,
               val args = until(end)(readTpt())
               val tree = untpd.AppliedTypeTree(tycon, args)
               val ownType = ctx.typeAssigner.processAppliedType(tree, tycon.tpe.safeAppliedTo(args.tpes))
-              tree.withType(postProcessFunction(ownType))
+              tree.withType(postProcessFunction(ownType) match {
+                case tp @ MatchType.InDisguise(_) => tp
+                case tp: AndType                  => tp // pickleSkolem
+                case tp                           => tp.simplified // i17149
+              })
             case ANNOTATEDtpt =>
               Annotated(readTpt(), readTerm())
             case LAMBDAtpt =>

compiler/src/dotty/tools/dotc/transform/TypeUtils.scala

@@ -76,7 +76,11 @@ object TypeUtils {
       case AndType(tp1, tp2) =>
         // We assume that we have the following property:
         // (T1, T2, ..., Tn) & (U1, U2, ..., Un) = (T1 & U1, T2 & U2, ..., Tn & Un)
-        tp1.tupleElementTypes.zip(tp2.tupleElementTypes).map { case (t1, t2) => t1.intersect(t2) }
+        val types1 = tp1.tupleElementTypes
+        val types2 = tp2.tupleElementTypes
+        if !types1.isDefined then types2 // e.g. i15302b which has Int *: Int *: Tuple (not EmptyTuple)
+        else if !types2.isDefined then types1
+        else types1.zip(types2).map { case (t1, t2) => t1.intersect(t2) }
       case OrType(tp1, tp2) =>
         None // We can't combine the type of two tuples
       case _ =>

scaladoc-testcases/src/tests/typesSignatures.scala

@@ -51,7 +51,7 @@ class Operators
   // type Binary2 = String op Int
 
   import scala.compiletime.ops.boolean.*
-  type Unary = ![true]
+  type Unary = ![true] //expected: type Unary = false
 }
 
 trait ThisTypeTest

tests/neg/11982.scala

@@ -4,8 +4,8 @@ type Head[X] = X match {
 }
 
 object Unpair {
-  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1
-  unpair[Tuple2["msg", 42]]: "msg"  // error
+  def unpair[X <: Tuple2[Any, Any]]: Head[X] = 1 // error
+  unpair[Tuple2["msg", 42]]: "msg"
 }
 
 
@@ -14,8 +14,8 @@ type Head2[X] = X match {
 }
 
 object Unpair2 {
-  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1
-  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg" // error
+  def unpair[X <: Tuple2[Tuple2[Any, Any], Tuple2[Any, Any]]]: Head2[X] = 1 // error
+  unpair[Tuple2[Tuple2["msg", 42], Tuple2[41, 40]]]: "msg"
 }
 
 
@@ -35,6 +35,6 @@ type Head4[X] = X match {
 }
 
 object Unpair4 {
-  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1
-  unpair[Foo["msg", 42]]: "msg" // error
+  def unpair[X <: Foo[Any, Any]]: Head4[Foo[X, X]] = 1 // error
+  unpair[Foo["msg", 42]]: "msg"
 }

tests/neg/i13780.check

@@ -1,3 +1,23 @@
+-- [E007] Type Mismatch Error: tests/neg/i13780.scala:12:32 ------------------------------------------------------------
+12 |  def unpair[X <: Y]: Head[X] = "" // error
+   |                                ^^
+   |                                Found:    ("" : String)
+   |                                Required: Head[X]
+   |
+   |                                where:    X is a type in method unpair with bounds <: A.this.Y
+   |
+   |
+   |                                Note: a match type could not be fully reduced:
+   |
+   |                                  trying to reduce  Head[X]
+   |                                  failed since selector X
+   |                                  does not uniquely determine parameters a, b in
+   |                                    case (a, b) => a
+   |                                  The computed bounds for the parameters are:
+   |                                    a >: Any
+   |                                    b >: Any
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg/i13780.scala:18:31 ------------------------------------------------------------
 18 |  def int[X <: Y]: Int = unpair[X]  // error
    |                         ^^^^^^^^^

tests/neg/i13780.scala

@@ -9,7 +9,7 @@ trait Z {
 
 class A extends Z {
   type Y <: Tuple2[Any, Any]
-  def unpair[X <: Y]: Head[X] = ""
+  def unpair[X <: Y]: Head[X] = "" // error
   def any[X <: Y]: Any = unpair[X]
 }
 

tests/neg/i17149.scala

@@ -0,0 +1,18 @@
+type Ext1[S] = S match {
+  case Seq[t] => t
+}
+type Ext2[S] = S match {
+  case Seq[_] => Int
+}
+type Ext3[S] = S match {
+  case Array[t] => t
+}
+type Ext4[S] = S match {
+  case Array[_] => Int
+}
+def foo[T <: Seq[Any], A <: Array[B], B] =
+  summon[Ext1[T] =:= T]    // error
+  summon[Ext2[T] =:= Int]  // ok
+  summon[Ext3[A] =:= B]    // ok
+  summon[Ext4[A] =:= Int]  // ok
+

tests/pos/i14964a.scala

@@ -0,0 +1,2 @@
+def toList: List[Int] =
+  (1, 1).toList

tests/pos/i15155.scala

@@ -8,4 +8,4 @@ type EnumValue[A <: Enumeration] = A match {
 // https://github.com/json4s/json4s/blob/355d8751391773e0d79d04402a4f9fb7bfc684ec/ext/src/main/scala/org/json4s/ext/EnumSerializer.scala#L25-L26
 class EnumSerializer[E <: Enumeration: ClassTag](enumeration: E) {
   val EnumerationClass = classOf[EnumValue[E]]
-}
+}

tests/pos/i15926.extract.scala

@@ -0,0 +1,21 @@
+sealed trait Nat
+final case class Zero() extends Nat
+final case class Succ[+N <: Nat]() extends Nat
+
+final case class Neg[+N <: Succ[Nat]]()
+
+type Sum[X, Y] = Y match
+  case Zero    => X
+  case Succ[y] => Sum[Succ[X], y]
+
+type IntSum[A, B] = B match
+  case Neg[b] => IntSumNeg[A, b]
+
+type IntSumNeg[A, B] = A match
+  case Neg[a] => Neg[Sum[a, B]]
+
+type One = Succ[Zero]
+type Two = Succ[One]
+
+class Test:
+  def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]]

tests/pos/i15926.min.scala

@@ -0,0 +1,19 @@
+sealed trait Nat
+final case class Zero() extends Nat
+final case class Succ[+N <: Nat]() extends Nat
+
+final case class Neg[+N <: Succ[Nat]]()
+
+type Sum[X, Y] = Y match
+  case Zero    => X
+  case Succ[y] => Sum[Succ[X], y]
+
+type IntSum[A, B] = B match
+  case Neg[b] => A match
+    case Neg[a] => Neg[Sum[a, b]]
+
+type One = Succ[Zero]
+type Two = Succ[One]
+
+class Test:
+  def test() = summon[IntSum[Neg[One], Neg[One]] =:= Neg[Two]]

tests/pos/i15926.scala

@@ -0,0 +1,27 @@
+@main def main(): Unit =
+  println(summon[Sum[Minus[Succ[Zero]], Minus[Succ[Zero]]] =:= Minus[Succ[Succ[Zero]]]])
+
+sealed trait IntT
+sealed trait NatT extends IntT
+final case class Zero() extends NatT
+final case class Succ[+N <: NatT](n: N) extends NatT
+final case class Minus[+N <: Succ[NatT]](n: N) extends IntT
+
+type NatSum[X <: NatT, Y <: NatT] <: NatT = Y match
+  case Zero => X
+  case Succ[y] => NatSum[Succ[X], y]
+
+type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match
+  case Zero => X
+  case Succ[y] => X match
+    case Zero => Minus[Y]
+    case Succ[x] => NatDif[x, y]
+
+type Sum[X <: IntT, Y <: IntT] <: IntT = Y match
+  case Zero => X
+  case Minus[y] => X match
+    case Minus[x] => Minus[NatSum[x, y]]
+    case _ => NatDif[X, y]
+  case _ => X match
+    case Minus[x] => NatDif[Y, x]
+    case _ => NatSum[X, Y]

tests/pos/i17149.scala

@@ -0,0 +1,5 @@
+type Ext[S <: Seq[_]] = S match {
+  case Seq[t] => t
+}
+
+def test = implicitly[Ext[Seq[Int]] =:= Int]