Add InferenceVar root-finding to NormalizeDeep

This changes NormalizeDeep to normalize unified inference variables
without values to the same 'root' inference variable, and fixes the
normalize_deep::test::infer test. The change is necessary to accomodate
the generalizer, which commonly creates new inference variables and then
unifies them with old ones. This has no functional change, but would
have broken normalization without this new behavior.

Co-authored-by: David Ross <daboross@daboross.net>

Author: 2 people

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))
+            }
         }
     }
 
@@ -104,6 +108,7 @@ mod test {
     use super::*;
     use chalk_integration::interner::ChalkIr;
     use chalk_integration::{arg, ty};
+    use chalk_solve::logging::with_tracing_logs;
 
     const U0: UniverseIndex = UniverseIndex { counter: 0 };
 
@@ -138,13 +143,16 @@ mod test {
                 &ty!(apply (item 0) (expr b)),
             )
             .unwrap();
-        // FIXME: can't just assert these are equal because the inference var gets set to a new var (?2)
-        // which is unified with b (?1). It might be good to pick a root to return. For now,
-        // this doesn't work as-is.
-        //assert_eq!(
-        //    DeepNormalizer::normalize_deep(&mut table, interner, &a),
-        //    &ty!(apply (item 1)),
-        //);
+        // 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 DeepNormalizer::normalize_deep(&mut table, interner, &b))),
+        );
         table
             .relate(
                 interner,

chalk-solve/src/infer.rs

@@ -146,6 +146,17 @@ impl<I: Interner> InferenceTable<I> {
             .map(|p| p.assert_const_ref(interner).clone())
     }
 
+    /// Finds the root inference var for the given variable.
+    ///
+    /// The returned variable will be exactly equivalent to the given
+    /// variable except in name. All variables which have been unified to
+    /// eachother (but don't yet have a value) have the same "root".
+    ///
+    /// This is useful for `DeepNormalizer`.
+    pub fn inference_var_root(&mut self, var: InferenceVar) -> InferenceVar {
+        self.unify.find(var).into()
+    }
+
     /// If type `leaf` is a free inference variable, and that variable has been
     /// bound, returns `Some(P)` where `P` is the parameter to which it has been bound.
     pub fn probe_var(&mut self, leaf: InferenceVar) -> Option<GenericArg<I>> {

chalk-solve/src/infer/var.rs

@@ -50,6 +50,12 @@ impl<I: Interner> From<InferenceVar> for EnaVariable<I> {
     }
 }
 
+impl<I: Interner> From<EnaVariable<I>> for InferenceVar {
+    fn from(ena_var: EnaVariable<I>) -> InferenceVar {
+        ena_var.var
+    }
+}
+
 impl<I: Interner> EnaVariable<I> {
     /// Convert this inference variable into a type. When using this
     /// method, naturally you should know from context that the kind