alias eq goals

Author: basil-cow

chalk-solve/src/clauses/builder.rs

@@ -80,7 +80,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
         let clause = if self.binders.len() == 0 {
             ProgramClauseData::Implies(clause).intern(interner)
         } else {
-            ProgramClauseData::ForAll(Binders::new(ParameterKinds::from(interner, self.binders.clone()), clause)).intern(interner)
+            ProgramClauseData::ForAll(Binders::new(
+                ParameterKinds::from(interner, self.binders.clone()),
+                clause,
+            ))
+            .intern(interner)
         };
 
         self.clauses.push(syn_eq_lower(interner, &clause));

chalk-solve/src/clauses/program_clauses.rs

@@ -735,6 +735,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()),
@@ -743,8 +744,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.
@@ -753,7 +754,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

@@ -2,49 +2,34 @@ use std::{iter, mem::replace};
 
 use chalk_engine::fallible::Fallible;
 use chalk_ir::{
+    cast::Cast,
     fold::{shift::Shift, Fold, Folder, SuperFold},
     interner::Interner,
-    Binders, BoundVar, DebruijnIndex, EqGoal, Goal, GoalData, Goals, Parameter, ProgramClause,
-    ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, ParameterKind, ApplicationTy, TypeName,
-    ParameterKinds,
+    AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, Goal, GoalData, Goals, ParameterKind,
+    ParameterKinds, ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty,
+    TyData,
 };
 
-pub fn syn_eq_lower<I: Interner>(interner: &I, clause: &ProgramClause<I>) -> ProgramClause<I> {
+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()
+    clause
+        .fold_with(&mut folder, DebruijnIndex::INNERMOST)
+        .unwrap()
 }
 
 struct SynEqFolder<'i, I: Interner> {
     interner: &'i I,
-    new_params: Vec<Parameter<I>>,
+    new_params: Vec<ParameterKind<()>>,
+    new_goals: Vec<Goal<I>>,
     binders_len: usize,
 }
 
-impl<'i, I: Interner> SynEqFolder<'i, I>
-where
-    I: 'i,
-{
-    fn to_eq_goals(&self, new_params: Vec<Parameter<I>>, old_len: usize) -> impl Iterator<Item = Goal<I>> + 'i {
-        let interner = self.interner;
-        new_params.into_iter().enumerate().map(move |(i, p)| {
-            let var = BoundVar {
-                debruijn: DebruijnIndex::INNERMOST,
-                index: i + old_len,
-            };
-            GoalData::EqGoal(EqGoal {
-                a: p.replace_bound(var, interner),
-                b: p,
-            })
-            .intern(interner)
-        })
-    }
-}
-
 impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
     fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
         self
@@ -54,14 +39,23 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
         let interner = self.interner;
         let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, self.binders_len);
 
-        let folded = ty.super_fold_with(self, outer_binder)?;
-        match folded.data(interner) {
-            TyData::Apply(ApplicationTy { name: TypeName::AssociatedType(_), .. }) => {
-                self.new_params.push(ParameterKind::Ty(ty.clone()).intern(interner));
+        let new_ty = TyData::BoundVar(bound_var).intern(interner);
+        match ty.data(interner) {
+            TyData::Alias(alias @ AliasTy::Projection(_)) => {
+                self.new_params.push(ParameterKind::Ty(()));
+                self.new_goals.push(
+                    AliasEq {
+                        alias: alias.clone(),
+                        ty: new_ty.clone(),
+                    }
+                    .cast(interner),
+                );
                 self.binders_len += 1;
-                Ok(TyData::BoundVar(bound_var).intern(interner))
+                ty.super_fold_with(self, outer_binder)?;
+                Ok(new_ty)
             }
-            _ => ty.super_fold_with(self, outer_binder),
+            TyData::Function(_) => Ok(ty.clone()),
+            _ => Ok(ty.super_fold_with(self, outer_binder)?),
         }
     }
 
@@ -73,42 +67,46 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
         let interner = self.interner;
 
         let ((binders, implication), in_binders) = match clause.data(interner) {
-            ProgramClauseData::ForAll(for_all) => {
-                (for_all.clone().into(), true)
-            }
+            ProgramClauseData::ForAll(for_all) => (for_all.clone().into(), true),
             // introduce a dummy binder and shift implication through it
-            ProgramClauseData::Implies(implication) => ((ParameterKinds::new(interner), implication.shifted_in(interner)), false),
+            ProgramClauseData::Implies(implication) => (
+                (
+                    ParameterKinds::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)?)
+            return Ok(ProgramClauseData::Implies(
+                ProgramClauseImplication {
+                    consequence,
+                    conditions,
+                    priority: implication.priority,
+                }
+                .shifted_out(interner)?,
+            )
             .intern(interner));
         }
 
-        let old_len = binders.len();
-        binders.extend(new_params.iter().map(|p| p.data(interner).anonymize()));
+        binders.extend(new_params.into_iter());
 
         conditions = Goals::from(
             interner,
-            conditions
-                .iter(interner)
-                .cloned()
-                .chain(self.to_eq_goals(new_params, old_len)),
+            conditions.iter(interner).cloned().chain(new_goals),
         );
 
         Ok(ProgramClauseData::ForAll(Binders::new(
@@ -126,37 +124,35 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {
         assert!(self.new_params.is_empty(), true);
 
         let interner = self.interner;
-        let domain_goal = match goal.data(interner) {
-            GoalData::DomainGoal(dg) => dg,
+        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 domain_goal =
-            GoalData::DomainGoal(domain_goal.shifted_in(interner).fold_with(self, outer_binder)?).intern(interner);
+        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![]);
 
-        let binders: Vec<_> = new_params
-            .iter()
-            .map(|p| p.data(interner).anonymize())
-            .collect();
-
-        if binders.is_empty() {
+        if new_params.is_empty() {
             return Ok(goal.clone());
         }
 
         let goal = GoalData::All(Goals::from(
             interner,
-            iter::once(domain_goal).chain(self.to_eq_goals(new_params, 0)),
+            iter::once(syn_goal).into_iter().chain(new_goals),
         ))
         .intern(interner);
 
-        Ok(
-            GoalData::Quantified(QuantifierKind::Exists, Binders::new(ParameterKinds::from(interner, binders), goal))
-                .intern(interner),
+        Ok(GoalData::Quantified(
+            QuantifierKind::Exists,
+            Binders::new(ParameterKinds::from(interner, new_params), goal),
         )
+        .intern(interner))
     }
 
     fn interner(&self) -> &'i I {

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
     }