Variance

chalk-derive/src/lib.rs

@@ -224,7 +224,7 @@ fn derive_zip(mut s: synstructure::Structure) -> TokenStream {
     let mut body = each_variant_pair(&mut a, &mut b, |v_a, v_b| {
         let mut t = TokenStream::new();
         for (b_a, b_b) in v_a.bindings().iter().zip(v_b.bindings().iter()) {
-            quote!(chalk_ir::zip::Zip::zip_with(zipper, #b_a, #b_b)?;).to_tokens(&mut t);
+            quote!(chalk_ir::zip::Zip::zip_with(zipper, variance, #b_a, #b_b)?;).to_tokens(&mut t);
         }
         quote!(Ok(())).to_tokens(&mut t);
         t
@@ -240,8 +240,9 @@ fn derive_zip(mut s: synstructure::Structure) -> TokenStream {
 
             fn zip_with<'i, Z: ::chalk_ir::zip::Zipper<'i, #interner>>(
                 zipper: &mut Z,
-                 a: &Self,
-                 b: &Self,
+                variance: ::chalk_ir::Variance,
+                a: &Self,
+                b: &Self,
             ) -> ::chalk_ir::Fallible<()>
             where
                 #interner: 'i,

chalk-engine/src/logic.rs

@@ -12,8 +12,8 @@ use crate::{
 
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    AnswerSubst, Canonical, CanonicalVarKinds, ConstrainedSubst, Floundered, Goal, GoalData,
-    InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
+    AnswerSubst, Canonical, CanonicalVarKinds, ConstrainedSubst, FallibleOrFloundered, Floundered,
+    Goal, GoalData, InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
 };
 use chalk_solve::clauses::program_clauses_for_goal;
 use chalk_solve::coinductive_goal::IsCoinductive;
@@ -278,6 +278,7 @@ impl<I: Interner> Forest<I> {
                             info!("program clause = {:#?}", clause);
                             let mut infer = infer.clone();
                             if let Ok(resolvent) = infer.resolvent_clause(
+                                context.unification_database(),
                                 context.program().interner(),
                                 &environment,
                                 &domain_goal,
@@ -316,21 +317,23 @@ impl<I: Interner> Forest<I> {
                 // simplified subgoals. You can think of this as
                 // applying built-in "meta program clauses" that
                 // reduce goals into Domain goals.
-                if let Ok(ex_clause) =
-                    Self::simplify_goal(context, &mut infer, subst, environment, goal)
-                {
-                    info!(
-                        ex_clause = ?infer.debug_ex_clause(context.program().interner(), &ex_clause),
-                        "pushing initial strand"
-                    );
-                    let strand = Strand {
-                        infer,
-                        ex_clause,
-                        selected_subgoal: None,
-                        last_pursued_time: TimeStamp::default(),
-                    };
-                    let canonical_strand = Self::canonicalize_strand(context, strand);
-                    table.enqueue_strand(canonical_strand);
+                match Self::simplify_goal(context, &mut infer, subst, environment, goal) {
+                    FallibleOrFloundered::Ok(ex_clause) => {
+                        info!(
+                            ex_clause = ?infer.debug_ex_clause(context.program().interner(), &ex_clause),
+                            "pushing initial strand"
+                        );
+                        let strand = Strand {
+                            infer,
+                            ex_clause,
+                            selected_subgoal: None,
+                            last_pursued_time: TimeStamp::default(),
+                        };
+                        let canonical_strand = Self::canonicalize_strand(context, strand);
+                        table.enqueue_strand(canonical_strand);
+                    }
+                    FallibleOrFloundered::NoSolution => {}
+                    FallibleOrFloundered::Floundered => table.mark_floundered(),
                 }
             }
         }
@@ -653,6 +656,7 @@ impl<'forest, I: Interner> SolveState<'forest, I> {
                 );
                 match strand.infer.apply_answer_subst(
                     self.context.program().interner(),
+                    self.context.unification_database(),
                     &mut strand.ex_clause,
                     &subgoal,
                     &table_goal,

chalk-engine/src/normalize_deep.rs

@@ -55,7 +55,11 @@ where
                 .assert_ty_ref(interner)
                 .fold_with(self, DebruijnIndex::INNERMOST)?
                 .shifted_in(interner)), // FIXME shift
-            None => Ok(var.to_ty(interner, kind)),
+            None => {
+                // Normalize all inference vars which have been unified into a
+                // single variable. Ena calls this the "root" variable.
+                Ok(self.table.inference_var_root(var).to_ty(interner, kind))
+            }
         }
     }
 
@@ -107,6 +111,20 @@ mod test {
 
     const U0: UniverseIndex = UniverseIndex { counter: 0 };
 
+    // We just use a vec of 20 `Invariant`, since this is zipped and no substs are
+    // longer than this
+    #[derive(Debug)]
+    struct TestDatabase;
+    impl UnificationDatabase<ChalkIr> for TestDatabase {
+        fn fn_def_variance(&self, _fn_def_id: FnDefId<ChalkIr>) -> Variances<ChalkIr> {
+            Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied())
+        }
+
+        fn adt_variance(&self, _adt_id: AdtId<ChalkIr>) -> Variances<ChalkIr> {
+            Variances::from(&ChalkIr, [Variance::Invariant; 20].iter().copied())
+        }
+    }
+
     #[test]
     fn infer() {
         let interner = &ChalkIr;
@@ -115,14 +133,34 @@ mod test {
         let a = table.new_variable(U0).to_ty(interner);
         let b = table.new_variable(U0).to_ty(interner);
         table
-            .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr b)))
+            .relate(
+                interner,
+                &TestDatabase,
+                &environment0,
+                Variance::Invariant,
+                &a,
+                &ty!(apply (item 0) (expr b)),
+            )
             .unwrap();
+        // a is unified to Adt<#0>(c), where 'c' is a new inference var
+        // created by the generalizer to generalize 'b'. It then unifies 'b'
+        // and 'c', and when we normalize them, they'll both be output as
+        // the same "root" variable. However, there are no guarantees for
+        // _which_ of 'b' and 'c' becomes the root. We need to normalize
+        // "b" too, then, to ensure we get a consistent result.
         assert_eq!(
             DeepNormalizer::normalize_deep(&mut table, interner, &a),
-            ty!(apply (item 0) (expr b))
+            ty!(apply (item 0) (expr DeepNormalizer::normalize_deep(&mut table, interner, &b))),
         );
         table
-            .unify(interner, &environment0, &b, &ty!(apply (item 1)))
+            .relate(
+                interner,
+                &TestDatabase,
+                &environment0,
+                Variance::Invariant,
+                &b,
+                &ty!(apply (item 1)),
+            )
             .unwrap();
         assert_eq!(
             DeepNormalizer::normalize_deep(&mut table, interner, &a),

chalk-engine/src/simplify.rs

@@ -5,7 +5,8 @@ use crate::{ExClause, Literal, TimeStamp};
 use chalk_ir::cast::Cast;
 use chalk_ir::interner::Interner;
 use chalk_ir::{
-    Environment, Fallible, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
+    Environment, FallibleOrFloundered, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
+    Variance,
 };
 use tracing::debug;
 
@@ -19,7 +20,7 @@ impl<I: Interner> Forest<I> {
         subst: Substitution<I>,
         initial_environment: Environment<I>,
         initial_goal: Goal<I>,
-    ) -> Fallible<ExClause<I>> {
+    ) -> FallibleOrFloundered<ExClause<I>> {
         let mut ex_clause = ExClause {
             subst,
             ambiguous: false,
@@ -65,13 +66,37 @@ impl<I: Interner> Forest<I> {
                             subgoal.clone(),
                         )));
                 }
-                GoalData::EqGoal(goal) => infer.unify_generic_args_into_ex_clause(
+                GoalData::EqGoal(goal) => match infer.relate_generic_args_into_ex_clause(
                     context.program().interner(),
+                    context.unification_database(),
                     &environment,
+                    Variance::Invariant,
                     &goal.a,
                     &goal.b,
                     &mut ex_clause,
-                )?,
+                ) {
+                    Ok(()) => {}
+                    Err(_) => return FallibleOrFloundered::NoSolution,
+                },
+                GoalData::SubtypeGoal(goal) => {
+                    if goal.a.inference_var(context.program().interner()).is_some()
+                        && goal.b.inference_var(context.program().interner()).is_some()
+                    {
+                        return FallibleOrFloundered::Floundered;
+                    }
+                    match infer.relate_tys_into_ex_clause(
+                        context.program().interner(),
+                        context.unification_database(),
+                        &environment,
+                        Variance::Covariant,
+                        &goal.a,
+                        &goal.b,
+                        &mut ex_clause,
+                    ) {
+                        Ok(()) => {}
+                        Err(_) => return FallibleOrFloundered::NoSolution,
+                    }
+                }
                 GoalData::DomainGoal(domain_goal) => {
                     ex_clause
                         .subgoals
@@ -87,6 +112,6 @@ impl<I: Interner> Forest<I> {
             }
         }
 
-        Ok(ex_clause)
+        FallibleOrFloundered::Ok(ex_clause)
     }
 }

chalk-engine/src/slg.rs

@@ -6,7 +6,7 @@ use chalk_ir::cast::Caster;
 use chalk_ir::interner::Interner;
 use chalk_ir::*;
 use chalk_solve::infer::ucanonicalize::UCanonicalized;
-use chalk_solve::infer::unify::UnificationResult;
+use chalk_solve::infer::unify::RelationResult;
 use chalk_solve::infer::InferenceTable;
 use chalk_solve::solve::truncate;
 use chalk_solve::RustIrDatabase;
@@ -81,6 +81,10 @@ impl<I: Interner> SlgContextOps<'_, I> {
     pub(crate) fn max_size(&self) -> usize {
         self.max_size
     }
+
+    pub(crate) fn unification_database(&self) -> &dyn UnificationDatabase<I> {
+        self.program.unification_database()
+    }
 }
 
 /// "Truncation" (called "abstraction" in the papers referenced below)
@@ -111,6 +115,7 @@ pub trait ResolventOps<I: Interner> {
     /// The bindings in `infer` are unaffected by this operation.
     fn resolvent_clause(
         &mut self,
+        ops: &dyn UnificationDatabase<I>,
         interner: &I,
         environment: &Environment<I>,
         goal: &DomainGoal<I>,
@@ -121,6 +126,7 @@ pub trait ResolventOps<I: Interner> {
     fn apply_answer_subst(
         &mut self,
         interner: &I,
+        unification_database: &dyn UnificationDatabase<I>,
         ex_clause: &mut ExClause<I>,
         selected_goal: &InEnvironment<Goal<I>>,
         answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
@@ -187,14 +193,27 @@ pub trait UnificationOps<I: Interner> {
     ///
     /// If the parameters fail to unify, then `Error` is returned
     // Used by: simplify
-    fn unify_generic_args_into_ex_clause(
+    fn relate_generic_args_into_ex_clause(
         &mut self,
         interner: &I,
+        db: &dyn UnificationDatabase<I>,
         environment: &Environment<I>,
+        variance: Variance,
         a: &GenericArg<I>,
         b: &GenericArg<I>,
         ex_clause: &mut ExClause<I>,
     ) -> Fallible<()>;
+
+    fn relate_tys_into_ex_clause(
+        &mut self,
+        interner: &I,
+        db: &dyn UnificationDatabase<I>,
+        environment: &Environment<I>,
+        variance: Variance,
+        a: &Ty<I>,
+        b: &Ty<I>,
+        ex_clause: &mut ExClause<I>,
+    ) -> Fallible<()>;
 }
 
 #[derive(Clone)]
@@ -305,23 +324,43 @@ impl<I: Interner> UnificationOps<I> for TruncatingInferenceTable<I> {
         self.infer.invert(interner, value)
     }
 
-    fn unify_generic_args_into_ex_clause(
+    fn relate_generic_args_into_ex_clause(
         &mut self,
         interner: &I,
+        db: &dyn UnificationDatabase<I>,
         environment: &Environment<I>,
+        variance: Variance,
         a: &GenericArg<I>,
         b: &GenericArg<I>,
         ex_clause: &mut ExClause<I>,
     ) -> Fallible<()> {
-        let result = self.infer.unify(interner, environment, a, b)?;
+        let result = self
+            .infer
+            .relate(interner, db, environment, variance, a, b)?;
+        Ok(into_ex_clause(interner, result, ex_clause))
+    }
+
+    fn relate_tys_into_ex_clause(
+        &mut self,
+        interner: &I,
+        db: &dyn UnificationDatabase<I>,
+        environment: &Environment<I>,
+        variance: Variance,
+        a: &Ty<I>,
+        b: &Ty<I>,
+        ex_clause: &mut ExClause<I>,
+    ) -> Fallible<()> {
+        let result = self
+            .infer
+            .relate(interner, db, environment, variance, a, b)?;
         Ok(into_ex_clause(interner, result, ex_clause))
     }
 }
 
 /// Helper function
 fn into_ex_clause<I: Interner>(
     interner: &I,
-    result: UnificationResult<I>,
+    result: RelationResult<I>,
     ex_clause: &mut ExClause<I>,
 ) {
     ex_clause.subgoals.extend(