Skip to content

Commit 9093057

Browse files
wjoeltgodzik
authored andcommitted
Handle NoType in TypeComparer.disjointnessBoundary
Closes scala#20265
1 parent 7a3a297 commit 9093057

File tree

2 files changed

+51
-0
lines changed

2 files changed

+51
-0
lines changed

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[Lambda[String]#L] --> Unit].
19+
|
20+
| Note: a match type could not be fully reduced:
21+
|
22+
| trying to reduce Hinze[Fix[Lambda[String]#L] --> Unit]
23+
| failed since selector (Fix[Lambda[String]#L] --> 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)