File tree 3 files changed +53
-0
lines changed
compiler/src/dotty/tools/dotc/core
3 files changed +53
-0
lines changed Original file line number Diff line number Diff line change @@ -3057,6 +3057,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
3057
3057
disjointnessBoundary(tp.effectiveBounds.hi)
3058
3058
case tp : ErrorType =>
3059
3059
defn.AnyType
3060
+ case tp : NoType .type =>
3061
+ defn.AnyType
3060
3062
end disjointnessBoundary
3061
3063
3062
3064
(disjointnessBoundary(tp1), disjointnessBoundary(tp2)) match
Original file line number Diff line number Diff line change
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]
Original file line number Diff line number Diff line change
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
You can’t perform that action at this time.
0 commit comments