we only need to prove things one way #754

nikomatsakis · 2022-03-10T21:37:02Z

Partially addresses #727 (some work is left for future work).

chalk-recursive/src/solve.rs

flodiebold · 2022-03-11T13:59:52Z

I tried out this patch with rust-analyzer on the rust-analyzer codebase:

> $ ./ra-chalk-master -q analysis-stats . 
Database loaded:     1.23s, 246minstr (metadata 747.44ms, 24minstr; build 266.50ms, 9338kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     17.80s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 155
Inference:           102.34s, 375ginstr
Total:               120.14s, 453ginstr

> $ ./ra-chalk-niko -q analysis-stats . 
Database loaded:     1.14s, 245minstr (metadata 720.16ms, 24minstr; build 222.83ms, 9060kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     17.82s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 17
Inference:           96.19s, 361ginstr
Total:               114.01s, 439ginstr

> $ ./ra-chalk-niko-early-exit -q analysis-stats .
Database loaded:     1.15s, 245minstr (metadata 711.23ms, 24minstr; build 206.14ms, 9085kinstr)
  crates: 39, mods: 857, decls: 19554, fns: 14566
Item Collection:     16.40s, 78ginstr
  exprs: 400526, ??ty: 342 (0%), ?ty: 514 (0%), !ty: 17
Inference:           75.01s, 318ginstr
Total:               91.41s, 396ginstr

So this patch fixes almost all remaining type mismatches (that's the !ty) we have on our codebase, and with the early exit I mentioned it actually improves inference time by 25%!

I inspected the results, seems good

nikomatsakis · 2022-03-16T00:31:25Z

@flodiebold ready to merge, I think

tests/test/misc.rs

jackh726 · 2022-03-16T00:40:05Z

tests/test/misc.rs

        } yields[SolverChoice::slg_default()] {
            expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
        } yields[SolverChoice::recursive_default()] {
-            expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
+            expect![[r#"Ambiguous; no inference guidance"#]]
        }


These are, I believe, equivalent. That substitution is an "identity substitution", so it's not very useful guidance. I looked into why this was coming about -- it's because I removed the (erroneous) "early exit" that was causing us to bail out early. What we now do is bail out because we see ?T: '?a for some unknown ?T and we can't make progress (in fact, we could see that it's in the environment, but the code doesn't do that today).

jackh726

A few points, but I'm okay if we want to merge this.

jackh726 · 2022-03-18T20:40:05Z

tests/test/misc.rs

        } yields[SolverChoice::slg_default()] {
            expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
        } yields[SolverChoice::recursive_default()] {
-            expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
+            expect![[r#"Ambiguous; no inference guidance"#]]
        }


The fact these are still different bothers me. Also, SLG is still given the identity solution as "ambiguous", which is somewhat at odds with what the aggregate hack is saying, right?

jackh726 · 2022-03-18T20:40:34Z

tests/test/ambiguity_issue_727.rs

@@ -0,0 +1,133 @@
+use super::*;


I feel like I'd like to see these tests more properly categorized. But I don't know how strongly I feel about it.

Makes sense-- but I'm not sure where to categorize them!

jackh726 · 2022-03-18T20:41:29Z

chalk-engine/src/slg/aggregate.rs

@@ -83,9 +91,11 @@ impl<I: Interner> AggregateOps<I> for SlgContextOps<'_, I> {
                break Guidance::Unknown;
            }

+            // FIXME: This may cause us to miss some "trivially true" answers maybe? Haven't investigated very deeply.


I'm guessing this is the cause of the test I pointed out.

jackh726 · 2022-03-18T20:42:49Z

chalk-engine/src/slg/aggregate.rs

@@ -46,8 +46,16 @@ impl<I: Interner> AggregateOps<I> for SlgContextOps<'_, I> {
            }
        };

+        // If the answer is trivially true and thus subsumes all others, then that's a unique-enough answer for us :)


Maybe at least a comment that this is hacky would be nice.

This reverts commit 502d989.

nikomatsakis · 2022-04-12T15:25:25Z

I reverted the last commit

jackh726

r=me with issue opened to reconcile ambiguous vs unique, and how they different between the two solvers

nikomatsakis · 2022-04-12T15:56:58Z

@bors r+

bors · 2022-04-12T15:57:00Z

📌 Commit 70b2fdb has been approved by nikomatsakis

bors · 2022-04-12T15:57:06Z

⌛ Testing commit 70b2fdb with merge 3e3f76a...

nikomatsakis · 2022-04-12T15:58:08Z

Filed #760

lnicola · 2022-04-12T16:00:12Z

Would it be possible to trigger an early publish? We want to get our hands on this in RA, and upgrading sooner will let us find any issues before the next release.

jackh726 · 2022-04-12T16:01:47Z

I can kick off a release later today.

bors · 2022-04-12T16:08:27Z

☀️ Test successful - checks-actions
Approved by: nikomatsakis
Pushing 3e3f76a to master...

jackh726 · 2022-04-12T16:44:53Z

0.82.0 released

lnicola · 2022-04-12T17:28:26Z

with the early exit I mentioned it actually improves inference time by 25%!

Strangely, I'm not seeing that large of a difference:

baseline
Database loaded:     1.79s, 244minstr (metadata 420.87ms, 24minstr; build 1.29s, 8944kinstr)
  crates: 39, mods: 878, decls: 20758, fns: 15517
Item Collection:     9.90s, 79ginstr
58  exprs: 425364, ??ty: 325 (0%), ?ty: 145 (0%), !ty: 142                                                                                                         
Inference:           53.36s, 405ginstr
Total:               63.25s, 484ginstr

chalk-0.82
Database loaded:     1.22s, 244minstr (metadata 413.94ms, 24minstr; build 727.46ms, 8602kinstr)
  crates: 39, mods: 878, decls: 20758, fns: 15517
Item Collection:     9.87s, 79ginstr
  exprs: 425364, ??ty: 325 (0%), ?ty: 145 (0%), !ty: 1                                                                                                             
Inference:           48.90s, 373ginstr
Total:               58.77s, 452ginstr

lnicola · 2022-04-12T17:32:19Z

Sure, but flodiebold reported a 25% speed-up vs. the 8% I got. Still good, but a bit unexpected.

nikomatsakis added 2 commits March 10, 2022 16:35

start of a fix for rust-lang#727

f979cd1

mark the failing test as "WIP"

d55a9a2

nikomatsakis mentioned this pull request Mar 10, 2022

Recursive solver reports ambiguity #727

Open

nikomatsakis linked an issue Mar 10, 2022 that may be closed by this pull request

Recursive solver reports ambiguity #727

Open

nikomatsakis removed a link to an issue Mar 10, 2022

Recursive solver reports ambiguity #727

Open

flodiebold reviewed Mar 11, 2022

View reviewed changes

chalk-recursive/src/solve.rs Show resolved Hide resolved

nikomatsakis added 2 commits March 15, 2022 20:03

fix tests

2e759c1

I inspected the results, seems good

add a fast path

a5083eb

nikomatsakis force-pushed the issue-727 branch from 0e94e3d to a5083eb Compare March 16, 2022 00:30

jackh726 reviewed Mar 16, 2022

View reviewed changes

lnicola mentioned this pull request Mar 17, 2022

fix: Properly unify receivers during method resolution rust-lang/rust-analyzer#11743

Merged

extend SLG solver with a similar optimization

502d989

jackh726 requested changes Mar 18, 2022

View reviewed changes

This was referenced Mar 25, 2022

Type-mismatch error boxed Trait rust-lang/rust-analyzer#11818

Closed

Fix another const generic panic rust-lang/rust-analyzer#11840

Merged

rust-analyzer gets confused on variable type when using the use_async yew hook. rust-lang/rust-analyzer#11510

Open

Revert "extend SLG solver with a similar optimization"

70b2fdb

This reverts commit 502d989.

jackh726 approved these changes Apr 12, 2022

View reviewed changes

nikomatsakis mentioned this pull request Apr 12, 2022

reconcile SLG/recursive solver's attempts to merge multiple results #760

Open

bors merged commit 3e3f76a into rust-lang:master Apr 12, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

we only need to prove things one way #754

we only need to prove things one way #754

nikomatsakis commented Mar 10, 2022

flodiebold commented Mar 11, 2022

nikomatsakis commented Mar 16, 2022

jackh726 Mar 16, 2022

nikomatsakis Mar 16, 2022

jackh726 left a comment

jackh726 Mar 18, 2022

jackh726 Mar 18, 2022

nikomatsakis Apr 12, 2022

jackh726 Mar 18, 2022

jackh726 Mar 18, 2022

nikomatsakis commented Apr 12, 2022

jackh726 left a comment

nikomatsakis commented Apr 12, 2022

bors commented Apr 12, 2022

bors commented Apr 12, 2022

nikomatsakis commented Apr 12, 2022

lnicola commented Apr 12, 2022

jackh726 commented Apr 12, 2022

bors commented Apr 12, 2022

jackh726 commented Apr 12, 2022

lnicola commented Apr 12, 2022 •

edited

Loading

lnicola commented Apr 12, 2022 •

edited

Loading

we only need to prove things one way #754

we only need to prove things one way #754

Conversation

nikomatsakis commented Mar 10, 2022

flodiebold commented Mar 11, 2022

nikomatsakis commented Mar 16, 2022

jackh726 Mar 16, 2022

Choose a reason for hiding this comment

nikomatsakis Mar 16, 2022

Choose a reason for hiding this comment

jackh726 left a comment

Choose a reason for hiding this comment

jackh726 Mar 18, 2022

Choose a reason for hiding this comment

jackh726 Mar 18, 2022

Choose a reason for hiding this comment

nikomatsakis Apr 12, 2022

Choose a reason for hiding this comment

jackh726 Mar 18, 2022

Choose a reason for hiding this comment

jackh726 Mar 18, 2022

Choose a reason for hiding this comment

nikomatsakis commented Apr 12, 2022

jackh726 left a comment

Choose a reason for hiding this comment

nikomatsakis commented Apr 12, 2022

bors commented Apr 12, 2022

bors commented Apr 12, 2022

nikomatsakis commented Apr 12, 2022

lnicola commented Apr 12, 2022

jackh726 commented Apr 12, 2022

bors commented Apr 12, 2022

jackh726 commented Apr 12, 2022

lnicola commented Apr 12, 2022 • edited Loading

lnicola commented Apr 12, 2022 • edited Loading

lnicola commented Apr 12, 2022 •

edited

Loading

lnicola commented Apr 12, 2022 •

edited

Loading