Skip to content

Fix #9107: Restore constraints after MT reduction #9108

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

Closed
wants to merge 3 commits into from

Conversation

OlivierBlanvillain
Copy link
Contributor

Because of caseLambda = constrained(cas) in def matchCase, subtyping wrongly things that it's OK to further constrain types introduced in match type patterns. This commit fixes the issue with a stronger version of inFrozenConstraint around match type reduction.

recur(cases)
// inFrozenConstraint is not sufficient here as it doesn't prevent
// parameters of type lambdas from being added to `constraint`, see
// ConstraintHandling.canConstrain and tests/neg/9107.scala.
Copy link
Member

Choose a reason for hiding this comment

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

But why does canConstrain behave that way? To me it seems pretty surprising that isFrozenConstraint does not in fact fully freeze the constraints

Copy link
Contributor

Choose a reason for hiding this comment

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

There's an exception made for parameters of cases that are tested in a match type. These need to be instantiatable even though the constraint as a whole is frozen.

Maybe resetting the constraint should be done in matchCase? That's where we set caseLambda and where we instantiate it at the end if it's a match. So it seems to be cleaner to reset the constraint there.

@odersky odersky self-assigned this Jun 8, 2020
// `6570-1.scala` for examples that exploit emptiness to break match
// type soundness.

// If we revered the uncertainty case of this empty check, that is,
Copy link
Contributor

Choose a reason for hiding this comment

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

reversed

recur(cases)
// inFrozenConstraint is not sufficient here as it doesn't prevent
// parameters of type lambdas from being added to `constraint`, see
// ConstraintHandling.canConstrain and tests/neg/9107.scala.
Copy link
Contributor

Choose a reason for hiding this comment

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

There's an exception made for parameters of cases that are tested in a match type. These need to be instantiatable even though the constraint as a whole is frozen.

Maybe resetting the constraint should be done in matchCase? That's where we set caseLambda and where we instantiate it at the end if it's a match. So it seems to be cleaner to reset the constraint there.

@nicolasstucki nicolasstucki linked an issue Jun 24, 2020 that may be closed by this pull request
@OlivierBlanvillain
Copy link
Contributor Author

Maybe resetting the constraint should be done in matchCase? That's where we set caseLambda and where we instantiate it at the end if it's a match. So it seems to be cleaner to reset the constraint there.

That doesn't seem to work, I get an assertion error during bootstrap:

[error] ## Exception when compiling 204 sources to /home/olivier/workspace/dotty/library/../out/bootstrap/dotty-library-bootstra
pped/scala-0.26/classes                                                                                                        
[error] java.lang.AssertionError: assertion failed: param = x                                                                  
[error] constraint = Constraint(                                                                                               
[error]  uninstVars = ;                                                                                                        
[error]  constrained types =                                                                                                   
[error]  bounds =                                                                                                              
[error]  ordering =                                                                                                            
[error] )                                                                                                                      
[error] dotty.DottyPredef$.assertFail(DottyPredef.scala:17)                                                                    
[error] dotty.tools.dotc.core.ConstraintHandling.approximation(ConstraintHandling.scala:292)                                   

Because of `caseLambda = constrained(cas)` in `def matchCase`, subtyping
wrongly things that it's OK to further constrain types introduced in match
type patterns. This commit fixes the issue with a stronger version of
`inFrozenConstraint` around match type reduction.
This subtyping check use to work because of the bug in question. Note that
6697 tries to use GADT knowledge that is currently unavailable on expression
patterns (as demonstrated in 6697-2.scala), so I don't think we are in a urge
to support this with match types.
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.

Match type subtyping wrongly instantiates types in patterns
3 participants