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

Refinements to realizability #5568

Merged
merged 6 commits into from Dec 7, 2018
Merged

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Dec 5, 2018

This was another attempt to fix #4031 without breaking other things, before I found out that
it was not a fixable bug, after all. Keeping the bits that are still of value.

Supersedes #4036 and #5559.

I had a TypeError crash in refchecks after screwing up a typeclass encoding
in a particularly bad way. This commit reports an error instead.
Add the rule T <: Any for any *-Type T. This was not include fully before. We
did have the rule that T <: Any, if Any is in the base types of T. However,
it could be that the base type wrt Any does not exist. Example:

    Any#L <: Any

yielded false before, now yields true. This error manifested itself in i4031.scala.

With the new rule, we can drop again the special case in derivedSelect.
@odersky
Copy link
Contributor Author

odersky commented Dec 5, 2018

test performance please

@dottybot
Copy link
Member

dottybot commented Dec 5, 2018

performance test scheduled: 1 job(s) in queue, 0 running.

@odersky
Copy link
Contributor Author

odersky commented Dec 5, 2018

Something wrong with the CI? Test output for bootstrapped after 17.06 minutes is

Exit code 1

and nothing else.

@dottybot
Copy link
Member

dottybot commented Dec 5, 2018

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5568/ to see the changes.

Benchmarks is based on merging with master (ce62b37)

Unstable types can still be realizable (i.e. if their underlying
type is concrete with no bad bounds).
@odersky odersky changed the title Fix #4031: 4th attempt Refinements to realizability Dec 5, 2018
@odersky
Copy link
Contributor Author

odersky commented Dec 5, 2018

Turns out, #4031 was not a bug (or, rather, not a bug that should be fixed before we track nullability). Keeping the rest of this PR since it refines realizability in useful ways.

if (tp1.isLambdaSub) return false
if (cls2 eq AnyClass) return true
// Note: We would like to replace this by `if (tp1.hasHigherKind)`
Copy link
Member

Choose a reason for hiding this comment

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

This comment is now attached to the wrong line (it refers to isLambdaSub above)

Copy link
Contributor

Choose a reason for hiding this comment

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

Addressed.

@odersky
Copy link
Contributor Author

odersky commented Dec 5, 2018

@Blaisorblade I propose the following order to finish with realizability: You do a quick review of #5568 and we merge it. Then we rebase #5558 on top of the merged master and I review that one in turn. Sounds good?

Copy link
Contributor

@Blaisorblade Blaisorblade left a comment

Choose a reason for hiding this comment

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

LGTM.

For the record, I was worried because paths ending in unstable symbols can now be considered realizable — but we assume that paths are separately checked for stability. Indeed, paths written in source code appear to be checked via checkStable (if not, that should be fixed separately). realizability(tp) must still test isStable because tp might not arise from paths in the source code, but overall this seems sufficient.

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.

Good old unsoundness, CCE
4 participants