macro crushes invariant type variables to Nothing #12343
Comments
|
It seems there can be a simple fix. @nicolasstucki Could you have a look or give me a tip where the logic is located? |
|
It seems like we are not collecting the constraint while matching in compiler/src/scala/quoted/runtime/impl/Matcher.scala. Maybe a missing |
|
From the logs, it seems the problem is with GADT: narrow gadt bound of type h: from above to A TypeRef(NoPrefix,type A) false
adding ordering h(param)1 <: A(param)2 to
Constraint(
uninstantiated variables: A(param)2, h(param)1
constrained types: [A(param)2] => Any, [h(param)1] => Any
bounds:
A(param)2
h(param)1
ordering:
) down1 = List(TypeParamRef(h(param)1)), up2 = List(TypeParamRef(A(param)2))
added ordering h(param)1 <: A(param)2 to
Constraint(
uninstantiated variables: A(param)2, h(param)1
constrained types: [A(param)2] => Any, [h(param)1] => Any
bounds:
A(param)2
h(param)1
ordering:
h(param)1 <: A(param)2
) = true
adding upper bound type h <: A = true
narrow gadt bound of type A: from above to h TypeRef(NoPrefix,type h) false
unifying TypeParamRef(h(param)1) TypeParamRef(A(param)2)
added ordering A(param)2 <: h(param)1 to
Constraint(
uninstantiated variables: h(param)1
constrained types: [A(param)2] => Any, [h(param)1] => Any
bounds:
A(param)2 := h(param)1
h(param)1
ordering:
) = trueAs can be seen above, the inference unifies |
|
@liufengyun this constraint is correct, how are you using it? |
Yes, it works as expected. In However, this example seems to show that we need a mechanism in constraint solving where we can influence the direction of unification. In this case, we'd like to have Or, in |
|
Why is that code not typed similarly to the following? scala> def test(x: Any) = x match
| case h: Set[h] => h: Set[h]
|
def test(x: Any): Set[?]
scala> @main def d = test(Set(1)): Set[Int]
1 |@main def d = test(Set(1)): Set[Int]
| ^^^^^^^^^^^^
|Found: Set[?1.CAP]
|Required: Set[Int]
|
|where: ?1 is an unknown value of type scala.runtime.TypeBox[Nothing, Any]Regardless of the bounds of |
|
@liufengyun again, how are you using the constraint? Are you extracting TypeBounds for EDIT: OK, I think I can guess what's happening here. Manually extracting the information out of the GADT constraint could solve this particular example, but there could be further problems down the road. Maybe it's possible to keep a set of "frozen" GADT-constrainable types in Context, types for which no further GADT bounds should be recorded? That sounds like it could work. |
I don't think reading the bounds help, as they just work as expected. Reading the bounds, we get From what I read in val ctx1 = ctx.fresh.setFreshGADTBounds.addMode(dotc.core.Mode.GadtConstraintInference)Later it ask GADT to approximate the type holes: def typeHoleApproximation(sym: Symbol) =
ctx1.gadt.approximation(sym, !sym.hasAnnotation(dotc.core.Symbols.defn.QuotedRuntimePatterns_fromAboveAnnot)).asInstanceOf[qctx1.reflect.TypeRepr].asType |
Yes, that could help as well. |
|
@LPTK From the user's perspective, they may have the same expectations. The technical difference is that in this example there is an interference of two GADT constraints -- the side effect of such interference is not expected by the programmer. Technically, it might be related to type avoidance as well --- if we have |
|
Yes, this is all about type avoidance. An existential should be introduced (the
It's not just a matter of expectations – it's a matter of the right thing to do. In case you missed it, this bug constitutes a soundness hole. If |
Good point. This means the quoted pattern match logic may have to be improved. /cc: @nicolasstucki |
|
Yes, the logic needs to improve. #12402 does to preliminary steps to be able to improve that code. |
|
Is there a process by which I can get this prioritized for 3.0.3? Thanks. |
|
Is anyone working on this? |
|
Some good news: it looks like #14026 at least fixed the soundness hole pointed out by @LPTK above which means I did my job correctly 😅 : def inv3[A](a: Set[A]): Set[Nothing] = Test.inv(a) // error:
// ^^^^^^^^^^^
// Found: Set[A(param)1]
// Required: Set[Nothing](I'm not familiar with QuoteMatcher so I can't comment on what is needed to actually infer A here instead of an unknown abstract type) |
|
@ahjohannessen you can use |
|
@nicolasstucki Thanks 👍 |
|
@nicolasstucki I tried the following with scala-cli: Test.scala: import scala.quoted._
object Test {
// Invariant (Set)
def inv(arg: Expr[Any])(using Quotes): Expr[Any] =
arg match {
case '{ $h : Set[h] } => '{ $h : Set[h] }
}
transparent inline def inv(inline arg: Any): Any =
${ inv('arg) }
// Covariant (List)
def cov(arg: Expr[Any])(using Quotes): Expr[Any] =
arg match {
case '{ $h : List[h] } => '{ $h : List[h] }
}
transparent inline def cov(inline arg: Any): Any =
${ cov('arg) }
}Run.scala: scala-cli: ~ scala-cli -S 3.1.2-RC1-bin-20220111-1292246-NIGHTLY Test.scala Run.scala
[error] ./Run.scala:5:36: Found: Set[A(param)2]
[error] Required: Set[A]
[error] def inv2[A](a: Set[A]): Set[A] = Test.inv(a)
[error] ^^^^^^^^^^^
Error compiling project (Scala 3.1.2-RC1-bin-20220111-1292246-NIGHTLY, JVM) |
|
Yep, inference isn't fixed as state in my comment, it's just the soundness bug that is fixed. |
you rang? |
|
Does anyone understand why it works in the covariant case, only failing in the invariant case? |
|
I don't. We get a TypeParamRef out of the constraint solver. Not sure if that is a new avoidance issue. |
|
The funny thing is that if you remove the precise type annotation, you get a compiler crash: object Run {
def inv2[A](a: Set[A]): Any = Test.inv(a)
}With [info] package progabs {
[info] final lazy module val Run: Run = new Run()
[info] final module class Run() extends Object() { this: Run.type =>
[info] def inv2[A >: Nothing <: Any](a: Set[A]): Set[A] = a:Set[A(param)1]
[info] }
[info] }Actually that may not be so funny for @smarter 😬 |
|
@dwijnand That's a step in the right direcrtion, but it's still wrong. Looking at your change: object Test:
// [...]
def inv2[X](a: Set[X]): Set[X] = Macro.inv(a) // doesn't compile; Set[Nothing] is inferredReferring to my comment from #12343 (comment):
I think this issue shouldn't be closed. |
|
Sorry for misleading there. That comment is from the original case. Now it infers Set[X] as desired, and sound. I should've updated the comment but I only realised after I had complete green CI runs.. |
|
Ah ok sure, good to know! I missed this was in the pos tests. Would be nice to fix the comment still 😬 |
Skunk's
sqlinterpolator has a bug in which I am unable to abstract over interpolatedEncoder[A]s because the type arguments are crushed toNothing. I have minimized it in the following dumb but small macros.Compiler version
3.0.0-RC3
Minimized code
Here is a pair of transparent macros. One takes any expression, and if it's a
Setit returns it, annotated with its own type. The other does the same, but withList.Here are some examples. In both cases calling the macros with concrete types works correctly; the passed expression is inlined with the correct type annotation. But in the case where the type argument is a type variable the covariant case works (the type is
List[A]) but in the invariant case the type isSet[Nothing]rather thanSet[A].Expectation
My expectation is that this mechanism shouldn't be sensitive to variance.
Notes
The annotated type is important in the code I generate. If I simplify the returned expressions above to simply
hthen the examples work, but I can't do this in the actual macro because it causes inference failures downstream.The text was updated successfully, but these errors were encountered: