Semantic equality to syntactic equality

chalk-engine/src/logic.rs

@@ -1487,8 +1487,13 @@ impl<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> SolveState<'for
     /// coinductive goal. But `top_of_stack_is_coinductive_from(0)` is
     /// false, since `XXX` is not an auto trait.
     pub(super) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool {
+        debug_heading!("top_of_stack_is_coinductive_from(depth={:?})", depth);
         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

@@ -16,6 +16,7 @@ mod dyn_ty;
 mod env_elaborator;
 mod generalize;
 pub mod program_clauses;
+pub mod syntactic_eq;
 
 /// For auto-traits, we generate a default rule for every struct,
 /// unless there is a manual impl for that struct given explicitly.
@@ -242,9 +243,15 @@ fn program_clauses_that_could_match<I: Interner>(
                 .opaque_ty_data(opaque_ty.opaque_ty_id)
                 .to_program_clauses(builder),
         },
-        DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
-        | DomainGoal::LocalImplAllowed(trait_ref) => {
-            db.trait_datum(trait_ref.trait_id)
+        DomainGoal::LocalImplAllowed(trait_ref) => db
+            .trait_datum(trait_ref.trait_id)
+            .to_program_clauses(builder),
+        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);
         }
         DomainGoal::ObjectSafe(trait_id) => {

chalk-solve/src/clauses/builder.rs

@@ -2,6 +2,7 @@ use std::iter;
 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;
 use chalk_ir::interner::{HasInterner, Interner};
@@ -77,18 +78,17 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
             priority,
         };
 
-        if self.binders.len() == 0 {
-            self.clauses
-                .push(ProgramClauseData::Implies(clause).intern(interner));
+        let clause = if self.binders.len() == 0 {
+            ProgramClauseData::Implies(clause).intern(interner)
         } else {
-            self.clauses.push(
-                ProgramClauseData::ForAll(Binders::new(
-                    VariableKinds::from(interner, self.binders.clone()),
-                    clause,
-                ))
-                .intern(interner),
-            );
-        }
+            ProgramClauseData::ForAll(Binders::new(
+                VariableKinds::from(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/program_clauses.rs

@@ -856,6 +856,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
 
             // add new type parameter U
             builder.push_bound_ty(|builder, ty| {
+                let alias = AliasTy::Projection(projection.clone());
                 // `Normalize(<T as Foo>::Assoc -> U)`
                 let normalize = Normalize {
                     alias: AliasTy::Projection(projection.clone()),
@@ -864,8 +865,8 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
 
                 // `AliasEq(<T as Foo>::Assoc = U)`
                 let projection_eq = AliasEq {
-                    alias: AliasTy::Projection(projection),
-                    ty,
+                    alias: alias.clone(),
+                    ty: ty.clone(),
                 };
 
                 // Projection equality rule from above.
@@ -874,7 +875,7 @@ impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> {
                 //        AliasEq(<T as Foo>::Assoc = U) :-
                 //            Normalize(<T as Foo>::Assoc -> U).
                 //    }
-                builder.push_clause(projection_eq, Some(normalize));
+                builder.push_clause(projection_eq.clone(), Some(normalize));
             });
         });
     }

chalk-solve/src/clauses/syntactic_eq.rs

@@ -0,0 +1,165 @@
+use std::{iter, mem::replace};
+
+use chalk_engine::fallible::Fallible;
+use chalk_ir::{
+    cast::Cast,
+    fold::{shift::Shift, Fold, Folder, SuperFold},
+    interner::Interner,
+    AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, Goal, GoalData, Goals, ProgramClause,
+    ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, VariableKind,
+    VariableKinds,
+};
+
+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,
+    new_params: Vec<VariableKind<I>>,
+    new_goals: Vec<Goal<I>>,
+    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 = TyData::BoundVar(bound_var).intern(interner);
+        match ty.data(interner) {
+            TyData::Alias(alias @ AliasTy::Projection(_)) => {
+                self.new_params.push(VariableKind::Ty);
+                self.new_goals.push(
+                    AliasEq {
+                        alias: alias.clone(),
+                        ty: new_ty.clone(),
+                    }
+                    .cast(interner),
+                );
+                self.binders_len += 1;
+                ty.super_fold_with(self, outer_binder)?;
+                Ok(new_ty)
+            }
+            TyData::Function(_) => Ok(ty.clone()),
+            _ => Ok(ty.super_fold_with(self, outer_binder)?),
+        }
+    }
+
+    fn fold_program_clause(
+        &mut self,
+        clause: &ProgramClause<I>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<ProgramClause<I>> {
+        let interner = self.interner;
+
+        let ((binders, implication), in_binders) = match clause.data(interner) {
+            ProgramClauseData::ForAll(for_all) => (for_all.clone().into(), true),
+            // introduce a dummy binder and shift implication through it
+            ProgramClauseData::Implies(implication) => (
+                (
+                    VariableKinds::new(interner),
+                    implication.shifted_in(interner),
+                ),
+                false,
+            ),
+        };
+        let mut binders: Vec<_> = binders.as_slice(interner).clone().into();
+
+        let outer_binder = outer_binder.shifted_in();
+
+        self.binders_len = binders.len();
+        let consequence = implication.consequence.fold_with(self, outer_binder)?;
+        // Immediately move `new_params` out of of the folder struct so it's safe
+        // to call `.fold_with` again
+        let new_params = replace(&mut self.new_params, vec![]);
+        let new_goals = replace(&mut self.new_goals, vec![]);
+
+        let mut conditions = implication.conditions.fold_with(self, outer_binder)?;
+        if new_params.is_empty() && !in_binders {
+            // shift the clause out since we didn't use the dummy binder
+            return Ok(ProgramClauseData::Implies(
+                ProgramClauseImplication {
+                    consequence,
+                    conditions,
+                    priority: implication.priority,
+                }
+                .shifted_out(interner)?,
+            )
+            .intern(interner));
+        }
+
+        binders.extend(new_params.into_iter());
+
+        conditions = Goals::from(
+            interner,
+            conditions.iter(interner).cloned().chain(new_goals),
+        );
+
+        Ok(ProgramClauseData::ForAll(Binders::new(
+            VariableKinds::from(interner, binders),
+            ProgramClauseImplication {
+                consequence,
+                conditions,
+                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(), true);
+
+        let interner = self.interner;
+        match goal.data(interner) {
+            GoalData::DomainGoal(_) | GoalData::EqGoal(_) => (),
+            _ => return goal.super_fold_with(self, outer_binder),
+        };
+
+        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 = replace(&mut self.new_params, vec![]);
+        let new_goals = replace(&mut self.new_goals, vec![]);
+
+        if new_params.is_empty() {
+            return Ok(goal.clone());
+        }
+
+        let goal = GoalData::All(Goals::from(
+            interner,
+            iter::once(syn_goal).into_iter().chain(new_goals),
+        ))
+        .intern(interner);
+
+        Ok(GoalData::Quantified(
+            QuantifierKind::Exists,
+            Binders::new(VariableKinds::from(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) {
@@ -26,10 +38,33 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
                 WhereClause::AliasEq(..) => 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
     }