Support const evaulation #596

hayashi-stl · 2020-08-19T17:11:02Z

Fixes #548
For Chalk's tests, a special-formatted Option<u32> is used, where Some(n) evaluates to n and None evaluates to a specific but unknown constant. Some(n) is formatted as n? and None is formatted as ?.

jackh726

Just a quick first pass.

jackh726 · 2020-08-19T17:44:11Z

chalk-engine/src/slg/aggregate.rs

@@ -483,6 +483,44 @@ impl<I: Interner> AntiUnifier<'_, '_, I> {
                }
            }

+            (ConstValue::Concrete(e), ConstValue::Unevaluated(u))


Initial thought: Will we ever actually give an answer with an Unevaluated const?

I don't see why not. Chalk can return associated type projections in answers, and an unevalutated const is basically a projection.

jackh726 · 2020-08-19T17:52:08Z

chalk-engine/src/slg/resolvent.rs

+                match u.try_eval(answer_ty, interner) {
+                    Ok(ev) => assert!(c.const_eq(answer_ty, &ev, interner)),
+
+                    Err(ConstEvalError::TooGeneric) => panic!(


Similarly here...feels like we should have already have caught this before and the answer itself (or the goal) shouldn't have unevaluated consts. (Well...maybe the goal would?)

Turns out that unevaluated const expressions can appear in the answer and the goal in the resolvent if we so much as write impl Foo<3?> for Baz {}.

chalk-integration/src/interner.rs

chalk-ir/src/interner.rs

chalk-ir/src/lib.rs

chalk-parse/src/parser.lalrpop

jackh726 · 2020-08-19T18:13:18Z

tests/test/constants.rs

+                S<N>: Trait
+            }
+        } yields {
+            "Unique; substitution [?0 := 3?], lifetime constraints []"


Ah, interesting. I have to think if this is something we want to be able to support. (Giving solutions with unevaluated consts). It's pretty clear that these would have to be evaluable, since they would have to pass WF/coherence checks.

tests/test/constants.rs

jackh726 · 2020-08-19T18:15:48Z

tests/test/constants.rs

+        goal {
+            S<?>: Trait
+        } yields {
+            "Unique"


See, this should be Ambiguous, for a similar reason that two InferenceVars aren't the same: we don't actually know this would evaluate to the same const.

I've been assuming that for chalk testing purposes that ? evaluates to a specific but unknown constant. I don't feel like breaking reflexivity.

But that's not true. The point here is that ? represents a constant that can't be evaluated yet. Importantly, if you have two constants that can't be evaluated (e.g. {N+1} and {X +1}), then we can't say that if there is a solution that covers one case, there is a solution that covers all cases.

As it turns out, removing const_eq for unevaluated consts and assuming that two ?s don't necessarily evaluate to the same value breaks LocalImplAllowed(Baz: Foo<?>) in the unevaluated_const_unknown coherence test.

That's probably okay and what we expect :) That can be a lowering_error

Wouldn't it be weird for it to fail because it violated the orphan rules, though? impl Foo<?> for Baz isn't violating the orphan rules because Foo is local.

Oops, I never responded to this. Sorry about that.

So, I think theoretically we could always say that impl Foo<?0> for Baz {} never violates orphan rules, since both Foo and Baz are local. However, I think for unevaluated consts, it's okay to say it's Ambiguous if we get TooGeneric. I would have to look more into the orphan rules code to figure out how to best handle this. For this PR, we can mark a comment or FIXME and file a followup issue for more discussion.

tests/test/constants.rs

tests/test/coherence.rs

jackh726 · 2020-08-28T21:13:38Z

tests/test/coherence.rs

+// FIXME: The following test fails by violation of the orphan rules.
+// This is because right now, unevaluated const expressions have a
+// temporary reflexivity hole, where ? != ?,
+// which messes with the SLG resolvent.
+// The test should be uncommented when the reflexivity hole is fixed.
+// It is supposed to fail because of overlapping impls.


See above. What error do we get here if we leave these uncommented? With these, we actually don't know that these are overlapping impls (could impl Foo<3> and impl Foo<4>). But this still shouldn't lower successfully.

Right now it's structural mismatch between answer '?' and pending goal '?'. Is the resolvent allowed to create a CannotProve goal? Also, in the case where chalk can't prove that impls don't overlap, it assumes that they do.

tests/test/constants.rs

chalk-solve/src/infer/unify.rs

bors · 2020-09-11T17:28:55Z

☔ The latest upstream changes (presumably #606) made this pull request unmergeable. Please resolve the merge conflicts.

Note that reviewers usually do not review pull requests until merge conflicts are resolved! Once you resolve the conflicts, you should change the labels applied by bors to indicate that your PR is ready for review. Post this as a comment to change the labels:

@rustbot modify labels: +S-waiting-on-review -S-waiting-on-author

nikomatsakis · 2020-10-16T20:18:47Z

chalk-ir/src/interner.rs

+    /// `InternedUnevaluatedConst` instances are not created by chalk,
+    /// it can only evaluate them with the [`try_eval_const`] method
+    /// and check for (syntactic for now) equality between them.
+    type InternedUnevaluatedConst: Debug + Clone + Eq + Hash;


Do we anticipate that this will carry a "substitutions"?

I expect not, right?

nikomatsakis · 2020-10-16T20:22:29Z

chalk-ir/src/interner.rs

+        &self,
+        ty: &Self::InternedType,
+        constant: &Self::InternedUnevaluatedConst,
+    ) -> Result<Self::InternedConcreteConst, ConstEvalError>;


I kind of expect this to take a set of substitutions. Consider how the rustc variant looks.

nikomatsakis · 2020-10-16T20:26:12Z

chalk-solve/src/infer/unify.rs

+            // Note that we assume that the unevaluated const doesn't contain inference variables.
+            // Also, for now, the unevalutable unevaluated const is too generic.
+            (&ConstValue::InferenceVar(_), &ConstValue::Unevaluated(_))
+            | (&ConstValue::Unevaluated(_), &ConstValue::InferenceVar(_)) => Ok(self.goals.push(


Hmm, I think I expected us to unify an inference variable here...

nikomatsakis · 2020-10-16T20:26:38Z

chalk-solve/src/infer/unify.rs

@@ -440,9 +452,23 @@ impl<'t, I: Interner> Unifier<'t, I> {
                }
            }

+            // For now, the unevalutable unevaluated const is too generic.
+            (&ConstValue::Concrete(_), &ConstValue::Unevaluated(_))
+            | (&ConstValue::Unevaluated(_), &ConstValue::Concrete(_)) => Ok(self.goals.push(


...and then to generate a subobligation here, kind of like associated type normalization. Is this planned for "future PRs" or is my idea of how to approach this outdated :)

nikomatsakis · 2020-10-16T20:33:00Z

tests/test/coherence.rs

+    }
+}
+
+// FIXME: The following test fails by structural mismatch of ? and ?


What does this FIXME mean exactly?

jackh726 · 2020-10-22T04:07:50Z

We discussed this in our meeting Tuesday. The conclusion was that the PR as-is isn't correct (see @nikomatsakis's review). Part of this is we need better direction for how consts will be handled.

I'm going to go ahead and close this for now. @josh65536 if you still want to work on this, feel free to reopen. Either Niko or I can answer questions on here or, preferably, Zulip. We really would like to get this over the finish line :)

hayashi-stl added 4 commits August 19, 2020 11:35

Basic support for unevaluated const expressions

eea70d6

Merge branch 'master' of https://github.com/josh65536/chalk

58fb4ff

Code formatting and unevaluated const formatting

e0748ad

Fixed tests

69623ba

jackh726 requested changes Aug 19, 2020

View reviewed changes

hayashi-stl added 4 commits August 20, 2020 14:50

Added newline, deleted unnecessary try_eval functions

b4684d0

Added comments on tests

f4cd784

Moved UnevaluatedConstData to chalk-integration

f2ca1db

Removed const_eq for unevaluated consts. Rip reflexivity for now.

d767d7e

jackh726 requested changes Aug 28, 2020

View reviewed changes

hayashi-stl added 9 commits August 29, 2020 22:42

Merge branch 'master' of https://github.com/rust-lang/chalk

6a6a68f

Fixed tests

3389719

Added newline, deleted unnecessary try_eval functions

bce9291

Added comments on tests

0b603f9

Moved UnevaluatedConstData to chalk-integration

d4ee9a3

Removed const_eq for unevaluated consts. Rip reflexivity for now.

d05b66c

Disabled coherence in failing test and fixed comments in coherence tests

60da39c

Oops, merge conflicts

1c38d7c

Deduplicated some logic and fixed a test

e048d93

nikomatsakis reviewed Oct 16, 2020

View reviewed changes

jackh726 closed this Oct 22, 2020

flodiebold mentioned this pull request May 13, 2021

Support const generics rust-lang/rust-analyzer#8655

Open

6 tasks

jackh726 mentioned this pull request Dec 7, 2021

Support const evaluation #736

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support const evaulation #596

Support const evaulation #596

hayashi-stl commented Aug 19, 2020 •

edited

Loading

jackh726 left a comment

jackh726 Aug 19, 2020

hayashi-stl Aug 28, 2020

jackh726 Aug 19, 2020

hayashi-stl Aug 22, 2020

jackh726 Aug 19, 2020

jackh726 Aug 19, 2020

hayashi-stl Aug 20, 2020

jackh726 Aug 20, 2020

hayashi-stl Aug 21, 2020

jackh726 Aug 21, 2020

hayashi-stl Aug 22, 2020

jackh726 Aug 27, 2020

jackh726 Aug 28, 2020

hayashi-stl Aug 30, 2020

bors commented Sep 11, 2020

nikomatsakis Oct 16, 2020

nikomatsakis Oct 16, 2020

nikomatsakis Oct 16, 2020

nikomatsakis Oct 16, 2020

nikomatsakis Oct 16, 2020

nikomatsakis Oct 16, 2020

jackh726 commented Oct 22, 2020

Support const evaulation #596

Support const evaulation #596

Conversation

hayashi-stl commented Aug 19, 2020 • edited Loading

jackh726 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bors commented Sep 11, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jackh726 commented Oct 22, 2020

hayashi-stl commented Aug 19, 2020 •

edited

Loading