Auto merge of #609 - daboross:subtype-variance-and-goal-writer, r=nikomatsakis

Variance

This contains `@super-tuple` and my work on rebasing `@jackh726's` variance work from #520 and implementing the generalizer on top of it.

As mentioned in Zulip, we've been trying to port rustc tests for the generalizer to chalk, in an effort to see what fails. Since we've been failing at this for so long, we decided to just try to write the generalizer instead! We don't fully understand it, but have enough of an idea to write something that hopefully works.

This fails 5 of the existing tests, and that's part of the motivation for opening this now - we aren't sure how to proceed on those. We have not written any new tests for variance nor the generalizer.

The last one we've debugged is `dyn_lifetime_bound`, which fails because when unifying our generalized value and the original ty value, the code tries to unify a inference var with universe 4, created freshly for our generalized value, with a placeholder with universe 6 - and that fails to pass the `OccursCheck`. Here's the debug logs we generated for that failed test: https://gist.github.com/daboross/24f1d2310bd86e1d542678c4ebd550e0

Author: bors

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(