fix(#559): implement + wire trait coherence checking

Trait.check_coherence was a no-op stub ("TODO: Check for overlapping
impls") and was never called, so two impls of the same trait for the same
(or unifiable) self type were silently accepted and method resolution
picked whichever impl came first — an unsoundness.

- Implement check_coherence: two impls overlap iff their self types unify
  after each is instantiated with fresh vars for its own type params (reuses
  fresh_impl_self_ty + Unify.unify; the existing OverlappingImpl error).
- Add check_all_coherence over every registered trait.
- Wire it into Typecheck.check_program after the forward pass registers all
  impls; surface via a new, clearly-named TraitCoherenceError type_error.
- Tests (E2E Trait Coherence #559): duplicate concrete impl → rejected;
  impls for distinct types → accepted; distinct generic args
  (Pair[Int,Bool] vs Pair[Bool,Int]) → accepted (no over-reject).

Known follow-up (documented in-test): generic-subsumption overlap
(impl[T] for Box[T] vs impl for Box[Int]) is not yet detected — it rides on
generic-impl handling that has separate pre-existing immaturities; the
soundness hole #559 named (silent acceptance of overlapping concrete impls)
is closed. 525 tests green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

lib/trait.ml

@@ -420,22 +420,56 @@ let find_method_for_type (registry : trait_registry) (self_ty : ty) (method_name
   in
   search_impls impls
 
-(** Check for overlapping implementations *)
+(** Check for overlapping implementations of [trait_name] (#559).
+
+    Two impls overlap when some type could satisfy BOTH — i.e. their self
+    types unify after each is instantiated with fresh unification variables
+    for its own type parameters.  Overlap makes method resolution ambiguous
+    ([find_impl] would return whichever impl happens to come first), so it is
+    a coherence violation and must be rejected.
+
+    Each candidate is given a freshly-instantiated self type via
+    {!fresh_impl_self_ty} so that one impl's generic parameters cannot leak
+    into another; the unification side-effects land only on those fresh
+    variables, which are discarded with each pair.  Concrete (parameter-free)
+    self types carry no unification variables, so unifying them never mutates
+    the registry's stored types. *)
 let check_coherence (registry : trait_registry) (trait_name : string) : unit result =
   match Hashtbl.find_opt registry.impls trait_name with
   | None -> Ok ()
   | Some impls ->
-    (* TODO: Check for overlapping impls *)
-    (* For now, just ensure no duplicate self types *)
+    let fresh_var () =
+      let id = !Types.next_tyvar in
+      Types.next_tyvar := id + 1;
+      TVar (ref (Unbound (id, 0)))
+    in
     let rec check_pairs = function
       | [] -> Ok ()
-      | _impl :: rest ->
-        (* Check if any impl in rest has same self_ty *)
-        (* TODO: Proper unification check *)
-        check_pairs rest
+      | impl :: rest ->
+        let rec check_against = function
+          | [] -> Ok ()
+          | other :: more ->
+            let s1 = fresh_impl_self_ty impl fresh_var in
+            let s2 = fresh_impl_self_ty other fresh_var in
+            (match Unify.unify s1 s2 with
+             | Ok () -> Error (OverlappingImpl (trait_name, impl.ti_self_ty))
+             | Error _ -> check_against more)
+        in
+        (match check_against rest with
+         | Ok () -> check_pairs rest
+         | err -> err)
     in
     check_pairs impls
 
+(** Run {!check_coherence} for every trait that has registered impls (#559).
+    Returns the first overlap found, if any. *)
+let check_all_coherence (registry : trait_registry) : unit result =
+  Hashtbl.fold (fun trait_name _impls acc ->
+    match acc with
+    | Error _ -> acc
+    | Ok () -> check_coherence registry trait_name
+  ) registry.impls (Ok ())
+
 (** Standard library traits - automatically registered *)
 let register_stdlib_traits (registry : trait_registry) : unit =
   (* Eq trait *)

lib/typecheck.ml

@@ -123,6 +123,10 @@ type type_error =
       (** `break` / `continue` used outside any enclosing loop body
           (issue #459). The string carries the keyword name for the
           error message. *)
+  | TraitCoherenceError of string
+      (** Two impls of the same trait have overlapping (unifiable) self
+          types, so method resolution would be ambiguous (#559). The string
+          is the human-readable overlap description. *)
 
 (* Known exports of stdlib/prelude.affine. Mirrors the same list in
    lib/face.ml — when an UnboundVariable fires at type-check time with
@@ -198,6 +202,12 @@ let show_type_error = function
       "`%s` used outside a loop body (#459). `break` and `continue` must be \
        lexically enclosed by a `while` or `for` loop."
       kw
+  | TraitCoherenceError msg ->
+    Printf.sprintf
+      "Trait coherence violation (#559): %s. Two implementations whose self \
+       types can unify would make method resolution ambiguous; remove or \
+       narrow one of the overlapping impls."
+      msg
 
 let format_type_error = show_type_error
 
@@ -2438,6 +2448,13 @@ let check_program ?(import_types : (string, scheme) Hashtbl.t option)
       Ok ()
     | _ -> Ok ()
   ) (Ok ()) prog.prog_decls in
+  (* #559: trait coherence — now that every impl is registered, reject
+     overlapping impls of the same trait (self types that unify). Done before
+     the check pass so an ambiguous instance base is reported up front. *)
+  let* () = match Trait.check_all_coherence ctx.trait_registry with
+    | Ok () -> Ok ()
+    | Error re -> Error (TraitCoherenceError (Trait.show_resolution_error re))
+  in
   (* Check pass: verify all declarations *)
   let result = List.fold_left (fun acc decl ->
     let* () = acc in

test/test_e2e.ml

@@ -2315,6 +2315,91 @@ let handler_fence_tests = [
   Alcotest.test_case "c: handle → loud failure"                   `Quick test_handle_c_loud_fail;
 ]
 
+(* ============================================================================
+   Issue #559: trait coherence — overlapping impls must be rejected
+   ============================================================================
+
+   `Trait.check_coherence` was a no-op stub (TODO) and unwired, so two impls of
+   the same trait for the same (or unifiable) self type were silently accepted
+   and method resolution picked whichever impl came first. `check_all_coherence`
+   now runs in `check_program` after every impl is registered and rejects any
+   pair of impls whose self types unify. *)
+
+let tc_source src =
+  let prog = Parse_driver.parse_string ~file:"<test>" src in
+  match resolve_program prog with
+  | Error msg -> Error msg
+  | Ok (ctx, _) ->
+    (match Typecheck.check_program ctx.symbols prog with
+     | Ok _ -> Ok ()
+     | Error e -> Error (Typecheck.format_type_error e))
+
+let test_coherence_duplicate_rejected () =
+  let src = {|
+trait Greet { fn greet() -> Int; }
+struct Person { age: Int }
+impl Greet for Person { fn greet() -> Int = 1; }
+impl Greet for Person { fn greet() -> Int = 2; }
+fn main() -> Int = 0;
+|} in
+  match tc_source src with
+  | Ok () ->
+      Alcotest.fail "#559: two impls of Greet for Person must be rejected as \
+                     overlapping; the checker accepted them"
+  | Error msg ->
+      Alcotest.(check bool) "error names trait coherence" true
+        (contains_str "coherence" msg)
+
+let test_coherence_distinct_types_ok () =
+  let src = {|
+trait Greet { fn greet() -> Int; }
+struct Person { age: Int }
+struct Robot { id: Int }
+impl Greet for Person { fn greet() -> Int = 1; }
+impl Greet for Robot { fn greet() -> Int = 2; }
+fn main() -> Int = 0;
+|} in
+  match tc_source src with
+  | Ok () -> ()
+  | Error msg ->
+      Alcotest.failf "#559: impls of Greet for two DISTINCT types must be \
+                      accepted (no overlap), got error: %s" msg
+
+let test_coherence_distinct_generic_args_ok () =
+  (* Coherence must not over-reject: impls for the SAME generic head but
+     distinct concrete args (`Pair[Int,Bool]` vs `Pair[Bool,Int]`) do not
+     overlap and must both be accepted. *)
+  let src = {|
+trait Greet { fn greet() -> Int; }
+enum Pair[A, B] { Mk(A, B) }
+impl Greet for Pair[Int, Bool] { fn greet() -> Int = 1; }
+impl Greet for Pair[Bool, Int] { fn greet() -> Int = 2; }
+fn main() -> Int = 0;
+|} in
+  match tc_source src with
+  | Ok () -> ()
+  | Error msg ->
+      Alcotest.failf "#559: impls for Pair[Int,Bool] vs Pair[Bool,Int] do not \
+                      overlap and must be accepted, got error: %s" msg
+
+(* KNOWN LIMITATION (#559): generic-subsumption overlap — a blanket/generic
+   impl `impl[T] Greet for Box[T]` overlapping a specific `impl Greet for
+   Box[Int]` — is NOT yet detected. The coherence check itself instantiates
+   impl type params and would catch it, but generic *impl* handling has its
+   own separate immaturities (e.g. `impl[T] ... for Box[T]` currently trips a
+   spurious "Trait not found" before coherence runs), so this case rides on a
+   prerequisite that is not yet solid. The soundness-critical hole #559 named
+   — silently accepting overlapping *concrete* impls — IS fixed and covered by
+   the rejected/accepted tests above. Generic-subsumption coherence is tracked
+   as follow-up, not pinned here as an executable accept (it would mis-document
+   a moving target). *)
+
+let coherence_tests = [
+  Alcotest.test_case "duplicate impl (same self type) → rejected"    `Quick test_coherence_duplicate_rejected;
+  Alcotest.test_case "impls for distinct types → accepted"           `Quick test_coherence_distinct_types_ok;
+  Alcotest.test_case "distinct generic args → accepted (no over-reject)" `Quick test_coherence_distinct_generic_args_ok;
+]
+
 (* ============================================================================
    Issue #556: async CPS table-miss loud-fail fence
    ============================================================================
@@ -5652,6 +5737,7 @@ let tests =
     ("E2E Handler Fence (#555)", handler_fence_tests);
     ("E2E Async Fence (#556)", async_fence_tests);
     ("E2E Resume Soundness (#555)", resume_soundness_tests);
+    ("E2E Trait Coherence (#559)", coherence_tests);
     ("E2E Ownership Verify", tw_verify_tests);
     ("E2E Cmd Linearity", cmd_linear_tests);
     ("E2E Boundary Verify", tw_interface_tests);