introduce "known true" into constraints

Author: nikomatsakis

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

@@ -9,8 +9,9 @@ use formality_types::{
     visit::Visit,
 };
 
-#[derive(Clone, Default, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
+#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
 pub struct Constraints {
+    known_true: bool,
     substitution: Substitution,
 }
 
@@ -24,6 +25,16 @@ where
     fn upcast_from(term: (A, B)) -> Self {
         Constraints {
             substitution: term.upcast(),
+            known_true: true,
+        }
+    }
+}
+
+impl Default for Constraints {
+    fn default() -> Self {
+        Self {
+            known_true: true,
+            substitution: Default::default(),
         }
     }
 }
@@ -53,6 +64,13 @@ impl Constraints {
             .map(|(v, p)| AtomicRelation::eq(v, p))
             .collect()
     }
+
+    pub fn ambiguous(self) -> Constraints {
+        Self {
+            known_true: false,
+            ..self
+        }
+    }
 }
 
 pub fn merge_constraints(
@@ -89,12 +107,20 @@ pub fn merge_constraints(
         .filter(|(v, _)| !existentials.contains(&v.upcast()))
         .collect();
 
-    Binder::mentioned((c1_bound_vars, existentials), Constraints { substitution })
+    let known_true = c0.known_true && c1.known_true;
+    Binder::mentioned(
+        (c1_bound_vars, existentials),
+        Constraints {
+            known_true,
+            substitution,
+        },
+    )
 }
 
 impl Fold for Constraints {
     fn substitute(&self, substitution_fn: formality_types::fold::SubstitutionFn<'_>) -> Self {
         let c = Constraints {
+            known_true: self.known_true,
             substitution: self.substitution.substitute(substitution_fn),
         };
 

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

@@ -26,7 +26,7 @@ fn eq_implies_partial_eq() {
     let constraints = prove_wc_list(program, assumptions, goal);
     expect![[r#"
         {
-            <> Constraints { substitution: Substitution { map: {} } },
+            <> Constraints { known_true: true, substitution: Substitution { map: {} } },
         }
     "#]]
     .assert_debug_eq(&constraints);

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

@@ -23,7 +23,7 @@ fn exists_u_for_t() {
     let constraints = test_prove(&program, term("<ty U> ({}, {is_implemented(Foo(U))})"));
     expect![[r#"
         {
-            <ty> Constraints { substitution: Substitution { map: {?ty_0: (rigid (adt Vec) ^ty0_0)} } },
+            <ty> Constraints { known_true: true, substitution: Substitution { map: {?ty_0: (rigid (adt Vec) ^ty0_0)} } },
         }
     "#]]
         .assert_debug_eq(&constraints);

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

@@ -30,7 +30,7 @@ fn vec_u32_debug() {
     let constraints = prove_wc_list(program, assumptions, goal);
     expect![[r#"
         {
-            <> Constraints { substitution: Substitution { map: {} } },
+            <> Constraints { known_true: true, substitution: Substitution { map: {} } },
         }
     "#]]
     .assert_debug_eq(&constraints);
@@ -44,7 +44,7 @@ fn vec_vec_u32_debug() {
     let constraints = prove_wc_list(program, assumptions, goal);
     expect![[r#"
         {
-            <> Constraints { substitution: Substitution { map: {} } },
+            <> Constraints { known_true: true, substitution: Substitution { map: {} } },
         }
     "#]]
     .assert_debug_eq(&constraints);