wrong univrese ordering

Author: nikomatsakis

crates/formality-prove/src/prove/prove_eq.rs

@@ -111,6 +111,9 @@ fn equate_variable(
 ) -> Option<(Env, Constraints)> {
     let p: Parameter = p.upcast();
 
+    let span = tracing::debug_span!("equate_variable", ?x, ?p, ?env);
+    let _guard = span.enter();
+
     let fvs = p.free_variables().deduplicate();
 
     // Ensure that `x` passes the occurs check for the free variables in `p`.
@@ -146,6 +149,7 @@ fn equate_variable(
         .chain(Some((x, universe_subst.apply(&p)).upcast()))
         .collect();
 
+    tracing::debug!("success: env={:?}, constraints={:?}", env, constraints);
     Some((env, constraints))
 }
 
@@ -161,7 +165,7 @@ fn passes_occurs_check(env: &Env, x: InferenceVar, fvs: &[Variable]) -> bool {
     for fv in fvs {
         match fv {
             Variable::PlaceholderVar(pv) => {
-                if env.universe(pv) < universe_x {
+                if universe_x < env.universe(pv) {
                     return false;
                 } else {
                 }

crates/formality-prove/src/test/eq_assumptions.rs

@@ -21,9 +21,7 @@ fn test_a() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {},
-                    },
+                    substitution: {},
                 },
             ),
         }

crates/formality-prove/src/test/exists_constraints.rs

@@ -33,10 +33,8 @@ fn exists_u_for_t() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {
-                            ?ty_1_U(0): (rigid (adt Vec) ?ty_3_U(0)),
-                        },
+                    substitution: {
+                        ?ty_1_U(0) => (rigid (adt Vec) ?ty_3_U(0)),
                     },
                 },
             ),

crates/formality-prove/src/test/expanding.rs

@@ -30,9 +30,7 @@ fn expanding() {
                 Constraints {
                     result: (),
                     known_true: false,
-                    substitution: Substitution {
-                        map: {},
-                    },
+                    substitution: {},
                 },
             ),
         }

crates/formality-prove/src/test/occurs_check.rs

@@ -44,11 +44,9 @@ fn eq_variable_to_rigid() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {
-                            ?ty_1_U(0): (rigid (adt Vec) ?ty_3_U(0)),
-                            ?ty_2_U(0): ?ty_3_U(0),
-                        },
+                    substitution: {
+                        ?ty_1_U(0) => (rigid (adt Vec) ?ty_3_U(0)),
+                        ?ty_2_U(0) => ?ty_3_U(0),
                     },
                 },
             ),
@@ -74,11 +72,9 @@ fn eq_rigid_to_variable() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {
-                            ?ty_1_U(0): (rigid (adt Vec) ?ty_3_U(0)),
-                            ?ty_2_U(0): ?ty_3_U(0),
-                        },
+                    substitution: {
+                        ?ty_1_U(0) => (rigid (adt Vec) ?ty_3_U(0)),
+                        ?ty_2_U(0) => ?ty_3_U(0),
                     },
                 },
             ),

crates/formality-prove/src/test/simple_impl.rs

@@ -31,9 +31,7 @@ fn vec_u32_debug() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {},
-                    },
+                    substitution: {},
                 },
             ),
         }
@@ -54,9 +52,7 @@ fn vec_vec_u32_debug() {
                 Constraints {
                     result: (),
                     known_true: true,
-                    substitution: Substitution {
-                        map: {},
-                    },
+                    substitution: {},
                 },
             ),
         }

crates/formality-prove/src/test/universes.rs

@@ -29,7 +29,16 @@ fn for_t_exists_u() {
     let constraints = super::test_prove(program, term("<> ({}, {for<ty T> Test(T, T)})"));
     expect![[r#"
         {
-            <> Constraints { result: (), known_true: true, substitution: Substitution { map: {} } },
+            (
+                Env {
+                    variables: [],
+                },
+                Constraints {
+                    result: (),
+                    known_true: true,
+                    substitution: {},
+                },
+            ),
         }
     "#]]
     .assert_debug_eq(&constraints);

crates/formality-types/src/grammar/ty.rs

@@ -628,7 +628,7 @@ impl std::ops::Add<usize> for VarIndex {
     }
 }
 
-#[derive(Clone, Default, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[derive(Clone, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct Substitution {
     map: Map<Variable, Parameter>,
 }
@@ -654,6 +654,25 @@ impl Substitution {
     }
 }
 
+impl std::fmt::Debug for Substitution {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let mut f = f.debug_set();
+        for (v, p) in self.iter() {
+            f.entry(&Entry { v, p });
+            struct Entry {
+                v: Variable,
+                p: Parameter,
+            }
+            impl std::fmt::Debug for Entry {
+                fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+                    write!(f, "{:?} => {:?}", self.v, self.p)
+                }
+            }
+        }
+        f.finish()
+    }
+}
+
 impl<Vs> std::ops::SubAssign<Vs> for Substitution
 where
     Vs: Upcast<Vec<Variable>>,