[WIP] Convert from semantic to syntactic equality

chalk-engine/src/logic.rs

@@ -1571,9 +1571,14 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
     /// would be true, since `Send` is an auto trait, which yields a
     /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is
     /// false, since `XXX` is not an auto trait.
+    #[instrument(level = "debug", skip(self))]
     pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool {
         StackIndex::iterate_range(self.stack.top_of_stack_from(depth)).all(|d| {
             let table = self.stack[d].table;
+            debug!(
+                "d = {:?}, table = {:?}",
+                d, self.forest.tables[table].table_goal
+            );
             self.forest.tables[table].coinductive_goal
         })
     }

chalk-solve/src/clauses.rs

@@ -18,6 +18,7 @@ mod dyn_ty;
 mod env_elaborator;
 mod generalize;
 pub mod program_clauses;
+pub mod syntactic_eq;
 
 // yields the types "contained" in `app_ty`
 fn constituent_types<I: Interner>(db: &dyn RustIrDatabase<I>, ty: &TyKind<I>) -> Vec<Ty<I>> {
@@ -526,11 +527,19 @@ fn program_clauses_that_could_match<I: Interner>(
                 })
             });
         }
-        DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
-        | DomainGoal::LocalImplAllowed(trait_ref) => {
+        DomainGoal::LocalImplAllowed(trait_ref) => {
             db.trait_datum(trait_ref.trait_id)
                 .to_program_clauses(builder, environment);
         }
+
+        DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => {
+            let self_ty = trait_predicate.self_type_parameter(interner);
+            if self_ty.bound_var(interner).is_some() || self_ty.inference_var(interner).is_some() {
+                return Err(Floundered);
+            }
+            db.trait_datum(trait_predicate.trait_id)
+                .to_program_clauses(builder, environment);
+        }
         DomainGoal::ObjectSafe(trait_id) => {
             if builder.db.is_object_safe(*trait_id) {
                 builder.push_fact(DomainGoal::ObjectSafe(*trait_id));

chalk-solve/src/clauses/builder.rs

@@ -1,6 +1,7 @@
 use std::marker::PhantomData;
 
 use crate::cast::{Cast, CastTo};
+use crate::clauses::syntactic_eq::syn_eq_lower;
 use crate::RustIrDatabase;
 use chalk_ir::fold::{Fold, Shift};
 use chalk_ir::interner::{HasInterner, Interner};
@@ -95,14 +96,13 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
         } else {
             clause
         };
+        let clause = ProgramClauseData(Binders::new(
+            VariableKinds::from_iter(interner, self.binders.clone()),
+            clause,
+        ))
+        .intern(interner);
 
-        self.clauses.push(
-            ProgramClauseData(Binders::new(
-                VariableKinds::from_iter(interner, self.binders.clone()),
-                clause,
-            ))
-            .intern(interner),
-        );
+        self.clauses.push(syn_eq_lower(interner, &clause));
 
         debug!("pushed clause {:?}", self.clauses.last());
     }

chalk-solve/src/clauses/syntactic_eq.rs

@@ -0,0 +1,202 @@
+use std::{iter, mem::take};
+
+use chalk_ir::{
+    cast::Cast,
+    fold::{shift::Shift, Fold, Folder, SuperFold},
+    interner::Interner,
+    AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals,
+    ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyKind,
+    TyVariableKind, VariableKind, VariableKinds,
+};
+
+/// Converts a set of clauses to require only syntactic equality.
+/// This is done by introducing new parameters and subgoals in cases
+/// where semantic equality may diverge, for instance in unnormalized projections.
+pub fn syn_eq_lower<I: Interner, T: Fold<I>>(interner: &I, clause: &T) -> <T as Fold<I>>::Result {
+    let mut folder = SynEqFolder {
+        interner,
+        new_params: vec![],
+        new_goals: vec![],
+        binders_len: 0,
+    };
+
+    clause
+        .fold_with(&mut folder, DebruijnIndex::INNERMOST)
+        .unwrap()
+}
+
+struct SynEqFolder<'i, I: Interner> {
+    interner: &'i I,
+    /// Stores the kinds of new parameters introduced during folding.
+    /// The new parameters will either be added to an enclosing `exists` binder (when lowering a goal)
+    /// or to an enclosing `forall` binder (when lowering a program clause).
+    new_params: Vec<VariableKind<I>>,
+    /// For each new parameter `X`, a new goal is introduced to define it, e.g. `EqGoal(<T as Iterator>::Item, X)
+    new_goals: Vec<Goal<I>>,
+
+    /// Stores the current number of variables in the binder we are adding parameters to.
+    /// Incremented for each new variable added.
+    binders_len: usize,
+}
+
+impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
+    fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
+        self
+    }
+
+    fn fold_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> Fallible<Ty<I>> {
+        let interner = self.interner;
+        let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.binders_len);
+
+        let new_ty = TyKind::BoundVar(bound_var).intern(interner);
+        match ty.kind(interner) {
+            TyKind::Alias(AliasTy::Projection(_)) | TyKind::Function(_) => {
+                self.new_params
+                    .push(VariableKind::Ty(TyVariableKind::General));
+                self.new_goals.push(
+                    EqGoal {
+                        a: new_ty.clone().cast(interner),
+                        b: ty.clone().cast(interner),
+                    }
+                    .cast(interner),
+                );
+                self.binders_len += 1;
+                Ok(new_ty)
+            }
+            _ => ty.super_fold_with(self, outer_binder),
+        }
+    }
+
+    /// Convert a program clause to rem
+    ///
+    /// Consider this (nonsense) example:
+    ///
+    /// ```notrust
+    /// forall<X> {
+    ///     Implemented(<X as Iterator>::Item>: Debug) :-
+    ///         Implemented(X: Debug)
+    /// }
+    /// ```
+    ///
+    /// we would lower this into:
+    ///
+    /// ```notrust
+    /// forall<X, Y> {
+    ///     Implemented(Y: Debug) :-
+    ///         EqGoal(<X as Iterator>::Item>, Y),
+    ///         Implemented(X: Debug)
+    /// }
+    /// ```
+    fn fold_program_clause(
+        &mut self,
+        clause: &ProgramClause<I>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<ProgramClause<I>> {
+        let interner = self.interner;
+        assert!(self.new_params.is_empty());
+        assert!(self.new_goals.is_empty());
+
+        let ProgramClauseData(binders) = clause.data(interner);
+
+        let implication = binders.skip_binders();
+        let mut binders: Vec<_> = binders.binders.as_slice(interner).into();
+
+        // Adjust the outer binder to account for the binder in the program clause
+        let outer_binder = outer_binder.shifted_in();
+
+        // Set binders_len to binders.len() since new parameters will be added into the existing forall<...> binder on the program clause.
+        self.binders_len = binders.len();
+
+        // First lower the "consequence" -- in our example that is
+        //
+        // ```
+        // Implemented(<X as Iterator>::Item: Debug)
+        // ```
+        //
+        // then save out the `new_params` and `new_goals` vectors to store any new variables created as a result.
+        // In this case, that would be the `Y` parameter and `EqGoal(<X as Iterator>::Item, Y)` goals.
+        //
+        // Note that these new parameters will have indices that come after the existing parameters,
+        // so any references to existing parameters like `X` in the "conditions" are still valid even if we insert new parameters.
+        let consequence = implication.consequence.fold_with(self, outer_binder)?;
+
+        let mut new_params = take(&mut self.new_params);
+        let mut new_goals = take(&mut self.new_goals);
+
+        // Now fold the conditions (in our example, Implemented(X: Debug).
+        // The resulting list might be expanded to include new EqGoal goals.
+        let mut conditions = implication.conditions.fold_with(self, outer_binder)?;
+
+        new_params.extend(take(&mut self.new_params));
+        new_goals.extend(take(&mut self.new_goals));
+
+        let constraints = implication.constraints.fold_with(self, outer_binder)?;
+
+        new_params.extend(take(&mut self.new_params));
+        new_goals.extend(take(&mut self.new_goals));
+
+        binders.extend(new_params.into_iter());
+
+        conditions = Goals::from_iter(
+            interner,
+            conditions.iter(interner).cloned().chain(new_goals),
+        );
+
+        Ok(ProgramClauseData(Binders::new(
+            VariableKinds::from_iter(interner, binders),
+            ProgramClauseImplication {
+                consequence,
+                conditions,
+                constraints,
+                priority: implication.priority,
+            },
+        ))
+        .intern(interner))
+    }
+
+    fn fold_goal(&mut self, goal: &Goal<I>, outer_binder: DebruijnIndex) -> Fallible<Goal<I>> {
+        assert!(self.new_params.is_empty());
+        assert!(self.new_goals.is_empty());
+
+        let interner = self.interner;
+        match goal.data(interner) {
+            GoalData::DomainGoal(_) | GoalData::EqGoal(_) => (),
+            _ => return goal.super_fold_with(self, outer_binder),
+        };
+
+        // Set binders_len to zero as in the exists<..> binder we will create, there are no existing variables.
+        self.binders_len = 0;
+
+        // shifted in because we introduce a new binder
+        let outer_binder = outer_binder.shifted_in();
+        let syn_goal = goal
+            .shifted_in(interner)
+            .super_fold_with(self, outer_binder)?;
+        let new_params = take(&mut self.new_params);
+        let new_goals = take(&mut self.new_goals);
+
+        if new_params.is_empty() {
+            return Ok(goal.clone());
+        }
+
+        let goal = GoalData::All(Goals::from_iter(
+            interner,
+            iter::once(syn_goal).into_iter().chain(new_goals),
+        ))
+        .intern(interner);
+
+        Ok(GoalData::Quantified(
+            QuantifierKind::Exists,
+            Binders::new(VariableKinds::from_iter(interner, new_params), goal),
+        )
+        .intern(interner))
+    }
+
+    fn interner(&self) -> &'i I {
+        self.interner
+    }
+
+    fn target_interner(&self) -> &'i I {
+        self.interner
+    }
+}

chalk-solve/src/coinductive_goal.rs

@@ -15,6 +15,18 @@ pub trait IsCoinductive<I: Interner> {
 }
 
 impl<I: Interner> IsCoinductive<I> for Goal<I> {
+    /// A "coinductive" goal `G` is a goal where `G :- G` should be considered
+    /// true. When we are doing trait solving, if we encounter a cycle of goals
+    /// where solving `G1` requires `G2..Gn` and solving `Gn` requires `G1`,
+    /// then our behavior depends on whether each goal `Gi` in that cycle is
+    /// coinductive.
+    ///
+    /// If all the goals are coinductive, then `G1` is considered provable,
+    /// presuming that all the other subgoals for `G2..Gn` within can be fully
+    /// proven.
+    ///
+    /// If any goal `Gi` in the cycle is inductive, however, then the cycle is
+    /// considered unprovable.
     fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
         let interner = db.interner();
         match self.data(interner) {
@@ -28,10 +40,33 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
                 WhereClause::TypeOutlives(..) => false,
             },
             GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
-            GoalData::Quantified(QuantifierKind::ForAll, goal) => {
-                goal.skip_binders().is_coinductive(db)
-            }
-            _ => false,
+            GoalData::DomainGoal(_) => false,
+
+            // Goals like `forall<..> { G }` or `... => G` we will consider to
+            // be coinductive if G is coinductive, although in practice I think
+            // it would be ok to simply consider them coinductive all the time.
+            GoalData::Quantified(_, goal) => goal.skip_binders().is_coinductive(db),
+            GoalData::Implies(_, goal) => goal.is_coinductive(db),
+
+            // The "All(...)" quantifier is considered coinductive. This could
+            // be somewhat surprising as you might have `All(Gc, Gi)` where `Gc`
+            // is coinductive and `Gi` is inductive. This however is really no
+            // different than defining a fresh coinductive goal like
+            //
+            // ```notrust
+            // Gx :- Gc, Gi
+            // ```
+            //
+            // and requiring `Gx` in place of `All(Gc, Gi)`, and that would be
+            // perfectly reasonable.
+            GoalData::All(..) => true,
+
+            // For simplicity, just assume these remaining types of goals must
+            // be inductive, since there is no pressing reason to consider them
+            // coinductive.
+            GoalData::Not(_) => false,
+            GoalData::EqGoal(_) => false,
+            GoalData::CannotProve => false,
         }
     }
 }

chalk-solve/src/ext.rs

@@ -1,3 +1,4 @@
+use crate::clauses::syntactic_eq::syn_eq_lower;
 use crate::infer::InferenceTable;
 use chalk_ir::fold::Fold;
 use chalk_ir::interner::{HasInterner, Interner};
@@ -89,7 +90,9 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
                 }
             }
         };
-        let canonical = infer.canonicalize(interner, &peeled_goal).quantified;
+        let canonical = infer
+            .canonicalize(interner, &syn_eq_lower(interner, &peeled_goal))
+            .quantified;
         infer.u_canonicalize(interner, &canonical).quantified
     }
 
@@ -104,7 +107,8 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
     /// Will panic if this goal does in fact contain free variables.
     fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
         let mut infer = InferenceTable::new();
-        let env_goal = InEnvironment::new(&Environment::new(interner), self);
+        let lowered_goal = syn_eq_lower(interner, &self);
+        let env_goal = InEnvironment::new(&Environment::new(interner), &lowered_goal);
         let canonical_goal = infer.canonicalize(interner, &env_goal).quantified;
         infer.u_canonicalize(interner, &canonical_goal).quantified
     }

tests/test/projection.rs

@@ -968,19 +968,6 @@ fn rust_analyzer_regression() {
             }
         }
 
-        //fn try_reduce_with<PI, R, T>(pi: PI, reduce_op: R) -> Option<T>
-        //    where
-        //        PI: ParallelIterator<Item = T>,
-        //        R: FnOnce(T::Ok) -> T,
-        //        T: Try,
-        //    {
-        //        pi.drive_unindexed()
-        //    }
-        //
-        // where `drive_unindexed` is a method in `ParallelIterator`:
-        //
-        // fn drive_unindexed(self) -> ();
-
         goal {
             forall<PI, R, T> {
                 if (
@@ -991,8 +978,8 @@ fn rust_analyzer_regression() {
                     PI: ParallelIterator
                 }
             }
-        } yields_first[SolverChoice::slg(4, None)] {
-            "Floundered"
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
         }
     }
 }