WIP

chalk-parse/src/ast.rs

@@ -165,6 +165,7 @@ pub enum Goal {
     Implies(Vec<WhereClause>, Box<Goal>),
     And(Box<Goal>, Box<Goal>),
     Not(Box<Goal>),
+    StrongNot(Box<Goal>),
 
     // Additional kinds of goals:
     Leaf(WhereClause),

chalk-parse/src/parser.lalrpop

@@ -30,6 +30,7 @@ Goal1: Box<Goal> = {
     "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
     "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
+    "strong not" "{" <g:Goal> "}" => Box::new(Goal::StrongNot(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
 };
 

src/fold/mod.rs

@@ -200,7 +200,7 @@ enum_fold!(DomainGoal[] { Implemented(a), RawNormalize(a), Normalize(a), WellFor
 enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
 enum_fold!(LeafGoal[] { EqGoal(a), DomainGoal(a) });
 enum_fold!(Constraint[] { LifetimeEq(a, b) });
-enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), Leaf(wc) });
+enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g), StrongNot(g), Leaf(wc) });
 
 macro_rules! struct_fold {
     ($s:ident $([$($n:ident),*])* { $($name:ident),* } $($w:tt)*) => {

src/ir/debug.rs

@@ -206,6 +206,7 @@ impl Debug for Goal {
             Goal::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
             Goal::And(ref g1, ref g2) => write!(fmt, "({:?}, {:?})", g1, g2),
             Goal::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
+            Goal::StrongNot(ref g) => write!(fmt, "strong not {{ {:?} }}", g),
             Goal::Leaf(ref wc) => write!(fmt, "{:?}", wc),
         }
     }

src/ir/mod.rs

@@ -539,6 +539,7 @@ pub enum Goal {
     Implies(Vec<DomainGoal>, Box<Goal>),
     And(Box<Goal>, Box<Goal>),
     Not(Box<Goal>),
+    StrongNot(Box<Goal>),
     Leaf(LeafGoal),
 }
 
@@ -592,6 +593,10 @@ impl Substitution {
 
         Substitution { tys, lifetimes }
     }
+
+    pub fn is_empty(&self) -> bool {
+        self.tys.is_empty() && self.lifetimes.is_empty()
+    }
 }
 
 #[derive(Clone, Debug, PartialEq, Eq)]

src/lower/mod.rs

@@ -736,6 +736,8 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))),
             Goal::Not(ref g) =>
                 Ok(Box::new(ir::Goal::Not(g.lower(env)?))),
+            Goal::StrongNot(ref g) =>
+                Ok(Box::new(ir::Goal::StrongNot(g.lower(env)?))),
             Goal::Leaf(ref wc) =>
                 Ok(Box::new(ir::Goal::Leaf(wc.lower(env)?))),
         }
@@ -993,7 +995,7 @@ impl ir::AssociatedTyDatum {
         // we generate:
         //
         //    ?T: Foo<Assoc = ?U> :- ?T: Foo<Assoc =raw ?U>.
-        //    ?T: Foo<Assoc = (Foo::Assoc)<?T>> :- not { exists<U> { ?T: Foo<Assoc =raw U> } }.
+        //    ?T: Foo<Assoc = (Foo::Assoc)<?T>> :- strong not { exists<U> { ?T: Foo<Assoc =raw U> } }.
 
         let binders: Vec<_> = self.parameter_kinds.iter().map(|pk| pk.map(|_| ())).collect();
         let parameters: Vec<_> = binders.iter().zip(0..).map(|p| p.to_parameter()).collect();
@@ -1042,7 +1044,7 @@ impl ir::AssociatedTyDatum {
                     binders,
                     value: ir::ProgramClauseImplication {
                         consequence: ir::Normalize { projection: projection.clone(), ty }.cast(),
-                        conditions: vec![ir::Goal::Not(Box::new(exists))]
+                        conditions: vec![ir::Goal::StrongNot(Box::new(exists))]
                     }
                 }
             }

src/solve/fulfill.rs

@@ -23,6 +23,11 @@ impl Outcome {
     }
 }
 
+pub struct UnifyOutcome {
+    pub ambiguous_left: bool,
+    pub ambiguous_right: bool,
+}
+
 /// A goal that must be resolved
 #[derive(Clone, Debug, PartialEq, Eq)]
 enum Obligation {
@@ -33,7 +38,14 @@ enum Obligation {
     /// For "negative" goals, we don't flatten in *this* `Fulfill`, which would
     /// require having a logical "or" operator. Instead, we recursively solve in
     /// a fresh `Fulfill`.
-    Refute(InEnvironment<Goal>),
+    ///
+    /// A "weak" refutation is true negation: if the subgoal is ambiguous, so is
+    /// its refutation.
+    RefuteWeak(InEnvironment<Goal>),
+
+    /// A "strong" refutation is sensitive to the proof system: it succeeds only
+    /// when the subgoal definitely fails, and it fails otherwise.
+    RefuteStrong(InEnvironment<Goal>),
 }
 
 /// When proving a leaf goal, we record the free variables that appear within it
@@ -115,19 +127,20 @@ impl<'s> Fulfill<'s> {
     ///
     /// Wraps `InferenceTable::unify`; any resulting normalizations are added
     /// into our list of pending obligations with the given environment.
-    pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<()>
+    pub fn unify<T>(&mut self, environment: &Arc<Environment>, a: &T, b: &T) -> Result<UnifyOutcome>
         where T: ?Sized + Zip + Debug
     {
-        let UnificationResult { goals, constraints, ambiguous } =
+        let UnificationResult { goals, constraints, ambiguous_left, ambiguous_right } =
             self.infer.unify(environment, a, b)?;
         debug!("unify({:?}, {:?}) succeeded", a, b);
         debug!("unify: goals={:?}", goals);
         debug!("unify: constraints={:?}", constraints);
-        debug!("unify: ambiguous={:?}", ambiguous);
+        debug!("unify: ambiguous left={:?}, right={:?}", ambiguous_left, ambiguous_right);
         self.constraints.extend(constraints);
         self.obligations.extend(goals.into_iter().map(Obligation::Prove));
-        self.ambiguous = self.ambiguous || ambiguous;
-        Ok(())
+        self.ambiguous = self.ambiguous || ambiguous_left || ambiguous_right;
+
+        Ok(UnifyOutcome { ambiguous_left, ambiguous_right })
     }
 
     /// Create obligations for the given goal in the given environment. This may
@@ -173,7 +186,12 @@ impl<'s> Fulfill<'s> {
                 self.push_goal(environment, *subgoal2);
             }
             Goal::Not(subgoal) => {
-                self.obligations.push(Obligation::Refute(InEnvironment::new(environment, *subgoal)));
+                let in_env = InEnvironment::new(environment, *subgoal);
+                self.obligations.push(Obligation::RefuteWeak(in_env));
+            }
+            Goal::StrongNot(subgoal) => {
+                let in_env = InEnvironment::new(environment, *subgoal);
+                self.obligations.push(Obligation::RefuteStrong(in_env));
             }
             Goal::Leaf(wc) => {
                 self.obligations.push(Obligation::Prove(InEnvironment::new(environment, wc)));
@@ -190,7 +208,7 @@ impl<'s> Fulfill<'s> {
         })
     }
 
-    fn refute(&mut self, goal: &InEnvironment<Goal>) -> Result<NegativeSolution> {
+    fn refute(&mut self, strong: bool, goal: &InEnvironment<Goal>) -> Result<NegativeSolution> {
         let canonicalized = self.infer.canonicalize(goal);
 
         // Following the original negation-as-failure semantics, we refuse to
@@ -219,6 +237,8 @@ impl<'s> Fulfill<'s> {
 
         // Negate the result
         if let Ok(solution) =  self.solver.solve_goal(canonicalized.quantified) {
+            if strong { Err("strong refutation failed")? }
+
             match solution {
                 Solution::Unique(_) => Err("refutation failed")?,
                 Solution::Ambig(_) => Ok(NegativeSolution::Ambiguous),
@@ -309,8 +329,11 @@ impl<'s> Fulfill<'s> {
 
                         solution.is_ambig()
                     }
-                    Obligation::Refute(ref goal) => {
-                        self.refute(goal)? == NegativeSolution::Ambiguous
+                    Obligation::RefuteWeak(ref goal) => {
+                        self.refute(false, goal)? == NegativeSolution::Ambiguous
+                    }
+                    Obligation::RefuteStrong(ref goal) => {
+                        self.refute(true, goal)? == NegativeSolution::Ambiguous
                     }
                 };
 

src/solve/infer/unify.rs

@@ -34,7 +34,8 @@ struct Unifier<'t> {
     snapshot: InferenceSnapshot,
     goals: Vec<InEnvironment<LeafGoal>>,
     constraints: Vec<InEnvironment<Constraint>>,
-    ambiguous: bool,
+    ambiguous_left: bool,
+    ambiguous_right: bool,
 }
 
 #[derive(Debug)]
@@ -44,8 +45,10 @@ pub struct UnificationResult {
 
     /// When unifying two skolemized (forall-quantified) type names, we can
     /// neither confirm nor deny their equality, so we return an ambiguous
-    /// result.
-    pub ambiguous: bool,
+    /// result. The `left` vs `right` says which side(s) such a skolemized
+    /// variable appeared on.
+    pub ambiguous_left: bool,
+    pub ambiguous_right: bool,
 }
 
 impl<'t> Unifier<'t> {
@@ -57,7 +60,8 @@ impl<'t> Unifier<'t> {
             snapshot: snapshot,
             goals: vec![],
             constraints: vec![],
-            ambiguous: false,
+            ambiguous_left: false,
+            ambiguous_right: false,
         }
     }
 
@@ -66,7 +70,8 @@ impl<'t> Unifier<'t> {
         Ok(UnificationResult {
             goals: self.goals,
             constraints: self.constraints,
-            ambiguous: self.ambiguous,
+            ambiguous_left: self.ambiguous_left,
+            ambiguous_right: self.ambiguous_right,
         })
     }
 
@@ -115,8 +120,9 @@ impl<'t> Unifier<'t> {
             (&Ty::Apply(ref apply1), &Ty::Apply(ref apply2)) => {
                 if apply1.name != apply2.name {
                     if apply1.name.is_for_all() || apply2.name.is_for_all() {
-                        self.ambiguous = true;
-                        return Ok(());
+                        if apply1.name.is_for_all() { self.ambiguous_left = true }
+                        if apply2.name.is_for_all() { self.ambiguous_right = true }
+                        return Ok(())
                     } else {
                         bail!("cannot equate `{:?}` and `{:?}`", apply1.name, apply2.name);
                     }

src/solve/mod.rs

@@ -66,8 +66,10 @@ impl Solution {
         use self::Guidance::*;
 
         if self == other { return self }
+        if self.is_empty_unique() { return self }
+        if other.is_empty_unique() { return other }
 
-        // unless we have two matching Unique solutions, we always downgrade to Ambig:
+        // Otherwise, always downgrade to Ambig:
 
         let guidance = match (self.into_guidance(), other.into_guidance()) {
             (Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 =>
@@ -91,8 +93,10 @@ impl Solution {
         use self::Guidance::*;
 
         if self == other { return self }
+        if self.is_empty_unique() { return self }
+        if other.is_empty_unique() { return other }
 
-        // unless we have two matching Unique solutions, we always downgrade to Ambig:
+        // Otherwise, always downgrade to Ambig:
 
         let guidance = match (self.into_guidance(), other.into_guidance()) {
             (Definite(subst), _) | (Suggested(subst), _) => Suggested(subst),
@@ -146,6 +150,15 @@ impl Solution {
             _ => false,
         }
     }
+
+    pub fn is_empty_unique(&self) -> bool {
+        match *self {
+            Solution::Unique(ref subst) => {
+                subst.binders.is_empty() && subst.value.subst.is_empty()
+            }
+            _ => false,
+        }
+    }
 }
 
 impl fmt::Display for Solution {

src/solve/solver.rs

@@ -187,7 +187,9 @@ impl Solver {
             fulfill.instantiate_in(goal.environment.universe, clause.binders, &clause.value);
 
         // first, see if the implication's conclusion might solve our goal
-        fulfill.unify(&goal.environment, &goal.goal, &implication.consequence)?;
+        if fulfill.unify(&goal.environment, &goal.goal, &implication.consequence)?.ambiguous_right {
+            Err("using the implication would require changing a forall variable")?;
+        }
 
         // if so, toss in all of its premises
         for condition in implication.conditions {

src/solve/test.rs

@@ -145,7 +145,7 @@ fn prove_forall() {
         goal {
             forall<T> { T: Marker }
         } yields {
-            "No possible solution"
+            "Ambiguous; no inference guidance"
         }
 
         // If we assume `T: Marker`, then obviously `T: Marker`.
@@ -168,7 +168,7 @@ fn prove_forall() {
         goal {
             forall<T> { Vec<T>: Clone }
         } yields {
-            "No possible solution"
+            "Ambig"
         }
 
         // Here, we do know that `T: Clone`, so we can.
@@ -253,7 +253,7 @@ fn max_depth() {
 }
 
 #[test]
-fn normalize() {
+fn normalize_basic() {
     test! {
         program {
             trait Iterator { type Item; }
@@ -264,6 +264,7 @@ fn normalize() {
             }
         }
 
+        /*
         goal {
             forall<T> {
                 exists<U> {
@@ -291,17 +292,18 @@ fn normalize() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := u32], lifetime constraints []"
+            "Ambiguous; suggested substitution [?0 := u32]"
         }
+*/
 
         goal {
-            forall<T> {
-                if (T: Iterator) {
-                    exists<U> {
-                        T: Iterator<Item = U>
-                    }
-                }
-            }
+forall<T> {
+    if (T: Iterator) {
+        exists<U> {
+            T: Iterator<Item = U>
+        }
+    }
+}
         } yields {
             "Unique; substitution [?0 := (Iterator::Item)<!1>]"
         }