From 525e05b5d3917f1eec1419210ec6a15411e0de5f Mon Sep 17 00:00:00 2001
From: Muneeb Sheikh <muneikh@gmail.com>
Date: Sun, 11 Oct 2026 15:00:26 -0400
Subject: [PATCH] Show both types when theorem statements differ

---
 .github/workflows/lean_action_ci.yml |  4 ++
 Comparator/Compare.lean              |  6 ++-
 tests/StatementDiagnostics.lean      | 80 ++++++++++++++++++++++++++++
 3 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 tests/StatementDiagnostics.lean

diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index b863382..aedff34 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -49,6 +49,10 @@ jobs:
         working-directory: lean4export
         run: lake build
 
+      - name: Check statement mismatch diagnostics
+        working-directory: comparator
+        run: lake env lean tests/StatementDiagnostics.lean
+
       - name: Run comparator tests
         working-directory: comparator
         run: |
diff --git a/Comparator/Compare.lean b/Comparator/Compare.lean
index 8bf6363..8b04fb6 100644
--- a/Comparator/Compare.lean
+++ b/Comparator/Compare.lean
@@ -82,7 +82,11 @@ def compareAt (challenge solution : Export.ExportedEnv) (theoremTargets : Array
       | _, _ => throw s!"Challenge and solution constant kind don't match: '{target}'"
 
     if challengeConst != solutionConst then
-      throw s!"Challenge and solution theorem statement do not match: '{target}'"
+      throw <| s!"Challenge and solution theorem statement do not match: '{target}'\n"
+        ++ s!"Challenge type: {challengeConst.type}\n"
+        ++ s!"Challenge universe parameters: {challengeConst.levelParams}\n"
+        ++ s!"Solution type: {solutionConst.type}\n"
+        ++ s!"Solution universe parameters: {solutionConst.levelParams}"
 
     worklist := worklist ++ challengeConst.type.getUsedConstants
 
diff --git a/tests/StatementDiagnostics.lean b/tests/StatementDiagnostics.lean
new file mode 100644
index 0000000..d21a3c9
--- /dev/null
+++ b/tests/StatementDiagnostics.lean
@@ -0,0 +1,80 @@
+import Comparator.Compare
+
+open Lean Comparator
+
+private def target : Name := `testTheorem
+
+-- These in-memory exports exercise comparison without installing declarations
+-- into a Lean environment or asking a pretty printer to elaborate them.
+private def mkTheoremInfo (type : Expr) (levelParams : List Name := []) : ConstantInfo :=
+  .thmInfo { name := target, levelParams, type, value := .bvar 0 }
+
+private def mkAxiomInfo (type : Expr) : ConstantInfo :=
+  .axiomInfo { name := target, levelParams := [], type, isUnsafe := false }
+
+private def exported (info : ConstantInfo) : Export.ExportedEnv :=
+  { constMap := ({} : Std.HashMap Name ConstantInfo).insert target info, constOrder := #[target] }
+
+private def compare (challenge solution : ConstantInfo) : Except String Unit :=
+  compareAt (exported challenge) (exported solution) #[target] #[] #[]
+
+private def expectMismatch (result : Except String Unit) (details : Array String) : IO Unit := do
+  let .error message := result
+    | throw <| IO.userError "Expected statement mismatch"
+  let expectedPrefix := s!"Challenge and solution theorem statement do not match: '{target}'"
+  unless message.startsWith expectedPrefix do
+    throw <| IO.userError s!"Missing mismatch prefix in: {message}"
+  for detail in details do
+    unless message.splitOn "\n" |>.contains detail do
+      throw <| IO.userError s!"Missing diagnostic '{detail}' in: {message}"
+
+private def expectError (result : Except String Unit) (expected : String) : IO Unit := do
+  let .error message := result
+    | throw <| IO.userError "Expected comparison error"
+  unless message == expected do
+    throw <| IO.userError s!"Expected '{expected}', got '{message}'"
+
+private def expectAccepted (result : Except String Unit) : IO Unit := do
+  match result with
+  | .ok () => pure ()
+  | .error message => throw <| IO.userError s!"Expected acceptance, got '{message}'"
+
+private def tests : Array (String × IO Unit) := #[
+  ("theorem type mismatch", expectMismatch
+    (compare (mkTheoremInfo <| mkConst `Nat) (mkTheoremInfo <| mkConst `Int))
+    #["Challenge type: Nat", "Solution type: Int",
+      "Challenge universe parameters: []", "Solution universe parameters: []"]),
+  ("axiom type mismatch", expectMismatch
+    (compare (mkAxiomInfo <| mkConst `Bool) (mkAxiomInfo <| mkConst `Nat))
+    #["Challenge type: Bool", "Solution type: Nat"]),
+  ("universe parameter mismatch with identical types", expectMismatch
+    (compare (mkTheoremInfo (.sort <| .param `u) [`u])
+      (mkTheoremInfo (.sort <| .param `u) [`v]))
+    #["Challenge type: Sort.{u}", "Solution type: Sort.{u}",
+      "Challenge universe parameters: [u]", "Solution universe parameters: [v]"]),
+  ("matching theorem", expectAccepted <|
+    compare (mkTheoremInfo <| .sort .zero) (mkTheoremInfo <| .sort .zero)),
+  ("matching axiom", expectAccepted <|
+    compare (mkAxiomInfo <| .sort .zero) (mkAxiomInfo <| .sort .zero)),
+  ("missing challenge target", expectError
+    (compareAt default (exported <| mkTheoremInfo <| .sort .zero) #[target] #[] #[])
+    s!"Const not found in challenge: '{target}'"),
+  ("missing solution target", expectError
+    (compareAt (exported <| mkTheoremInfo <| .sort .zero) default #[target] #[] #[])
+    s!"Const not found in solution: '{target}'"),
+  ("different constant kinds", expectError
+    (compare (mkTheoremInfo <| .sort .zero) (mkAxiomInfo <| .sort .zero))
+    s!"Challenge and solution constant kind don't match: '{target}'")
+]
+
+#eval do
+  let mut failed := 0
+  for (name, test) in tests do
+    try
+      test
+      IO.println s!"PASS: {name}"
+    catch error =>
+      failed := failed + 1
+      IO.println s!"FAIL: {name}: {error}"
+  unless failed == 0 do
+    throw <| IO.userError s!"{failed} statement diagnostic regressions failed"