first coherence tests -- neat!

Author: nikomatsakis

crates/formality-check/src/coherence.rs

@@ -1,6 +1,10 @@
 use anyhow::bail;
+use formality_prove::Env;
 use formality_rust::grammar::{Crate, TraitImpl};
-use formality_types::{cast::Downcasted, grammar::Fallible};
+use formality_types::{
+    cast::Downcasted,
+    grammar::{Fallible, Wcs},
+};
 use itertools::Itertools;
 
 use crate::Check;
@@ -38,7 +42,24 @@ impl Check<'_> {
         Ok(())
     }
 
-    fn overlap_check(&self, _impl_a: &TraitImpl, _impl_b: &TraitImpl) -> Fallible<()> {
-        Ok(())
+    fn overlap_check(&self, impl_a: &TraitImpl, impl_b: &TraitImpl) -> Fallible<()> {
+        let mut env = Env::default();
+
+        let a = env.instantiate_universally(&impl_a.binder);
+        let b = env.instantiate_universally(&impl_b.binder);
+
+        let trait_ref_a = a.trait_ref();
+        let trait_ref_b = b.trait_ref();
+
+        // If the parameters from the two impls cannot be equal, then they do not overlap.
+        if let Ok(()) = self.prove_not_goal(
+            &env,
+            (&a.where_clauses, &b.where_clauses),
+            Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+        ) {
+            return Ok(());
+        }
+
+        bail!("impls may overlap: `{impl_a:?}` vs `{impl_b:?}`")
     }
 }

crates/formality-check/src/lib.rs

@@ -10,7 +10,7 @@ use formality_rust::{
 };
 use formality_types::{
     cast::Upcast,
-    grammar::{Fallible, Wcs},
+    grammar::{Fallible, Substitution, Wcs},
 };
 
 /// Check all crates in the program. The crates must be in dependency order
@@ -107,4 +107,45 @@ impl Check<'_> {
 
         bail!("failed to prove {goal:?} given {assumptions:?}, got {cs:?}")
     }
+
+    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();
+
+        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();
+        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,
+        );
+
+        if cs.is_empty() {
+            return Ok(());
+        }
+
+        bail!("failed to disprove {goal:?} given {assumptions:?}, got {cs:?}")
+    }
 }

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

@@ -5,8 +5,7 @@ use formality_types::{
     collections::Set,
     fold::Fold,
     grammar::{
-        Binder, InferenceVar, ParameterKind, PlaceholderVar, VarIndex, VarSubstitution,
-        Variable,
+        Binder, InferenceVar, ParameterKind, PlaceholderVar, VarIndex, VarSubstitution, Variable,
     },
     visit::Visit,
 };
@@ -18,11 +17,7 @@ pub struct Env {
 
 impl Env {
     pub fn only_universal_variables(&self) -> bool {
-        self.variables.iter().all(|v| match v {
-            Variable::PlaceholderVar(_) => true,
-            Variable::InferenceVar(_) => false,
-            Variable::BoundVar(_) => false,
-        })
+        self.variables.iter().all(|v| v.is_universal())
     }
 }
 
@@ -64,6 +59,13 @@ impl Env {
         }
     }
 
+    pub fn fresh_existential(&mut self, kind: ParameterKind) -> InferenceVar {
+        let var_index = self.fresh_index();
+        let v = InferenceVar { kind, var_index };
+        self.variables.push(v.upcast());
+        v
+    }
+
     pub fn insert_fresh_before(&mut self, kind: ParameterKind, rank: Universe) -> InferenceVar {
         let var_index = self.fresh_index();
         let v = InferenceVar { kind, var_index };

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

@@ -2,8 +2,8 @@ use formality_types::{
     cast::{Downcast, Upcast, Upcasted},
     collections::{Deduplicate, Set},
     grammar::{
-        AliasTy, InferenceVar, Parameter, PlaceholderVar, Relation, RigidTy, Substitution,
-        TyData, Variable, Wcs,
+        AliasTy, InferenceVar, Parameter, PlaceholderVar, Relation, RigidTy, Substitution, TyData,
+        Variable, Wcs,
     },
     judgment_fn, set,
     visit::Visit,
@@ -18,18 +18,6 @@ use crate::{
 
 use super::{constraints::Constraints, env::Env};
 
-/// Goal(s) to prove `a` and `b` are equal (they must have equal length)
-pub fn all_eq(a: impl Upcast<Vec<Parameter>>, b: impl Upcast<Vec<Parameter>>) -> Wcs {
-    let a: Vec<Parameter> = a.upcast();
-    let b: Vec<Parameter> = b.upcast();
-    assert_eq!(a.len(), b.len());
-    a.into_iter()
-        .zip(b)
-        .map(|(a, b)| Relation::eq(a, b))
-        .upcasted()
-        .collect()
-}
-
 /// Goal(s) to prove `a` and `b` are equal
 pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {
     Relation::eq(a, b)
@@ -59,7 +47,7 @@ judgment_fn! {
             (let RigidTy { name: a_name, parameters: a_parameters } = a)
             (let RigidTy { name: b_name, parameters: b_parameters } = b)
             (if a_name == b_name)
-            (prove(decls, env, assumptions, all_eq(a_parameters, b_parameters)) => c)
+            (prove(decls, env, assumptions, Wcs::all_eq(a_parameters, b_parameters)) => c)
             ----------------------------- ("rigid")
             (prove_eq(decls, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c)
         )
@@ -68,7 +56,7 @@ judgment_fn! {
             (let AliasTy { name: a_name, parameters: a_parameters } = a)
             (let AliasTy { name: b_name, parameters: b_parameters } = b)
             (if a_name == b_name)
-            (prove(decls, env, assumptions, all_eq(a_parameters, b_parameters)) => env_c)
+            (prove(decls, env, assumptions, Wcs::all_eq(a_parameters, b_parameters)) => env_c)
             ----------------------------- ("alias")
             (prove_eq(decls, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => env_c)
         )

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

@@ -9,11 +9,7 @@ use formality_types::{
 use crate::{
     decls::{AliasEqDeclBoundData, Decls},
     prove::{
-        env::Env,
-        prove,
-        prove_after::prove_after,
-        prove_eq::{all_eq, prove_existential_var_eq},
-        zip::zip,
+        env::Env, prove, prove_after::prove_after, prove_eq::prove_existential_var_eq, zip::zip,
     },
 };
 
@@ -41,7 +37,7 @@ judgment_fn! {
             (let decl = decl.binder.instantiate_with(&subst).unwrap())
             (let AliasEqDeclBoundData { alias: AliasTy { name, parameters }, ty, where_clause } = decl)
             (assert a.name == name)
-            (prove(&decls, env, &assumptions, all_eq(&a.parameters, &parameters)) => c)
+            (prove(&decls, env, &assumptions, Wcs::all_eq(&a.parameters, &parameters)) => c)
             (prove_after(&decls, c, &assumptions, &where_clause) => c)
             (let ty = c.substitution().apply(&ty))
             (let c = c.pop_subst(&subst))

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

@@ -6,7 +6,7 @@ use formality_types::{
 use crate::{
     decls::Decls,
     prove::{
-        constraints::Constraints, env::Env, prove, prove_after::prove_after, prove_eq::all_eq,
+        constraints::Constraints, env::Env, prove, prove_after::prove_after, 
     },
 };
 
@@ -24,7 +24,7 @@ judgment_fn! {
             (let (skel_c, parameters_c) = predicate.debone())
             (let (skel_g, parameters_g) = goal.debone())
             (if skel_c == skel_g)
-            (prove(decls, env, assumptions, all_eq(parameters_c, parameters_g)) => c)
+            (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c)
             ----------------------------- ("predicate-congruence-axiom")
             (prove_via(decls, env, assumptions, PR::Predicate(predicate), goal) => c)
         )

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

@@ -5,13 +5,7 @@ use formality_types::{
 
 use crate::{
     decls::Decls,
-    prove::{
-        env::Env,
-        prove,
-        prove_after::prove_after,
-        prove_eq::{all_eq, prove_eq},
-        prove_via::prove_via,
-    },
+    prove::{env::Env, prove, prove_after::prove_after, prove_eq::prove_eq, prove_via::prove_via},
 };
 
 use super::constraints::Constraints;
@@ -52,7 +46,7 @@ judgment_fn! {
             (let i = i.binder.instantiate_with(&subst).unwrap())
             (let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
             (let co_assumptions = (&assumptions, &trait_ref))
-            (prove(&decls, env, &co_assumptions, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
+            (prove(&decls, env, &co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
             (prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
             (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
             ----------------------------- ("impl")

crates/formality-rust/src/grammar.rs

@@ -5,7 +5,7 @@ use formality_types::{
     cast::Upcast,
     grammar::{
         AdtId, AssociatedItemId, Binder, CrateId, Fallible, FieldId, FnId, Lt, Parameter, TraitId,
-        Ty,
+        TraitRef, Ty,
     },
     term::Term,
 };
@@ -254,6 +254,12 @@ pub struct TraitImplBoundData {
     pub impl_items: Vec<ImplItem>,
 }
 
+impl TraitImplBoundData {
+    pub fn trait_ref(&self) -> TraitRef {
+        self.trait_id.with(&self.self_ty, &self.trait_parameters)
+    }
+}
+
 #[term]
 pub enum ImplItem {
     #[cast]

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

@@ -4,9 +4,6 @@ use crate::cast::To;
 use crate::cast::Upcast;
 use crate::cast_impl;
 
-use super::AdtId;
-use super::AliasName;
-use super::AliasTy;
 use super::Parameter;
 use super::Parameters;
 use super::TraitId;

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

@@ -486,6 +486,14 @@ impl Variable {
             }) => false,
         }
     }
+
+    pub fn is_universal(&self) -> bool {
+        match self {
+            Variable::PlaceholderVar(_) => true,
+            Variable::InferenceVar(_) => false,
+            Variable::BoundVar(_) => false,
+        }
+    }
 }
 
 impl Visit for Variable {