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

Instantiate more type variables to hard unions #15632

Merged
merged 5 commits into from
Sep 1, 2022

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jul 9, 2022

Fixes #14770

@odersky odersky marked this pull request as draft July 9, 2022 12:10
@odersky odersky marked this pull request as ready for review July 9, 2022 18:34
@odersky odersky requested a review from smarter July 9, 2022 18:34
@odersky
Copy link
Contributor Author

odersky commented Jul 9, 2022

I was hoping this would give some leverage for avoiding errors caused by level checking, but alas that's not the case. Nevertheless it seems useful to support the scenario of #14770.


val res = widenOK
|| joinOK
|| (tp1.isSoft || constrainRHSVars(tp2)) && recur(tp11, tp2) && recur(tp12, tp2)
Copy link
Member

Choose a reason for hiding this comment

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

Can this mechanism replaces the existing constrainRHSVars hack? As mentioned in #14770 (comment) this is supposed to handle this sort of cases, but it's incomplete and break internal invariants. I'd feel more comfortable adding new code here if we could remove the existing hacks first.

Copy link
Contributor Author

@odersky odersky Aug 20, 2022

Choose a reason for hiding this comment

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

I tried now, and the answer is no. We already can't build the compiler itself if we disable constrainRHSVars.

Copy link
Member

@smarter smarter left a comment

Choose a reason for hiding this comment

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

I won't have time reviewing this in more details but I'm not comfortable merging this as is. I think a TypeComparer-wide mode that gets set temporarily as we add the constraint as I hypothesized in #14770 would be easier to reason about.

// loop for a very long time without the recursion brake.
def hardenTypeVars(tp2: Type): Unit = tp2.dealiasKeepRefiningAnnots match
case tvar: TypeVar if constraint.contains(tvar.origin) =>
tvar.widenUnions = false
Copy link
Member

Choose a reason for hiding this comment

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

This seems very dangerous to me. The particular subtype check we're doing might be part of a TyperState that ends up being rolled back, but the mutation here will be preserved. This will make it extremely hard to debug any issue involving widening, and any change in inference could break existing code because this flag happens to be toggled.

Copy link
Contributor Author

@odersky odersky Jul 10, 2022

Choose a reason for hiding this comment

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

bccbaf7 now keeps this info in TyperState.

@smarter smarter removed their assignment Jul 9, 2022
@odersky
Copy link
Contributor Author

odersky commented Jul 9, 2022

I think a TypeComparer-wide mode that gets set temporarily as we add the constraint as I hypothesized in #14770 would be easier to reason about.

I think that would be harder to reason about since it is a global side effect, and you don't know what it will influence. Propagating windenUnion parameters is arduous, but at least we know exactly what they influence.

* to hard unions instead of being widened in `widenOr`.
*/
private var myRigidVars: TypeVars = _
def rigidVars: TypeVars = myRigidVars
Copy link
Member

Choose a reason for hiding this comment

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

I like this much more 😅, but I think the name could be misleading: usually "rigid variables" are variables that cannot be constrained at all (like the type parameters of a method as seen from inside that method). Maybe go with hardVars instead in keeping with hardenVars?

@@ -548,24 +554,41 @@ trait ConstraintHandling {
wideInst.dropRepeatedAnnot
end widenInferred

/** Convert all toplevel union types in `tp` to hard unions */
extension (tp: Type) private def hardenUnions(using Context): Type = tp.widen match
Copy link
Member

Choose a reason for hiding this comment

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

My original idea was to change https://github.com/lampepfl/dotty/blob/6540ad9154797164561281080b6a4e24a191691d/compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala#L266 which currently uses | (and thus creates soft unions) to instead check a flag to decide whether to use a soft or hard union. This would avoid having to convert unions after creating them, and it means we can reset the flag after adding the constraint.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

The problem I see with this is that the lower bound might be a union with type variables in it. In that case the type variables would end up in the ordering constraint and there would be no union to harden until the time we instantiate the type variable.

Copy link
Member

Choose a reason for hiding this comment

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

I see, so we couldn't reset the flag but could check hardVars in ConstraintHandling when we create the unions I think, that would cover unions created later from propagating constraints based on ordering.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think hardVars belongs in TyperState. If it's in ConstraintHandling we would lose it when we commit a constraint.

Copy link
Member

Choose a reason for hiding this comment

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

Right, I meant we could leave it in TyperState but check it in ConstraintHandling#addOneBound instead of checking it in TypeVar#instantiate, but I don't know if we're actually supposed to access the currrent TyperState from ConstraintHandling.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

But addOneBound does not necessarily create a union. The union might be created by fullBounds when we instantiate the variable.

Copy link
Member

Choose a reason for hiding this comment

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

But as far as I can tell we don't use fullBounds to instantiate a type variable (except for GADTs but we know that's problematic: #14288)

Copy link
Contributor Author

Choose a reason for hiding this comment

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

We do use fullLowerBound in approximation.

Copy link
Member

Choose a reason for hiding this comment

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

Ah that's right, so we'd have to check hardVars both in addOneBound and fullLowerBound, I'm neutral on whether this is better than the current scheme.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think it's better to tie it to typevariable instantiation, since we do fullLowerBound also elsewhere. We could possibly add it to approximate, but maybe that mixes up things too much.

@dwijnand
Copy link
Member

This looks too involved for me to review with little time, but I'll get back to this when I'm back - sorry for the delay.

Try alternative to track hard typevars in constraint instead of typer state. This avoids the problem
that a failing subtype comparison can also mark type variables as hard.
It seems constrainRHSVars is no longer needed with the new way to keep track
of hard type variables.
@odersky
Copy link
Contributor Author

odersky commented Aug 30, 2022

@smarter I think it now addresses your concerns. Do you have time to take a look again?

@odersky odersky assigned smarter and unassigned dwijnand Aug 30, 2022
@smarter
Copy link
Member

smarter commented Aug 30, 2022

Nice! I'll have a look tomorrow.

Copy link
Member

@smarter smarter left a comment

Choose a reason for hiding this comment

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

Otherwise LGTM!

tvars.foreach(tvar =>
if !tvar.inst.exists then
if !isOwnedAnywhere(this, tvar) then includeVar(tvar)
if other.isHard(tvar) then constraint = constraint.withHard(tvar))
Copy link
Member

Choose a reason for hiding this comment

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

This code path is only executed if constraint.contains(tl) is false above, but if the same type lambda appears in both constraints, they could still have different sets of hardened tvars. So I think this logic needs to be moved below inside the argument to constraint.uninstVars.forall.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Ah yes, well spotted.

@odersky odersky merged commit bf03086 into scala:main Sep 1, 2022
@odersky odersky deleted the fix-14770 branch September 1, 2022 07:58
@Kordyjan Kordyjan added this to the 3.2.1 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Type inference difficulties with UndefOr[A | B]
4 participants