diff --git a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala index 46c325209dee..33b592102e39 100644 --- a/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala +++ b/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala @@ -81,16 +81,26 @@ 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 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 +139,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 +189,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 +435,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"))