improve eq

also improve tracing and debuggability

Author: nikomatsakis

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

@@ -1,9 +1,9 @@
 use formality_types::{
-    cast::Upcast,
+    cast::{Downcast, Upcast},
     cast_impl,
-    derive_links::UpcastFrom,
+    derive_links::{DowncastTo, UpcastFrom},
     fold::Fold,
-    grammar::{Parameter, Substitution, Variable},
+    grammar::{InferenceVar, Parameter, Substitution, Variable},
     term::Term,
     visit::Visit,
 };
@@ -191,6 +191,7 @@ impl<R: Term> Visit for Constraints<R> {
         let domain = substitution.domain();
 
         for &v in &domain {
+            assert!(v.downcast::<InferenceVar>().is_some());
             assert!(v.is_free());
             assert!(is_valid_binding(v, &substitution[v]));
         }

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

@@ -10,16 +10,16 @@ use super::constraints::Constraints;
 judgment_fn! {
     pub fn prove_after(
         program: Program,
-        env1: Env,
-        c1: Constraints,
+        env: Env,
+        constraints: Constraints,
         assumptions: Wcs,
         goal: Wcs,
     ) => (Env, Constraints) {
         (
             (let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))
-            (prove(program, env1, assumptions, goal) => (env2, c2))
+            (prove(program, env, assumptions, goal) => (env, c2))
             --- ("prove_after")
-            (prove_after(program, env1, c1, assumptions, goal) => (env2, c1.seq(c2)))
+            (prove_after(program, env, c1, assumptions, goal) => (env, c1.seq(c2)))
         )
     }
 }

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

@@ -1,18 +1,20 @@
 use formality_types::{
-    cast::{Downcast, Upcast, Upcasted},
-    collections::Deduplicate,
+    cast::{Downcast, Downcasted, Upcast, Upcasted},
+    collections::{Deduplicate, Set},
     grammar::{
-        AliasTy, AtomicRelation, InferenceVar, Parameter, RigidTy, Substitution, Ty, TyData,
-        Variable, Wcs,
+        AliasTy, AtomicRelation, InferenceVar, Parameter, PlaceholderVar, RigidTy, Substitution,
+        Ty, TyData, Variable, Wcs,
     },
-    judgment_fn,
+    judgment_fn, set,
     visit::Visit,
 };
 
 use crate::{
     program::Program,
     prove::{
-        constraints::no_constraints, prove, prove_after::prove_after,
+        constraints::{no_constraints, occurs_in},
+        prove,
+        prove_after::prove_after,
         prove_normalize::prove_normalize,
     },
 };
@@ -75,17 +77,17 @@ judgment_fn! {
         )
 
         (
-            (if let None = t.downcast::<InferenceVar>())
-            (if let Some(env_c) = equate_variable(env, v, t))
+            (if let None = t.downcast::<Variable>())
+            (equate_variable(program, env, assumptions, v, t) => (env, c))
             ----------------------------- ("existential-l")
-            (prove_ty_eq(_program, env, _assumptions, Variable::InferenceVar(v), t) => env_c)
+            (prove_ty_eq(program, env, assumptions, Variable::InferenceVar(v), t) => (env, c))
         )
 
         (
-            (if let None = t.downcast::<InferenceVar>())
-            (if let Some(env_c) = equate_variable(env, v, t))
+            (if let None = t.downcast::<Variable>())
+            (equate_variable(program, env, assumptions, v, t) => (env, c))
             ----------------------------- ("existential-r")
-            (prove_ty_eq(_program, env, _assumptions, t, Variable::InferenceVar(v)) => env_c)
+            (prove_ty_eq(program, env, assumptions, t, Variable::InferenceVar(v)) => (env, c))
         )
 
         (
@@ -95,6 +97,12 @@ judgment_fn! {
             (prove_ty_eq(_program, env, _assumptions, Variable::InferenceVar(l), Variable::InferenceVar(r)) => (env, (b, a)))
         )
 
+        (
+            (if env.universe(p) < env.universe(v))
+            ----------------------------- ("existential-vs-placeholder")
+            (prove_ty_eq(_program, env, _assumptions, Variable::InferenceVar(v), Variable::PlaceholderVar(p)) => (env, (v, p)))
+        )
+
         (
             (prove_normalize(&program, env, &assumptions, &x) => (env1, y, c1))
             (prove_after(&program, env1, c1, &assumptions, eq(y, &z)) => (env2, c2))
@@ -105,20 +113,24 @@ judgment_fn! {
 }
 
 fn equate_variable(
+    program: Program,
     mut env: Env,
+    assumptions: Wcs,
     x: InferenceVar,
     p: impl Upcast<Parameter>,
-) -> Option<(Env, Constraints)> {
+) -> Set<(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();
 
+    env.assert_encloses((x, &fvs));
+
     // Ensure that `x` passes the occurs check for the free variables in `p`.
-    if !passes_occurs_check(&env, x, &fvs) {
-        return None;
+    if occurs_in(x, &fvs) {
+        return set![];
     }
 
     // Map each free variable `fv` in `p` that is of higher universe than `x`
@@ -130,7 +142,7 @@ fn equate_variable(
     let universe_x = env.universe(x);
     let universe_subst: Substitution = fvs
         .iter()
-        .flat_map(|&fv| {
+        .flat_map(|fv| {
             if universe_x < env.universe(fv) {
                 let y = env.insert_fresh_before(fv.kind(), universe_x);
                 Some((fv, y))
@@ -146,41 +158,23 @@ fn equate_variable(
     // * `x = universe_subst(p)` (e.g., `Vec<Z>` in our example above)
     let constraints: Constraints = universe_subst
         .iter()
+        .filter(|(v, _)| v.is_a::<InferenceVar>())
         .chain(Some((x, universe_subst.apply(&p)).upcast()))
         .collect();
 
-    tracing::debug!("success: env={:?}, constraints={:?}", env, constraints);
-    Some((env, constraints))
-}
-
-/// An existential variable `x` *passes the occurs check* with respect to
-/// a set of free variables `fvs` if
-///
-/// * `x` is not a member of `fvs`
-/// * all placeholders in `fvs` are in a lower universe than `v`
-fn passes_occurs_check(env: &Env, x: InferenceVar, fvs: &[Variable]) -> bool {
-    env.assert_encloses((x, fvs));
+    let goals: Wcs = universe_subst
+        .iter()
+        .filter(|(v, _)| v.is_a::<PlaceholderVar>())
+        .map(|(v, p)| eq(v, p))
+        .upcasted()
+        .collect();
 
-    let universe_x = env.universe(x);
-    for fv in fvs {
-        match fv {
-            Variable::PlaceholderVar(pv) => {
-                if universe_x < env.universe(pv) {
-                    return false;
-                } else {
-                }
-            }
-            Variable::InferenceVar(iv) => {
-                if *iv == x {
-                    return false;
-                } else {
-                }
-            }
-            Variable::BoundVar(_) => {
-                panic!("unexpected bound variable");
-            }
-        }
-    }
+    tracing::debug!(
+        "equated: env={:?}, constraints={:?}, goals={:?}",
+        env,
+        constraints,
+        goals
+    );
 
-    true
+    prove_after(program, env, constraints, assumptions, goals)
 }

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

@@ -36,7 +36,24 @@ fn test_b() {
         term("<ty A> ({}, {for<ty T, ty U> if {T = u32, U = Vec<T>} A = U})"),
     );
     expect![[r#"
-        {}
-    "#]] // FIXME
+        {
+            (
+                Env {
+                    variables: [
+                        ?ty_4_U(0),
+                        ?ty_1_U(0),
+                    ],
+                },
+                Constraints {
+                    result: (),
+                    known_true: true,
+                    substitution: {
+                        ?ty_1_U(0) => (rigid (adt Vec) (rigid (scalar u32))),
+                        ?ty_4_U(0) => (rigid (scalar u32)),
+                    },
+                },
+            ),
+        }
+    "#]]
     .assert_debug_eq(&constraints);
 }

crates/formality-types/src/cast.rs

@@ -44,6 +44,13 @@ pub trait Downcast: Sized {
     fn downcast<T>(&self) -> Option<T>
     where
         T: DowncastFrom<Self>;
+
+    fn is_a<T>(&self) -> bool
+    where
+        T: DowncastFrom<Self>,
+    {
+        self.downcast::<T>().is_some()
+    }
 }
 
 impl<U> Downcast for U {

crates/formality-types/src/fixed_point.rs

@@ -7,6 +7,7 @@ mod stack;
 pub use stack::FixedPointStack;
 
 pub fn fixed_point<Input, Output>(
+    tracing_span: impl Fn(&Input) -> tracing::Span,
     storage: &'static LocalKey<RefCell<FixedPointStack<Input, Output>>>,
     args: Input,
     default_value: impl Fn(&Input) -> Output,
@@ -18,6 +19,7 @@ where
 {
     stacker::maybe_grow(32 * 1024, 1024 * 1024, || {
         FixedPoint {
+            tracing_span,
             storage,
             default_value,
             next_value,
@@ -26,7 +28,12 @@ where
     })
 }
 
-struct FixedPoint<Input: Value, Output: Value, DefaultValue, NextValue> {
+struct FixedPoint<Input, Output, DefaultValue, NextValue, TracingSpan>
+where
+    Input: Value,
+    Output: Value,
+{
+    tracing_span: TracingSpan,
     storage: &'static LocalKey<RefCell<FixedPointStack<Input, Output>>>,
     default_value: DefaultValue,
     next_value: NextValue,
@@ -35,15 +42,18 @@ struct FixedPoint<Input: Value, Output: Value, DefaultValue, NextValue> {
 pub trait Value: Clone + Eq + Debug + Hash + 'static {}
 impl<T: Clone + Eq + Debug + Hash + 'static> Value for T {}
 
-impl<Input, Output, DefaultValue, NextValue> FixedPoint<Input, Output, DefaultValue, NextValue>
+impl<Input, Output, DefaultValue, NextValue, TracingSpan>
+    FixedPoint<Input, Output, DefaultValue, NextValue, TracingSpan>
 where
     Input: Value,
     Output: Value,
     DefaultValue: Fn(&Input) -> Output,
     NextValue: Fn(Input) -> Output,
+    TracingSpan: Fn(&Input) -> tracing::Span,
 {
     fn apply(&self, input: Input) -> Output {
         if let Some(r) = self.with_stack(|stack| stack.search(&input)) {
+            tracing::debug!("recursive call to {:?}, yielding {:?}", input, r);
             return r;
         }
 
@@ -53,12 +63,14 @@ where
         });
 
         loop {
-            let span = tracing::debug_span!("fixed-point iteration", ?input);
+            let span = (self.tracing_span)(&input);
             let _guard = span.enter();
             let output = (self.next_value)(input.clone());
             tracing::debug!(?output);
             if !self.with_stack(|stack| stack.update_output(&input, output)) {
                 break;
+            } else {
+                tracing::debug!("output is different from previous iteration, re-executing until fixed point is reached");
             }
         }