Skip to content

Commit 887f2ad

Browse files
dwijnanddwijnand
committed
Force MT reduction simplification, disallow infinite match types
1 parent 8184fa8 commit 887f2ad

File tree

12 files changed

+179
-12
lines changed

12 files changed

+179
-12
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3201,7 +3201,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32013201
}
32023202
}
32033203
case redux =>
3204-
MatchResult.Reduced(redux.simplified)
3204+
MatchResult.Reduced(redux)
32053205
case _ =>
32063206
MatchResult.Reduced(body)
32073207

@@ -3229,7 +3229,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
32293229
MatchTypeTrace.noInstance(scrut, cas, fails)
32303230
NoType
32313231
case MatchResult.Reduced(tp) =>
3232-
tp
3232+
tp.simplified
32333233
case Nil =>
32343234
val casesText = MatchTypeTrace.noMatchesText(scrut, cases)
32353235
ErrorType(reporting.MatchTypeNoCases(casesText))

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -359,7 +359,7 @@ object Types {
359359
* (since these are relevant for inference or resolution) but never consider prefixes
360360
* (since these often do not constrain the search space anyway).
361361
*/
362-
def unusableForInference(using Context): Boolean = widenDealias match
362+
def unusableForInference(using Context): Boolean = try widenDealias match
363363
case AppliedType(tycon, args) => tycon.unusableForInference || args.exists(_.unusableForInference)
364364
case RefinedType(parent, _, rinfo) => parent.unusableForInference || rinfo.unusableForInference
365365
case TypeBounds(lo, hi) => lo.unusableForInference || hi.unusableForInference
@@ -369,6 +369,7 @@ object Types {
369369
case CapturingType(parent, refs) => parent.unusableForInference || refs.elems.exists(_.unusableForInference)
370370
case _: ErrorType => true
371371
case _ => false
372+
catch case ex: Throwable => handleRecursive("unusableForInference", show, ex)
372373

373374
/** Does the type carry an annotation that is an instance of `cls`? */
374375
@tailrec final def hasAnnotation(cls: ClassSymbol)(using Context): Boolean = stripTypeVar match {

‎compiler/src/dotty/tools/dotc/typer/Inferencing.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,7 @@ object Inferencing {
198198
case tp => foldOver(x, tp)
199199
}
200200
catch case ex: Throwable =>
201-
handleRecursive("check fully defined", tp.show, ex)
201+
handleRecursive("check fully defined", tp.showSummary(20), ex)
202202
}
203203

204204
def process(tp: Type): Boolean =

‎compiler/test/dotty/tools/repl/ReplCompilerTests.scala

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,62 @@ class ReplCompilerTests extends ReplTest:
169169
)
170170
}
171171

172+
@Test def i16596 =
173+
initially {
174+
run("""
175+
|import scala.compiletime.{error, ops, requireConst}, ops.int.*
176+
|import scala.quoted.*
177+
|
178+
|sealed trait Nat
179+
|object Nat:
180+
| case object Zero extends Nat
181+
| case class Succ[N <: Nat](prev: N) extends Nat
182+
|
183+
| given zero: Zero.type = Zero
184+
| given buildSucc[N <: Nat](using n: N): Succ[N] = Succ(n)
185+
|
186+
| def value[N <: Nat](using n: N): N = n
187+
|
188+
| def prevImpl[I <: Int: Type](expr: Expr[I])(using Quotes): Expr[I - 1] =
189+
| val prev = expr.valueOrAbort - 1
190+
| // this compiles, but fails at use time
191+
| //Expr(prev).asExprOf[ops.int.-[I, 1]]
192+
| Expr(prev).asInstanceOf[Expr[I - 1]]
193+
|
194+
| inline def prevOf[I <: Int](inline i: I): I - 1 = ${prevImpl('i)}
195+
|
196+
| type FromInt[I <: Int] <: Nat = I match
197+
| case 0 => Zero.type
198+
| case _ => Succ[FromInt[I - 1]]
199+
|
200+
| inline def fromInt[I <: Int & Singleton](i: I): FromInt[i.type] =
201+
| requireConst(i)
202+
| inline i match
203+
| case _: 0 => Zero
204+
| case _ =>
205+
| inline if i < 0
206+
| then error("cannot convert negative to Nat")
207+
| else Succ(fromInt(prevOf[i.type](i)))
208+
""".stripMargin)
209+
}.andThen {
210+
assertEquals(
211+
"""// defined trait Nat
212+
|// defined object Nat
213+
|""".stripMargin, storedOutput())
214+
run("Nat.fromInt(2)")
215+
}.andThen {
216+
assertEquals("val res0: Nat.Succ[Nat.Succ[Nat.Zero.type]] = Succ(Succ(Zero))", storedOutput().trim)
217+
run("summon[Nat.FromInt[2]]")
218+
}.andThen {
219+
assertEquals("val res1: Nat.Succ[Nat.Succ[Nat.Zero.type]] = Succ(Succ(Zero))", storedOutput().trim)
220+
run("Nat.fromInt(3)")
221+
}.andThen {
222+
assertEquals("val res2: Nat.Succ[Nat.Succ[Nat.Succ[Nat.Zero.type]]] = Succ(Succ(Succ(Zero)))", storedOutput().trim)
223+
run("summon[Nat.FromInt[3]]")
224+
}.andThen {
225+
assertEquals("val res3: Nat.Succ[Nat.Succ[Nat.Succ[Nat.Zero.type]]] = Succ(Succ(Succ(Zero)))", storedOutput().trim)
226+
}
227+
172228
@Test def i6200 =
173229
initially {
174230
run("""

‎tests/neg-custom-args/isInstanceOf/i17435.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,10 @@ object Test:
1414
type JsonArray = mutable.Buffer[Json]
1515

1616
def encode(x: Json): Int = x match
17-
case str: String => 1
18-
case b: Boolean => 2
19-
case i: Int => 3
20-
case d: Double => 4
17+
case str: String => 1 // error
18+
case b: Boolean => 2 // error
19+
case i: Int => 3 // error
20+
case d: Double => 4 // error
2121
case arr: JsonArray => 5 // error
2222
case obj: JsonObject => 6 // error
2323
case _ => 7

‎tests/pos/i15158.scala renamed to ‎tests/neg/i15158.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ val x = foo {
1313
type Rec[A] = A match
1414
case String => Opt[Rec[String]]
1515

16-
val arr = new Buf[Rec[String]](8)
17-
val arr2 = Buf[Rec[String]](8)
18-
val arr3 = Buf.apply[Rec[String]](8)
16+
val arr = new Buf[Rec[String]](8) // error
17+
val arr2 = Buf[Rec[String]](8) // error
18+
val arr3 = Buf.apply[Rec[String]](8) // error
1919
}
2020

2121
import scala.collection.mutable
@@ -38,6 +38,6 @@ class Spec {
3838
JsonPrimitive
3939
]
4040

41-
val arr = new mutable.ArrayBuffer[Json](8)
41+
val arr = new mutable.ArrayBuffer[Json](8) // error
4242
}
4343
}

‎tests/neg/mt-recur.cov.scala

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// like mt-recur.scala, but covariant
2+
class Cov[+T]
3+
4+
type Recur[X] = X match
5+
case Int => Cov[Recur[X]]
6+
7+
def x = ??? : Recur[Int] // error

‎tests/neg/mt-recur.scala

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// an example of an infinite recursion match type
2+
// using an _invariant_ type constructor
3+
// see mt-recur.cov.scala for covariant
4+
// used to track the behaviour of match type reduction
5+
class Inv[T]
6+
7+
type Recur[X] = X match
8+
case Int => Inv[Recur[X]]
9+
10+
def x = ??? : Recur[Int] // error

‎tests/pos/i16596.more.scala

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
import scala.compiletime.ops.int.*
2+
3+
object NatExample {
4+
sealed trait Nat
5+
object Nat {
6+
case object Zero extends Nat
7+
case class Succ[N <: Nat](prev: N) extends Nat
8+
9+
given zero: Zero.type = Zero
10+
given buildSucc[N <: Nat](using n: N): Succ[N] = Succ(n)
11+
12+
def value[N <: Nat](using n: N): N = n
13+
14+
type FromInt[I <: Int] <: Nat = I match
15+
case 0 => Zero.type
16+
case _ => Succ[FromInt[I - 1]]
17+
18+
summon[FromInt[0] =:= Zero.type]
19+
summon[FromInt[1] =:= Succ[Zero.type]]
20+
summon[FromInt[2] =:= Succ[Succ[Zero.type]]]
21+
summon[FromInt[3] =:= Succ[Succ[Succ[Zero.type]]]]
22+
summon[FromInt[4] =:= Succ[Succ[Succ[Succ[Zero.type]]]]]
23+
24+
@main def test = {
25+
require(summon[FromInt[0]] == Zero)
26+
require(summon[FromInt[1]] == Succ(Zero))
27+
require(summon[FromInt[2]] == Succ(Succ(Zero)))
28+
require(summon[FromInt[3]] == Succ(Succ(Succ(Zero))))
29+
// we can summon 4 if we write it out:
30+
require(summon[Succ[Succ[Succ[Succ[Zero.type]]]]] == Succ(Succ(Succ(Succ(Zero)))))
31+
// we cannot summon 4 using the match type
32+
//require(summon[FromInt[4]] == Succ(Succ(Succ(Succ(Zero)))))
33+
}
34+
}
35+
}

‎tests/pos/i16596.orig.scala

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
import scala.compiletime.ops.int
2+
3+
type Count0[N,T] <: Tuple = (N,T) match
4+
case (0,_) => EmptyTuple
5+
case (N,String) => String *: Count0[int.-[N, 1], String]
6+
case (N,Int) => Int *: Count0[int.-[N, 1], Int]
7+
case (N,Float) => Float *: Count0[int.-[N, 1], Float]
8+
case (N,Double) => Double *: Count0[int.-[N, 1], Double]
9+
10+
11+
type Count1[N,T] <: Tuple = (N,T) match
12+
case (0,T) => EmptyTuple
13+
case (N,String) => String *: Count1[int.-[N, 1], String]
14+
case (N,Int) => Int *: Count1[int.-[N, 1], Int]
15+
case (N,Float) => Float *: Count1[int.-[N, 1], Float]
16+
case (N,Double) => Double *: Count1[int.-[N, 1], Double]
17+
18+
def t01 = summon[Count0[1, Int] =:= Int *: EmptyTuple ]
19+
def t02 = summon[Count0[2, Int] =:= Int *: Int *: EmptyTuple]
20+
def t03 = summon[Count0[3, Int] =:= Int *: Int *: Int *: EmptyTuple]
21+
def t04 = summon[Count0[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple]
22+
def t05 = summon[Count0[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple]
23+
24+
def t11 = summon[Count1[1, Int] =:= Int *: EmptyTuple ]
25+
def t12 = summon[Count1[2, Int] =:= Int *: Int *: EmptyTuple]
26+
def t13 = summon[Count1[3, Int] =:= Int *: Int *: Int *: EmptyTuple] // was: Fail from here
27+
def t14 = summon[Count1[4, Int] =:= Int *: Int *: Int *: Int *: EmptyTuple]
28+
def t15 = summon[Count1[5, Int] =:= Int *: Int *: Int *: Int *: Int *: EmptyTuple]

0 commit comments

Comments
 (0)