Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix match type instantiation when not approximating #17173

Closed
wants to merge 3 commits into from

Conversation

dwijnand
Copy link
Member

@dwijnand dwijnand commented Mar 29, 2023

When not approximating parameters, keep the constraint entries in a Range, so it can propagate through instantiateParams's ApproximatingTypeMap.

When not approximating parameters, keep the constraint entries in a
Range, so it can propagate through instantiateParams's ApproximatingTypeMap.
@dwijnand dwijnand force-pushed the match-types-completeness branch from d28c1df to 4f1431d Compare March 29, 2023 21:02
@dwijnand dwijnand marked this pull request as ready for review March 29, 2023 23:44
@odersky
Copy link
Contributor

odersky commented Mar 30, 2023

If I understand correctly this will essentially disallow all variable instantiations in the mode canWidenAbstract = true: Wrapping things in a Range produces a MatchResult.NoInstance in redux. So it's

  • try first with canWidenAbstract = false and allow to instantiate variables
  • if that fails, try with canWidenAbstract = true and disallow to instantiate variables

This is more restrictive than #17180, which still allows to instantiate invariant type variables even if canWidenAbstract = true. It would be good to develop tests that show the difference. I think #17180's neg test already has one such example with Array as the constructor, but we'd have to trry that out on this PR, and also find more examples.

@dwijnand
Copy link
Member Author

Yes, indeed - running locally:

Wrong number of errors encountered when compiling tests/neg/i17149.scala
expected: 1, actual: 2
Unfulfilled expectations:

Unexpected errors:
tests/neg/i17149.scala:16
-> following the errors:
 at 14: Cannot prove that Ext1[T] =:= T.

where:    T is a type in method foo with bounds <: Seq[Any]


Note: a match type could not be fully reduced:

  trying to reduce  Ext1[T]
  failed since selector T
  does not uniquely determine parameter t in
    case Seq[t] => t
  The computed bounds for the parameter are:
    t >: Any
 at 16: Cannot prove that Ext3[A] =:= B.

where:    A is a type in method foo with bounds <: Array[B]


Note: a match type could not be fully reduced:

  trying to reduce  Ext3[A]
  failed since selector A
  does not uniquely determine parameter t in
    case Array[t] => t
  The computed bounds for the parameter are:
    t >: B <: B

@dwijnand dwijnand closed this Mar 30, 2023
@dwijnand dwijnand deleted the match-types-completeness branch March 30, 2023 08:43
@dwijnand dwijnand restored the match-types-completeness branch March 30, 2023 08:57
@dwijnand dwijnand reopened this Mar 30, 2023
@dwijnand
Copy link
Member Author

Actually, as TypeAccumulator is also traversing the type, we do have the variance information to instantiate for invariance.

@@ -3095,7 +3095,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
def paramInstances(canApprox: Boolean) = new TypeAccumulator[Array[Type]]:
def apply(insts: Array[Type], t: Type) = t match
case param @ TypeParamRef(b, n) if b eq caseLambda =>
def range1(tp: Type) = Range(tp, tp)
def range1(tp: Type) = if variance == 0 then tp else Range(tp, tp)
Copy link
Contributor

@odersky odersky Mar 30, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that's still not as precise as the original solution. The original solution says:

Don't widen if the compared-to type contains variant named type parameters

Whereas here we implement a global criterion:

Under mode canWidenAbstract = true, don't instantiate variant named type parameters.

The original proposal would allow the instantiation of variant type parameters if they appear in a part of the pattern that does not correspond to a widened part of the scrutinee. Note: so far we only looked at widening of the scrutinee type as a whole, but one can easily imagine that only subparts are subject to widenings. We need tests for this! The whole thing is woefully under-tested.

It would be really good to work out the theory here. The fact that this is missing in the match type papers and thesis is a big problem.

@dwijnand dwijnand force-pushed the match-types-completeness branch from 4520faa to f331bcb Compare March 30, 2023 10:31
@dwijnand
Copy link
Member Author

Looking at #17180

@dwijnand dwijnand closed this Mar 30, 2023
@dwijnand dwijnand deleted the match-types-completeness branch March 30, 2023 10:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
2 participants