Use substitutions and suggestions in Solution; implement negation #36

aturon · 2017-05-27T02:34:31Z

This commit is a major refactoring with a few goals:

Move Solution to a Unique/Ambiguous model, with the ambiguous case
encompassing multiple forms of guidance for type inference (including
"suggestions" intended to be applied as fallback).
Remove the notion of goal refinement, and instead use substitutions
for communicating solutions.
Draw a more clear line between the generic Chalk engine (which "only
knows Prolog", i.e. doesn't know anything special about Rust) and
lowering. Put differently, everything specific to Rust should now be
encoded in the lowering, rather than though special cases in the Chalk
engine.
Consolidate the solver code so that the "strategies" for solving leaf
goals are more clear and all co-located.
Introduce some of the heuristics that rustc performs for inference,
e.g. preferring where clauses for influencing inference. We do this
in a way that decouples the heuristics from the rest of the solver;
the favor_over method, in particular, contains the relevant logic.
Introduce not { ... } as a logical operator, using negation-as-failure
semantics adjusted for our "three-valued" logic.

aturon · 2017-05-27T02:34:45Z

aturon · 2017-05-27T02:36:54Z

src/solve/infer/test.rs

-            binders: vec![ParameterKind::Ty(U1), ParameterKind::Ty(U0), ParameterKind::Ty(U2)],
-        });
-}
+// #[test]


Oops, forgot to get back to these.

aturon · 2017-05-28T08:57:03Z

I've now pushed up a commit with a preliminary implementation of negation, which is straightforward to add. However, it doesn't currently handle forall variables correctly when it comes to unification: you can prove forall<T, U> { not { T = U } }. This is straightforward to fix, but will require a refactor of unification to plumb the needed information. Will do that soon.

aturon · 2017-05-30T17:05:58Z

I've now pushed up an additional commit which adjusts the treatment of unification for skolemized type variables so that negation does the Right Thing. TLDR: we now treat forall<T, U> { T = U } as ambiguous, rather than false (by treating the inner equality as ambiguous); that means that we correctly also say that forall<T, U> { not { T = U } } is ambiguous.

aturon · 2017-05-31T00:45:19Z

Update: now includes a commit that implements normalization fallback via lowering to negation!

This commit is a major refactoring with a few goals: - Move `Solution` to a Unique/Ambiguous model, with the ambiguous case encompassing multiple forms of guidance for type inference (including "suggestions" intended to be applied as fallback). - Remove the notion of goal refinement, and instead use substitutions for communicating solutions. - Draw a more clear line between the generic Chalk engine (which "only knows Prolog", i.e. doesn't know anything special about Rust) and lowering. Put differently, everything specific to Rust should now be encoded in the lowering, rather than though special cases in the Chalk engine. This work is somewhat incomplete: the commit removes the normalization fallback, which was one major special case, but doesn't yet replace it. A follow up PR will introduce negation and use it in lowering to recover this fallback. - Consolidate the solver code so that the "strategies" for solving leaf goals are more clear and all co-located. - Introduce some of the heuristics that rustc performs for inference, e.g. preferring `where` clauses for influencing inference. We do this in a way that decouples the heuristics from the rest of the solver; the `favor_over` method, in particular, contains the relevant logic.

Introduce `not { ... }` as a logical operator, using negation-as-failure semantics adjusted for our "three-valued" logic. WIP; currently doesn't handle `forall` correctly for unification.

…, thereby correcting the semantics with respect to negation

This commit introduces a new domain goal: `KnownProjection`. It holds whenever you're able to directly normalize a projection, i.e. through an impl or where clause. Normalizations are then expanded to include a fallback precisely in the cases where `KnownProjection` cannot be proved.

aturon · 2017-05-31T00:51:00Z

OK, this PR is as big as it's going to get -- it now does not regress Chalk in any way, and fleshes out the complete story for negation.

I'll be working on the compat modality next, bound for a fresh PR.

withoutboats · 2017-05-31T01:01:58Z

Do you think this will be stable enough to branch off for overlap/specialization or should I wait until its landed?

aturon · 2017-05-31T01:05:18Z

@withoutboats I expect it to be stable, unless @nikomatsakis has a very surprising reaction to it :-)

nikomatsakis

This is great! I left various nits, along with a few more serious questions. Nothing major though.

nikomatsakis · 2017-05-31T00:57:00Z

src/fold/mod.rs

+        let mut lifetimes = BTreeMap::new();
+
+        for (var, ty) in &self.tys {
+            tys.insert(*var, ty.fold_with(folder, binders)?);


Nit: can't we write this with some kind of fancy collect() call? ;) (don't feel obligated)

The ? here is what seems to make the imperative more clear and nearly as concise, sadly.

Maybe something like this?

let tys = self.tys.iter() .map(|(&var, ty)| (var, ty.fold_with(folder, binders)?)) .collect::<Result<BTreemap<_, _>>>()?;

Anyway, doesn't matter. More readable this way =)

Right, that's exactly what I mean -- I find this iterator-chained version much harder to read...

nikomatsakis · 2017-05-31T00:58:06Z

src/ir/mod.rs

    pub trait_data: HashMap<ItemId, TraitDatum>,

-    /// For each trait:
+    /// For each trait (used for debugging):


Nit: should probably be "for each associated type" (pre-existing)

nikomatsakis · 2017-05-31T01:02:11Z

src/ir/mod.rs

@@ -91,22 +96,24 @@ impl Environment {
        Arc::new(env)
    }

-    pub fn elaborated_clauses(&self, program: &ProgramEnvironment) -> impl Iterator<Item = WhereClause> {
+    /// Generate the full set of clauses that are "syntactically implied" by the
+    /// clauses in this environment.


No good deed goes unpunished -- this comment could be improved by adding a few examples.

I'd write something like:

Generate the full set of clauses that are implied by the clauses in this environment. Currently this consists of two kinds of expansions:

Supertraits are added, so T: Ord would expand to {T: Ord, T: PartialOrd}

Associated type normalizations imply that the types are implemented, so T: Iterator<Item=Foo> expands to {T: Iterator, T: Iterator<Item=Foo>}.

Computes and returns the least-fixed-point of applying the above expansions.

nikomatsakis · 2017-05-31T01:02:42Z

src/ir/mod.rs

-pub enum WhereClause {
+/// A "domain goal" is a goal that is directly about Rust, rather than a pure
+/// logical statement. As much as possible, the Chalk solver should avoid
+/// decomposing this enum, and instead treat its values opaquely.


Nit: I prefer to put the comments above the #[derive] line -- is this something that just I do?

nikomatsakis · 2017-05-31T01:06:02Z

src/ir/mod.rs

 pub enum Constraint {
    LifetimeEq(Lifetime, Lifetime),
 }

+/// A mapping of inference variables to instantiations thereof.
+// Uses BTreeMap for extracting in order (mostly for debugging/testing)


Nit: was this supposed to be ///?

nikomatsakis · 2017-05-31T08:34:16Z

src/solve/fulfill.rs

+            let goal = canonicalized.quantified.value;
+
+            // Negation cannot be used to resolve existential variables, and do
+            // not have a useful (for us) logial meaning when they contain


Nit: s/logial/logical/

nikomatsakis · 2017-05-31T08:34:36Z

src/solve/fulfill.rs

+                return Ok(Outcome::Incomplete);
+            }
+
+


Nit: extra blank line

nikomatsakis · 2017-05-31T08:36:28Z

src/solve/fulfill.rs

+            // as ambiguous
+            if !canonicalized.free_vars.is_empty() {
+                return Ok(Outcome::Incomplete);
+            }


This is stronger than necessary, right? For example, imagine Vec<?T>: Copy -- given that there are no impls of Copy for Vec at all, and assuming a closed world, we could figure out that this is false. In particular, if we get a Unique result with an empty substitution, we are satisfied, even if free_vars is non-empty...?

nikomatsakis · 2017-05-31T08:37:52Z

src/solve/fulfill.rs

-                Ok(Solution::Ambig(Guidance::Definite(subst.quantified)))
+        // Next we look at the goals we must refute; doing so cannot create new
+        // obligations of any form
+        let negative = self.fulfill_negative()?;


Clever to stratify these like that, though probably not the most performant thing ever (i.e., we might have been able to see that we will fail to refute a "refute goal" and hence abort the process much earlier).

nikomatsakis · 2017-05-31T08:44:37Z

src/lower/mod.rs

+        //
+        // we generate:
+        //
+        //    ?T: SomeTrait<Assoc = (SomeTrait::Assoc)<?T>> :-


question -- currently, for each type Foo = Bar in an impl or the where-clause list, we generate two clauses:

<T as Trait>::Foo ==> Bar

and

known { <T as Trait>::Foo ==> Bar }

Maybe we should just translate the impl declarations along with T: Trait<Foo=Bar> where-clauses into the "known" form to start, and then, for each declaration in the trait, have two instances of the "general rule":

<?T as Trait>::Foo ==> Bar :- known { <?T as Trait>::Foo ==> Bar } <?T as Trait>::Foo ==> <?T as Trait>::Foo :- not { known { <?T as Trait>::Foo ==> Bar } }

Obviously, this is equivalent. Just seems a bit clearer to me somehow.

nikomatsakis · 2017-05-31T08:52:16Z

src/solve/fulfill.rs

+            // existential variables; treat negative goals with free variables
+            // as ambiguous
+            if !canonicalized.free_vars.is_empty() {
+                return Ok(Outcome::Incomplete);


Question: This is stronger than necessary, right? It seems like any result of Unique with an empty substitution is probably good enough. Consider something like not { Vec<?T>: Copy }... we know that it is false (given closed-world, at least), simply because there are no impls of Copy at all that could apply.

(I made this comment earlier, in my review, but GH marked it as "outdated" for some reason.)

nikomatsakis · 2017-05-31T08:53:28Z

src/solve/fulfill.rs

+            // go one last time through the positive obligations, this time
+            // applying even *tentative* inference suggestions, so that we can
+            // yield these upwards as our own suggestions. In particular, we
+            // yield up the first one we can find.


Question: First in what sense? we're popping the obligations, after all, so this isn't the first we would have encountered had we been applying the substs "in order", right? (Or am I missing something?)

(I made this comment earlier, in my review, but GH marked it as "outdated" for some reason.)

nikomatsakis · 2017-05-31T08:54:39Z

src/solve/fulfill.rs

+
+            Ok(Solution::Ambig(Guidance::Unknown))
+        } else {
+            // While we failed to prove the goal, we still leared that


Typo: s/leared/learned/

(I made this comment earlier, in my review, but GH marked it as "outdated" for some reason.)

nikomatsakis · 2017-05-31T08:55:41Z

I expect it to be stable, unless @nikomatsakis has a very surprising reaction to it :-)

Closing with prejudic--- oh, no, I guess it's fine.

scalexm · 2017-05-31T16:06:43Z

Actually I think I've found a regression. Load this Chalk program:

struct Foo { }

trait Marker { }
impl Marker for Foo { }

and then try to solve the goal

forall<T> { if (T: Marker) { T: Marker } }

current master branch answers: Solution { successful: Yes ...
while aturon's maybe-subst branch answers: Ambiguous; suggested substitution []

If you remove impl Marker for Foo { } then everything works fine.

In fact, aturon's branch will see the two rules !1: Marker and Foo: Marker into the environment, and it will try to unify the goal !1: Marker against these two rules and end up unifying !1 both as !1 and Foo. But I guess it should not unify !1 as Foo since it is a ! variable.

This bug is not caught by the prove_forall test because in this test, impl Marker for Foo { } is replaced by impl<T> Marker for Vec<T> { } and then the unification !1 as Vec<?0> cannot be done, so the issue does not appear.

aturon · 2017-05-31T17:43:03Z

OK, I've pushed up a couple of commits addressing @nikomatsakis's feedback. In particular, I added some commentary trying to explain in greater depth why we don't want to allow negations over free variables. Note also that this follows the original paper on negation as failure.

Also, I've collapsed the "clever" stratification of negative and positive goals. I think this new version is nicer.

@scalexm, I'll look at the issue you raised next.

aturon · 2017-05-31T17:58:30Z

@scalexm OK, I've investigated, and believe this comes down to the imprecision discussed in this comment about combining solutions. I don't see any harm in tightening that up, but am out of time for the moment.

nikomatsakis · 2017-05-31T19:27:25Z

@aturon

In particular, I added some commentary trying to explain in greater depth why we don't want to allow negations over free variables.

Thanks, that comment made sense, but I still think we could be yet more precise (not a blocker by any means, though). In your example:

struct Vec<T> {}
struct i32 {}
struct u32 {}
trait Foo {}
impl Foo for Vec<u32> {}

Given the query exists<T> { not { Vec<T>: Foo } }, I would expect a response of "ambiguous" or "maybe" or whatever your branch is calling it. In particular, we would try to solve Vec<?T>: Foo and we would get back a result that is Unique(?T = u32). Since the resulting substitution is non-trivial (what I called non-empty before), we would return Ok(NegativeSolution::Ambiguous).

Anyway, seems fine as is.

OK, I've investigated, and believe this comes down to the imprecision discussed in this comment about combining solutions. I don't see any harm in tightening that up, but am out of time for the moment.

yeah, I agree with this diagnosis.

nikomatsakis · 2017-05-31T19:28:47Z

Test failure:

failures:

---- solve::test::mixed_indices_normalize_application stdout ----
	program { struct Ref < 'a , T > {  } trait Foo { type T ; } }
----------------------------------------------------------------------
goal {
exists < T > {
exists < 'a > { exists < U > { < Ref < 'a , T > as Foo > :: T = U } } } }
expected:
Unique
actual:
Ambiguous; definite substitution [?0 := ?0, ?1 := (Foo::T)<Ref<'?1, ?0>>, '?0 := '?1]
thread 'solve::test::mixed_indices_normalize_application' panicked at 'assertion failed: !expected1.is_empty() && result1.starts_with(&expected1)', src/solve/test.rs:57
note: Run with `RUST_BACKTRACE=1` for a backtrace.


failures:
    solve::test::mixed_indices_normalize_application

nikomatsakis · 2017-05-31T21:11:01Z

On IRC, @scalexm and I were saying that maybe they will investigate this regression that they found. I also pointed them at this particular snippet of code, which I think may be the bit of logic that @aturon's branch doesn't have. (But I could be wrong.)

aturon · 2017-05-31T22:58:06Z

@nikomatsakis

Since the resulting substitution is non-trivial (what I called non-empty before), we would return Ok(NegativeSolution::Ambiguous).

Yeah, the confusion seemed to be around the precise conditions under which we'd go to ambiguous. But I agree we can punt this in any case.

aturon · 2017-05-31T22:59:18Z

On IRC, @scalexm and I were saying that maybe they will investigate this regression that they found. I also pointed them at this particular snippet of code, which I think may be the bit of logic that @aturon's branch doesn't have. (But I could be wrong.)

It's possible -- there are probably a few ways to deal with this. As much as possible, though, I'd like to push this kind of thing into the general logic for combining solutions.

nikomatsakis · 2017-06-01T01:11:24Z

As much as possible, though, I'd like to push this kind of thing into the general logic for combining solutions.

I agree that seems like the right place, didn't mean to suggest otherwise.

aturon commented May 27, 2017

View reviewed changes

aturon force-pushed the maybe-subst branch from 77a3a7a to 748d596 Compare May 27, 2017 02:39

aturon changed the title ~~Use substitutions and suggestions in Solution~~ Use substitutions and suggestions in Solution; implement negation (WIP) May 28, 2017

aturon mentioned this pull request May 30, 2017

Merge WhereClause and WhereClauseGoal into a single enum #37

Closed

aturon changed the title ~~Use substitutions and suggestions in Solution; implement negation (WIP)~~ Use substitutions and suggestions in Solution; implement negation May 30, 2017

aturon added 4 commits May 30, 2017 17:49

Introduce negation

8158847

Introduce `not { ... }` as a logical operator, using negation-as-failure semantics adjusted for our "three-valued" logic. WIP; currently doesn't handle `forall` correctly for unification.

Treat unification with unequal skolemized type variables as ambiguous…

05bdfce

…, thereby correcting the semantics with respect to negation

aturon force-pushed the maybe-subst branch from 23f4277 to 3bd7bf4 Compare May 31, 2017 00:49

nikomatsakis requested changes May 31, 2017

View reviewed changes

nikomatsakis reviewed May 31, 2017

View reviewed changes

aturon added 2 commits May 31, 2017 10:39

Address most review nits and questions

1444a69

Revamp normalization fallback to follow Niko's review suggestion

f79f6dd

nikomatsakis approved these changes May 31, 2017

View reviewed changes

Test fixup

d3e941e

aturon force-pushed the maybe-subst branch from b25510b to d3e941e Compare May 31, 2017 23:00

nikomatsakis merged commit eac7a6c into rust-lang:master Jun 1, 2017

Use substitutions and suggestions in Solution; implement negation #36

Use substitutions and suggestions in Solution; implement negation #36

Conversation

aturon commented May 27, 2017 • edited Loading

aturon commented May 27, 2017

Choose a reason for hiding this comment

aturon commented May 28, 2017

aturon commented May 30, 2017

aturon commented May 31, 2017

aturon commented May 31, 2017

withoutboats commented May 31, 2017

aturon commented May 31, 2017

nikomatsakis left a comment

Choose a reason for hiding this comment

nikomatsakis May 31, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis May 31, 2017 • edited Loading

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

nikomatsakis May 31, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented May 31, 2017

scalexm commented May 31, 2017

aturon commented May 31, 2017

aturon commented May 31, 2017

nikomatsakis commented May 31, 2017

nikomatsakis commented May 31, 2017

nikomatsakis commented May 31, 2017

aturon commented May 31, 2017

aturon commented May 31, 2017

nikomatsakis commented Jun 1, 2017

aturon commented May 27, 2017 •

edited

Loading

nikomatsakis May 31, 2017 •

edited

Loading

nikomatsakis May 31, 2017 •

edited

Loading

nikomatsakis May 31, 2017 •

edited

Loading