Merge pull request #171 from lcnr/coherence-cont

continue coherence work

book/src/formality_core/judgment_fn.md

@@ -1,6 +1,6 @@
 # Judgment functions and inference rules
 
-The next thing is the `judgement_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things:
+The next thing is the `judgment_fn!` macro. This lets you write a *judgment* using *inference rules*. A "judgment" just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things:
 
 ```
 premise1

crates/formality-check/src/coherence.rs

@@ -53,11 +53,14 @@ impl Check<'_> {
         let a = env.instantiate_universally(&impl_a.binder);
         let trait_ref = a.trait_ref();
 
-        self.prove_goal(
-            &env.with_coherence_mode(true),
-            &a.where_clauses,
-            trait_ref.is_local(),
-        )
+        // The orphan check passes if
+        // ∀P. ⌐ (coherence_mode => (wf(Ts) && cannot_be_proven(is_local_trait_ref)))
+        //
+        // TODO: feels like we do want a general "not goal", flipping existentials
+        // and universals and the coherence mode
+        // self.prove_not_goal(&env, &(Wcs::wf))
+
+        self.prove_goal(&env, &a.where_clauses, trait_ref.is_local())
     }
 
     #[context("orphan_check_neg({impl_a:?})")]
@@ -67,11 +70,7 @@ impl Check<'_> {
         let a = env.instantiate_universally(&impl_a.binder);
         let trait_ref = a.trait_ref();
 
-        self.prove_goal(
-            &env.with_coherence_mode(true),
-            &a.where_clauses,
-            trait_ref.is_local(),
-        )
+        self.prove_goal(&env, &a.where_clauses, trait_ref.is_local())
     }
 
     #[tracing::instrument(level = "Debug", skip(self))]
@@ -100,7 +99,7 @@ impl Check<'_> {
         //
         // ∀P_a, ∀P_b. ⌐ (coherence_mode => (Ts_a = Ts_b && WC_a && WC_b))
         if let Ok(()) = self.prove_not_goal(
-            &env.with_coherence_mode(true),
+            &env,
             (),
             (
                 Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),

crates/formality-check/src/lib.rs

@@ -3,12 +3,12 @@
 use std::{collections::VecDeque, fmt::Debug};
 
 use anyhow::bail;
-use formality_prove::{Decls, Env};
+use formality_prove::{is_definitely_not_proveable, Decls, Env};
 use formality_rust::{
     grammar::{Crate, CrateItem, Program, Test, TestBoundData},
     prove::ToWcs,
 };
-use formality_types::grammar::{Fallible, Substitution, Wcs};
+use formality_types::grammar::{Fallible, Wcs};
 
 /// Check all crates in the program. The crates must be in dependency order
 /// such that any prefix of the crates is a complete program.
@@ -115,58 +115,24 @@ impl Check<'_> {
     }
 
     #[tracing::instrument(level = "Debug", skip(self, assumptions, goal))]
-    fn prove_not_goal(
-        &self,
-        env: &Env,
-        assumptions: impl ToWcs,
-        goal: impl ToWcs + Debug,
-    ) -> Fallible<()> {
+    fn prove_not_goal(&self, env: &Env, assumptions: impl ToWcs, goal: impl ToWcs) -> Fallible<()> {
         let goal: Wcs = goal.to_wcs();
         let assumptions: Wcs = assumptions.to_wcs();
 
-        tracing::debug!("assumptions = {assumptions:?}");
-        tracing::debug!("goal = {goal:?}");
-
         assert!(env.only_universal_variables());
         assert!(env.encloses((&assumptions, &goal)));
 
-        // Proving `∀X. not(F(X))` is the same as proving: `not(∃X. F(X))`.
-        // Therefore, since we have only universal variables, we can change them all to
-        // existential and then try to prove. If we get back no solutions, we know that
-        // we've proven the negation. (This is called the "negation as failure" property,
-        // and it relies on our solver being complete -- i.e., if there is a solution,
-        // we'll find it, or at least return ambiguous.)
-        let mut existential_env = Env::default().with_coherence_mode(env.is_in_coherence_mode());
-        let universal_to_existential: Substitution = env
-            .variables()
-            .iter()
-            .map(|v| {
-                assert!(v.is_universal());
-                let v1 = existential_env.fresh_existential(v.kind());
-                (v, v1)
-            })
-            .collect();
-
-        let existential_assumptions = universal_to_existential.apply(&assumptions);
-        let existential_goal = universal_to_existential.apply(&goal);
-
-        let cs = formality_prove::prove(
-            self.decls,
-            &existential_env,
-            existential_assumptions.to_wcs(),
-            &existential_goal,
+        let cs = is_definitely_not_proveable(
+            env,
+            &assumptions,
+            goal.clone(),
+            |env, assumptions, goal| formality_prove::prove(self.decls, env, &assumptions, &goal),
         );
-
-        match cs.into_set() {
-            Ok(proofs) => {
-                bail!(
-                    "failed to disprove\n    {goal:?}\ngiven\n    {assumptions:?}\ngot\n{proofs:?}"
-                )
-            }
-            Err(err) => {
-                tracing::debug!("Proved not goal, error = {err}");
-                return Ok(());
-            }
+        let cs = cs.into_set()?;
+        if cs.iter().any(|c| c.unconditionally_true()) {
+            return Ok(());
         }
+
+        bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
 }

crates/formality-core/src/test_util.rs

@@ -41,7 +41,7 @@ use std::fmt::{Debug, Display};
 /// with `"src/file.rs:LL:CC"`. This makes error messages resilient against changes to the source code.
 pub fn normalize_paths(s: impl Display) -> String {
     let s = s.to_string();
-    let re = regex::Regex::new(r"\([^():]+.rs:\d+:\d+\)").unwrap();
+    let re = regex::Regex::new(r"\([^()]+.rs:\d+:\d+\)").unwrap();
     re.replace_all(&s, "(src/file.rs:LL:CC)").to_string()
 }
 

crates/formality-core/src/visit.rs

@@ -2,7 +2,7 @@ use std::sync::Arc;
 
 use crate::{collections::Set, language::Language, variable::CoreVariable};
 
-pub trait CoreVisit<L: Language> {
+pub trait CoreVisit<L: Language>: std::fmt::Debug {
     /// Extract the list of free variables (for the purposes of this function, defined by `Variable::is_free`).
     /// The list may contain duplicates and must be in a determinstic order (though the order itself isn't important).
     fn free_variables(&self) -> Vec<CoreVariable<L>>;

crates/formality-prove/src/lib.rs

@@ -8,7 +8,8 @@ mod prove;
 pub use decls::*;
 pub use prove::prove;
 pub use prove::Constraints;
-pub use prove::Env;
+pub use prove::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure};
+pub use prove::{Bias, Env};
 
 #[cfg(test)]
 mod test;

crates/formality-prove/src/prove.rs

@@ -3,6 +3,7 @@ mod constraints;
 mod env;
 mod is_local;
 mod minimize;
+mod negation;
 mod prove_after;
 mod prove_eq;
 mod prove_normalize;
@@ -19,8 +20,9 @@ use tracing::Level;
 
 use crate::decls::Decls;
 
-pub use self::env::Env;
+pub use self::env::{Bias, Env};
 use self::prove_wc_list::prove_wc_list;
+pub use negation::{is_definitely_not_proveable, may_not_be_provable, negation_via_failure};
 
 /// Top-level entry point for proving things; other rules recurse to this one.
 pub fn prove(

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

@@ -30,13 +30,6 @@ impl Constraints {
         Self::from(env, v)
     }
 
-    pub fn with_coherence_mode(self, b: bool) -> Self {
-        Self {
-            env: self.env.with_coherence_mode(b),
-            ..self
-        }
-    }
-
     pub fn unconditionally_true(&self) -> bool {
         self.known_true && self.substitution.is_empty()
     }

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

@@ -7,26 +7,56 @@ use formality_types::{
     rust::{Fold, Visit},
 };
 
+/// Whether the solver has to be sound or complete. While it should
+/// ideally be both at all times, we have some rules which break these
+/// properties, so we have to make sure they are only used while in
+/// the proper `Env`. Regardless of the current bias, it's always valid
+/// to return an ambiguous result.
+#[derive(Default, Debug, Clone, Copy, Hash, Ord, Eq, PartialEq, PartialOrd)]
+pub enum Bias {
+    /// Whenever we're able to prove something, it has to definitely be
+    /// *truly true*. We must never be able to prove somethingwhich is not
+    /// *truly true*. This is the default unless we're currently trying to
+    /// prove the negation via "negation as failure".
+    ///
+    /// By convention, functions which may only be used with a bias
+    /// for soundness are called `fn is_X` or `fn is_definitely_X`.
+    #[default]
+    Soundness,
+    /// If we are unable to find a solution for some goal, this goal must
+    /// definitely not be proveable, it is known to not be *truly true*. This
+    /// implies that we must only add constraints if they are definitely
+    /// necessary as we can otherwise use these constraints to incorrectly
+    /// disprove something.
+    ///
+    /// Most notably, this is used by coherence checking to make sure that impls
+    /// definitely do not overlap.
+    ///
+    /// By convention, functions which may only be used with a bias for
+    /// completeness are called `fn may_X`.
+    Completeness,
+}
+
 #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)]
 pub struct Env {
     variables: Vec<Variable>,
-    coherence_mode: bool,
+    bias: Bias,
 }
 
 impl Env {
+    pub fn new_with_bias(bias: Bias) -> Self {
+        Env {
+            variables: Default::default(),
+            bias,
+        }
+    }
+
     pub fn only_universal_variables(&self) -> bool {
         self.variables.iter().all(|v| v.is_universal())
     }
 
-    pub fn is_in_coherence_mode(&self) -> bool {
-        self.coherence_mode
-    }
-
-    pub fn with_coherence_mode(&self, b: bool) -> Env {
-        Env {
-            coherence_mode: b,
-            ..self.clone()
-        }
+    pub fn bias(&self) -> Bias {
+        self.bias
     }
 }
 
@@ -75,6 +105,13 @@ impl Env {
         v
     }
 
+    pub fn fresh_universal(&mut self, kind: ParameterKind) -> UniversalVar {
+        let var_index = self.fresh_index();
+        let v = UniversalVar { kind, var_index };
+        self.variables.push(v.upcast());
+        v
+    }
+
     pub fn insert_fresh_before(&mut self, kind: ParameterKind, rank: Universe) -> ExistentialVar {
         let var_index = self.fresh_index();
         let v = ExistentialVar { kind, var_index };
@@ -208,7 +245,7 @@ impl Env {
                 .iter()
                 .map(|&v| vs.map_var(v).unwrap_or(v))
                 .collect(),
-            coherence_mode: self.coherence_mode,
+            bias: self.bias,
         }
     }