Merge pull request #122 from nikomatsakis/2023-02-explorations

revamp

Author: nikomatsakis

Cargo.lock

@@ -10,22 +10,21 @@ rustc_private=true
 
 [dev-dependencies]
 pretty_assertions = "1.3.0"
+expect-test = "1.4.0"
 
 [dependencies]
+anyhow = "1"
 clap = { version = "4.0.9", features = ["derive"] }
 formality-rust = { version = "0.1.0", path = "crates/formality-rust" }
 formality-types = { version = "0.1.0", path = "crates/formality-types" }
-formality-core = { version = "0.1.0", path = "crates/formality-core" }
+formality-check = { version = "0.1.0", path = "crates/formality-check" }
 
 [workspace]
 members = [
     "crates/formality-macros",
     "crates/formality-core",
     "crates/formality-types",
-    "crates/formality-decl",
-    "crates/formality-mir",
     "crates/formality-check",
     "crates/formality-rust",
-    "crates/formality-main",
     "crates/formality-prove",
 ]

Cargo.toml

@@ -9,8 +9,8 @@ edition = "2021"
 formality-types = { path = "../formality-types" }
 formality-macros = { path = "../formality-macros" }
 formality-core = { path = "../formality-core" }
-formality-decl = { path = "../formality-decl" }
-formality-mir = { path = "../formality-mir" }
+formality-rust = { path = "../formality-rust" }
+formality-prove = { path = "../formality-prove" }
 tracing = "0.1"
 contracts = "0.6.3"
 anyhow = "1.0.66"

crates/formality-check/Cargo.toml

@@ -1,16 +1,10 @@
-use formality_decl::grammar::{Adt, AdtBoundData, AdtVariant, Field};
-use formality_types::{
-    cast::To,
-    grammar::{Fallible, Hypothesis},
-};
+use formality_prove::Env;
+use formality_rust::grammar::{Adt, AdtBoundData, Field, Variant};
+use formality_types::grammar::Fallible;
 
 impl super::Check<'_> {
     pub(super) fn check_adt(&self, adt: &Adt) -> Fallible<()> {
-        let Adt {
-            kind: _,
-            id: _,
-            binder,
-        } = adt;
+        let Adt { id: _, binder } = adt;
 
         let mut env = Env::default();
 
@@ -19,15 +13,13 @@ impl super::Check<'_> {
             variants,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<Hypothesis> = where_clauses.to();
-
-        self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;
+        self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?;
 
         // FIXME: check names are unique or integers from 0..n
 
-        for AdtVariant { name: _, fields } in &variants {
+        for Variant { name: _, fields } in &variants {
             for Field { name: _, ty } in fields {
-                self.prove_goal(&env, &assumptions, ty.well_formed())?;
+                self.prove_goal(&env, &where_clauses, ty.well_formed())?;
             }
         }
 

crates/formality-check/src/adts.rs

@@ -1,6 +1,10 @@
 use anyhow::bail;
-use formality_decl::grammar::{Crate, TraitImpl};
-use formality_types::{cast::Downcasted, grammar::Fallible};
+use formality_prove::Env;
+use formality_rust::grammar::{Crate, TraitImpl};
+use formality_types::{
+    cast::Downcasted,
+    grammar::{Fallible, Wcs},
+};
 use itertools::Itertools;
 
 use crate::Check;
@@ -38,7 +42,33 @@ 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(());
+        }
+
+        // If we can disprove the where clauses, then they do not overlap.
+        if let Ok(()) = self.prove_not_goal(
+            &env,
+            Wcs::all_eq(&trait_ref_a.parameters, &trait_ref_b.parameters),
+            (&a.where_clauses, &b.where_clauses),
+        ) {
+            return Ok(());
+        }
+
+        bail!("impls may overlap: `{impl_a:?}` vs `{impl_b:?}`")
     }
 }

crates/formality-check/src/coherence.rs

@@ -1,9 +1,6 @@
-use formality_decl::grammar::{Fn, FnBoundData};
-use formality_logic::Env;
-use formality_types::{
-    cast::Upcast,
-    grammar::{Fallible, Hypothesis},
-};
+use formality_prove::Env;
+use formality_rust::grammar::{Fn, FnBoundData, WhereClause};
+use formality_types::{cast::Upcast, grammar::Fallible};
 
 use crate::Check;
 
@@ -15,7 +12,7 @@ impl Check<'_> {
     pub(crate) fn check_fn(
         &self,
         in_env: &Env,
-        in_assumptions: &[Hypothesis],
+        in_assumptions: &[WhereClause],
         f: &Fn,
     ) -> Fallible<()> {
         let mut env = in_env.clone();
@@ -26,9 +23,10 @@ impl Check<'_> {
             input_tys,
             output_ty,
             where_clauses,
+            body: _,
         } = env.instantiate_universally(binder);
 
-        let assumptions: Vec<Hypothesis> = (in_assumptions, &where_clauses).upcast();
+        let assumptions: Vec<WhereClause> = (in_assumptions, &where_clauses).upcast();
 
         self.prove_where_clauses_well_formed(&env, &assumptions, &where_clauses)?;