From f7e141d50b2ff498adc27e6fd10aadd3d13757b5 Mon Sep 17 00:00:00 2001 From: Guillaume Martres Date: Thu, 14 Apr 2022 18:01:35 +0200 Subject: [PATCH] Relax avoidance checks more for match type reduction TypeParamRefs in match types do not have a corresponding TypeVar so they get assigned level Int.MaxValue by default, this means they can refer to variables at any level, but to avoid a crash in i14921 we also need the reverse direction (they can appear in the bounds of variables of any level), both direction should be safe because these constraints only exist during match type reduction (see `MatchType#reduced`). Fixes #14921. --- .../tools/dotc/core/ConstraintHandling.scala | 29 +++++++++++-------- .../dotty/tools/dotc/typer/Inferencing.scala | 16 +++++----- tests/pos/i14921/A_1.scala | 28 ++++++++++++++++++ tests/pos/i14921/B_2.scala | 3 ++ 4 files changed, 57 insertions(+), 19 deletions(-) create mode 100644 tests/pos/i14921/A_1.scala create mode 100644 tests/pos/i14921/B_2.scala diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 46c325209dee..93364f0bccb5 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -81,16 +81,28 @@ trait ConstraintHandling { assert(homogenizeArgs == false) assert(comparedTypeLambdas == Set.empty) - def nestingLevel(param: TypeParamRef) = constraint.typeVarOfParam(param) match + def nestingLevel(param: TypeParamRef)(using Context) = constraint.typeVarOfParam(param) match case tv: TypeVar => tv.nestingLevel - case _ => Int.MaxValue + case _ => + // This should only happen when reducing match types (in + // TrackingTypeComparer#matchCases) or in uncommitable TyperStates (as + // asserted in ProtoTypes.constrained) and is special-cased in `levelOK` + // below. + Int.MaxValue + + /** Is `level` <= `maxLevel` or legal in the current context? */ + def levelOK(level: Int, maxLevel: Int)(using Context): Boolean = + level <= maxLevel || + ctx.isAfterTyper || !ctx.typerState.isCommittable || // Leaks in these cases shouldn't break soundness + level == Int.MaxValue // See `nestingLevel` above. /** If `param` is nested deeper than `maxLevel`, try to instantiate it to a * fresh type variable of level `maxLevel` and return the new variable. * If this isn't possible, throw a TypeError. */ def atLevel(maxLevel: Int, param: TypeParamRef)(using Context): TypeParamRef = - if nestingLevel(param) <= maxLevel then return param + if levelOK(nestingLevel(param), maxLevel) then + return param LevelAvoidMap(0, maxLevel)(param) match case freshVar: TypeVar => freshVar.origin case _ => throw new TypeError( @@ -129,18 +141,12 @@ trait ConstraintHandling { /** An approximating map that prevents types nested deeper than maxLevel as * well as WildcardTypes from leaking into the constraint. - * Note that level-checking is turned off after typer and in uncommitable - * TyperState since these leaks should be safe. */ class LevelAvoidMap(topLevelVariance: Int, maxLevel: Int)(using Context) extends TypeOps.AvoidMap: variance = topLevelVariance - /** Are we allowed to refer to types of the given `level`? */ - private def levelOK(level: Int): Boolean = - level <= maxLevel || ctx.isAfterTyper || !ctx.typerState.isCommittable - def toAvoid(tp: NamedType): Boolean = - tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel) + tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel, maxLevel) /** Return a (possibly fresh) type variable of a level no greater than `maxLevel` which is: * - lower-bounded by `tp` if variance >= 0 @@ -185,7 +191,7 @@ trait ConstraintHandling { end legalVar override def apply(tp: Type): Type = tp match - case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel) => + case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) => legalVar(tp) // TypeParamRef can occur in tl bounds case tp: TypeParamRef => @@ -431,7 +437,6 @@ trait ConstraintHandling { final def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type = constraint.entry(param) match case entry: TypeBounds => - val maxLevel = nestingLevel(param) val useLowerBound = fromBelow || param.occursIn(entry.hi) val inst = if useLowerBound then fullLowerBound(param) else fullUpperBound(param) typr.println(s"approx ${param.show}, from below = $fromBelow, inst = ${inst.show}") diff --git a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala index 043f931113ab..20da4723d27f 100644 --- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala +++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala @@ -637,13 +637,15 @@ trait Inferencing { this: Typer => else if v.intValue != 0 then typr.println(i"interpolate $tvar in $state in $tree: $tp, fromBelow = ${v.intValue == 1}, $constraint") toInstantiate += ((tvar, v.intValue == 1)) - else if tvar.nestingLevel > ctx.nestingLevel then - // Invariant: a type variable of level N can only appear - // in the type of a tree whose enclosing scope is level <= N. - typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint") - comparing(_.atLevel(ctx.nestingLevel, tvar.origin)) - else - typr.println(i"no interpolation for nonvariant $tvar in $state") + else comparing(cmp => + if !cmp.levelOK(tvar.nestingLevel, ctx.nestingLevel) then + // Invariant: The type of a tree whose enclosing scope is level + // N only contains type variables of level <= N. + typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint") + cmp.atLevel(ctx.nestingLevel, tvar.origin) + else + typr.println(i"no interpolation for nonvariant $tvar in $state") + ) /** Instantiate all type variables in `buf` in the indicated directions. * If a type variable A is instantiated from below, and there is another diff --git a/tests/pos/i14921/A_1.scala b/tests/pos/i14921/A_1.scala new file mode 100644 index 000000000000..755a16717b4d --- /dev/null +++ b/tests/pos/i14921/A_1.scala @@ -0,0 +1,28 @@ +import scala.compiletime.ops.int.* + +final class Label (val getLabel: String) + +trait ShapelessPolyfill { + + type Represented[R] = R match { + case IndexedSeq[a] => a + } + + type TupleSized[R, A, N <: Int] <: Tuple = N match { + case 0 => EmptyTuple + case S[n] => A *: TupleSized[R, A, n] + } + + extension [R, A, N <: Int] (s: TupleSized[R, A, N]) { + def unsized: IndexedSeq[A] = s.productIterator.toIndexedSeq.asInstanceOf[IndexedSeq[A]] + } + + type Nat = Int + + type Sized[Repr, L <: Nat] = TupleSized[Repr, Represented[Repr], L] + + object Sized { + def apply[A](a1: A): Sized[IndexedSeq[A], 1] = Tuple1(a1) + } +} +object poly extends ShapelessPolyfill diff --git a/tests/pos/i14921/B_2.scala b/tests/pos/i14921/B_2.scala new file mode 100644 index 000000000000..712b04c37c26 --- /dev/null +++ b/tests/pos/i14921/B_2.scala @@ -0,0 +1,3 @@ +import poly.* + +def failing: Tuple1[Label] = Sized(new Label("foo"))