From af52685c7f48caab8be5996a9ffaee27712179ab Mon Sep 17 00:00:00 2001
From: tiif <pekyuan@gmail.com>
Date: Wed, 8 Oct 2025 22:04:26 +0800
Subject: [PATCH] Add documentation

---
 crates/formality-check/src/impls.rs          | 41 ++++++++++++++++++++
 crates/formality-prove/src/prove/prove_eq.rs | 13 +++++++
 crates/formality-types/src/grammar/wc.rs     |  6 +++
 3 files changed, 60 insertions(+)

diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs
index 31f83e89..20b5178b 100644
--- a/crates/formality-check/src/impls.rs
+++ b/crates/formality-check/src/impls.rs
@@ -120,6 +120,44 @@ impl super::Check<'_> {
         }
     }
 
+    /// Check that function `ii_fn` that appears in an impl is valid.
+    /// This includes the core check from [`Self::check_fn`][],
+    /// but also additional checks to ensure that the signature in the impl
+    /// matches what is declared in the trait.
+    ///
+    /// # Example
+    ///
+    /// Suppose we are checking `<Cup<L> as Potable>::drink` in this example...
+    ///
+    /// ```rust,ignore
+    /// trait Potable {
+    ///     fn drink(&self); // `trait_items` includes these fns
+    ///     fn smell(&self); //
+    /// }
+    ///
+    /// struct Water;
+    /// impl Potable for Water {
+    ///     fn drink(&self) {}
+    ///     fn smell(&self) {}
+    /// }
+    ///
+    /// struct Cup<L>;
+    /// impl<L> Potable for Cup<L> // <-- env has `L` in scope
+    /// where
+    ///     L: Potable, // <-- `impl_assumptions`
+    /// {
+    ///     fn drink(&self) {} // <-- `ii_fn`
+    ///     fn smell(&self) {} // not currently being checked
+    /// }
+    /// ```
+    ///
+    /// # Parameters
+    ///
+    /// * `env`, the environment from the impl header
+    /// * `impl_assumptions`, where-clauses declared on the impl
+    /// * `trait_items`, items declared in the trait that is being implemented
+    ///   (we search this to find the corresponding declaration of the method)
+    /// * `ii_fn`, the fn as declared in the impl
     fn check_fn_in_impl(
         &self,
         env: &Env,
@@ -149,12 +187,14 @@ impl super::Check<'_> {
 
         let mut env = env.clone();
         let (
+            // ii_: the signature of the function as found in the impl item (ii)
             FnBoundData {
                 input_tys: ii_input_tys,
                 output_ty: ii_output_ty,
                 where_clauses: ii_where_clauses,
                 body: _,
             },
+            // ti_: the signature of the function as found in the trait item (ti)
             FnBoundData {
                 input_tys: ti_input_tys,
                 output_ty: ti_output_ty,
@@ -169,6 +209,7 @@ impl super::Check<'_> {
             &ii_where_clauses,
         )?;
 
+        // Must have same number of arguments as declared in the trait
         if ii_input_tys.len() != ti_input_tys.len() {
             bail!(
                 "impl has {} function arguments but trait has {} function arguments",
diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs
index 801a9a44..0fab1999 100644
--- a/crates/formality-prove/src/prove/prove_eq.rs
+++ b/crates/formality-prove/src/prove/prove_eq.rs
@@ -64,8 +64,21 @@ judgment_fn! {
             (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c)
         )
 
+        // Example: we are trying to prove `x` (which equals `<SomeX<?V> as Iterator>::Item`)
+        // is equal to some type `z`.
         (
+            // Normalize `x` will find alternative "spellings" that it is equivalent to.
+            // For example, if there is an impl like
+            // `impl Iterator for SomeX<i32> { type Item = u32; ... }`
+            // then `prove_normalize` would yield `(c, u32)` where `c` are any constraints
+            // needed to show that it normalized (in this case, `c` would include the
+            // substitution `?V = i32`).
             (prove_normalize(&decls, env, &assumptions, &x) => (c, y))
+
+            // Now that we know that `x` is equivalent to `y`, we try to prove
+            // that `y` is equivalent to `z` (our original goal).
+            // We do that with `prove_after` so that the constraints `c` are considered
+            // (e.g., if `z` includes `?V`, it will be replaced with `i32`).
             (prove_after(&decls, c, &assumptions, eq(y, &z)) => c)
             ----------------------------- ("normalize-l")
             (prove_eq(decls, env, assumptions, x, z) => c)
diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs
index 97ef0842..17a4fa98 100644
--- a/crates/formality-types/src/grammar/wc.rs
+++ b/crates/formality-types/src/grammar/wc.rs
@@ -148,6 +148,12 @@ pub enum WcData {
     #[grammar(for $v0)]
     ForAll(Binder<Wc>),
 
+    // An *implication* `if $v0 $v1` says "assuming v0 is true, v1 is true".
+    // These are useful to express hypothetical syntax like
+    // `for<'a: 'b, 'b>` or as part of an implied bounds scheme
+    // where you might make the Rust syntax `for<'a, 'b> T: Something<'a, 'b>`
+    // expand to `for<'a, 'b> if ('a: 'b) (T: Something<'a, 'b>)`
+    // (given `trait Something<'a, 'b> where 'a: 'b`).
     #[grammar(if $v0 $v1)]
     Implies(Wcs, Wc),
 }