Skip to content

Commit a5f7e1c

Browse files
authoredJan 29, 2025··
Handle NoType in TypeComparer.disjointnessBoundary (#21520)
Closes #20265
2 parents 9cb97ec + 3d8a70f commit a5f7e1c

File tree

5 files changed

+67
-0
lines changed

5 files changed

+67
-0
lines changed
 

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

+2
Original file line numberDiff line numberDiff line change
@@ -3070,6 +3070,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
30703070
disjointnessBoundary(tp.effectiveBounds.hi)
30713071
case tp: ErrorType =>
30723072
defn.AnyType
3073+
case tp: NoType.type =>
3074+
defn.AnyType
30733075
end disjointnessBoundary
30743076

30753077
(disjointnessBoundary(tp1), disjointnessBoundary(tp2)) match

‎tests/neg/i20265-1.check

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
-- Error: tests/neg/i20265-1.scala:4:6 ---------------------------------------------------------------------------------
2+
4 | def apply(args: Tuple.Map[m.MirroredElemTypes, Expr]): Expr[T] = ??? // error
3+
| ^
4+
| non-private method apply in trait Ops refers to private given instance m
5+
| in its type signature (args: Tuple.Map[Ops.this.m.MirroredElemTypes, Expr]): Expr[T]

‎tests/neg/i20265-1.scala

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
trait Expr[T]
2+
3+
trait Ops[T](using m: scala.deriving.Mirror.ProductOf[T]) {
4+
def apply(args: Tuple.Map[m.MirroredElemTypes, Expr]): Expr[T] = ??? // error
5+
}
6+
7+
case class P(a: Int)
8+
object P extends Ops[P]
9+

‎tests/neg/i20265.check

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
-- [E172] Type Error: tests/neg/i20265.scala:22:95 ---------------------------------------------------------------------
2+
22 | println(summon[((String --> Unit) * (String --> Unit)) =:= Hinze[(String + String) --> Unit]]) // error
3+
| ^
4+
| Cannot prove that (String --> Unit) * (String --> Unit) =:= Hinze[String + String --> Unit].
5+
|
6+
| Note: a match type could not be fully reduced:
7+
|
8+
| trying to reduce Hinze[String + String --> Unit]
9+
| failed since selector (String + String --> Unit)#unfix
10+
| does not match case k1 + k2 --> v => Hinze[k1 --> v] * Hinze[k2 --> v]
11+
| and cannot be shown to be disjoint from it either.
12+
| Therefore, reduction cannot advance to the remaining case
13+
|
14+
| case k1 * k2 --> v => k1 --> Hinze[k2 --> v]
15+
-- [E172] Type Error: tests/neg/i20265.scala:23:66 ---------------------------------------------------------------------
16+
23 | println(summon[String =:= Hinze[Fix[Lambda[String]#L] --> Unit]]) // error
17+
| ^
18+
| Cannot prove that String =:= Hinze[Fix[[X] =>> String + String * X + X * X] --> Unit].
19+
|
20+
| Note: a match type could not be fully reduced:
21+
|
22+
| trying to reduce Hinze[Fix[[X] =>> String + String * X + X * X] --> Unit]
23+
| failed since selector (Fix[[X] =>> String + String * X + X * X] --> Unit)#unfix
24+
| does not match case k1 + k2 --> v => Hinze[k1 --> v] * Hinze[k2 --> v]
25+
| and cannot be shown to be disjoint from it either.
26+
| Therefore, reduction cannot advance to the remaining case
27+
|
28+
| case k1 * k2 --> v => k1 --> Hinze[k2 --> v]

‎tests/neg/i20265.scala

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
//> using options -source:3.3
2+
3+
trait Poly
4+
trait -->[X, Y] extends Poly
5+
trait +[X, Y] extends Poly
6+
trait *[X, Y] extends Poly
7+
8+
type Hinze[X <: Fix[?]] = X#unfix match
9+
case (k1 + k2) --> v => Hinze[(k1 --> v)] * Hinze[(k2 --> v)]
10+
case (k1 * k2) --> v => k1 --> Hinze[(k2 --> v)]
11+
12+
trait Lambda[V]:
13+
type Abs[X] = V * X
14+
type App[X] = X * X
15+
type L[X] = V + Abs[X] + App[X]
16+
17+
trait Fix[F[X]]:
18+
type unfix = F[Fix[F]]
19+
20+
@main
21+
def m =
22+
println(summon[((String --> Unit) * (String --> Unit)) =:= Hinze[(String + String) --> Unit]]) // error
23+
println(summon[String =:= Hinze[Fix[Lambda[String]#L] --> Unit]]) // error

0 commit comments

Comments
 (0)
Please sign in to comment.