Progress

Author: nomeata

src/Lean/Meta/Match/MatchEqs.lean

@@ -409,6 +409,7 @@ def genMatchCongrEqnsImpl (matchDeclName : Name) : MetaM (Array Name) := do
   realizeConst matchDeclName firstEqnName (go baseName)
   return matchCongrEqnsExt.getState (asyncMode := .async .asyncEnv) (asyncDecl := firstEqnName) (← getEnv) |>.find! matchDeclName
 where go baseName :=
+  withoutExporting do
   withConfig (fun c => { c with etaStruct := .none }) do
   trace[Meta.Match.matchEqs] "genMatchCongrEqnsImpl on {matchDeclName}"
   let constInfo ← getConstInfo matchDeclName

tests/lean/run/issue2237.lean

@@ -20,16 +20,46 @@ abbrev plus : Term Γ a → Term Γ a
 
 /--
 error: failed to generate equational theorem for `plus`
-  failed to generate equality theorems for `match` expression `plus.match_1`
-  Γ✝ : Context
-  a✝ : Ty
-  motive✝ : Term Γ✝ a✝ → Sort u_1
-  n✝ : Term ( ✶ :: Γ✝) ✶
-  h_1✝ : (i : Lookup Γ✝ a✝) → motive✝ (Term.var i)
-  h_2✝ : (n : Term ( ✶ :: Γ✝) ✶ ) → motive✝ n.lam
-  h_3✝ : (a : Term ( ✶ :: Γ✝) ✶ ) → (m : Term Γ✝ ✶ ) → motive✝ (a.lam.ap m)
-  h_4✝ : (l m : Term Γ✝ ✶ ) → motive✝ (l.ap m)
-  ⊢ (⋯ ▸ fun x motive h_1 h_2 h_3 h_4 h => ⋯ ▸ h_2 n✝) n✝.lam motive✝ h_1✝ h_2✝ h_3✝ h_4✝ ⋯ = h_2✝ n✝
+  Application type mismatch: The argument
+    l.ap m
+  has type
+    Term Γ ✶
+  but is expected to have type
+    Term Γ a
+  in the application
+    @HEq (Term Γ a) (l.ap m)
 -/
 #guard_msgs in
 #print equations plus
+
+
+/--
+error: Failed to realize constant plus.match_1.eq_1:
+  Application type mismatch: The argument
+    l.ap m
+  has type
+    Term Γ ✶
+  but is expected to have type
+    Term Γ a
+  in the application
+    @HEq (Term Γ a) (l.ap m)
+---
+error: Unknown constant `plus.match_1.eq_1`
+-/
+#guard_msgs in #print sig plus.match_1.eq_1
+
+/--
+error: Failed to realize constant plus.match_1.congr_eq_1:
+  Tactic `subst` failed: did not find equation for eliminating 'heq✝'
+  ⏎
+  Γ : Context
+  a : Ty
+  x✝ : Term Γ a
+  l m : Term Γ ✶
+  heq✝ : x✝ ≍ l.ap m
+  ⊢ (∀ (a_1 : Term ( ✶ :: Γ) ✶ ) (m_1 : Term Γ ✶ ), l.ap m ≍ a_1.lam.ap m_1 → False) →
+      ∀ (a_1 : Term ( ✶ :: Γ) ✶ ) (m : Term Γ ✶ ), x✝ ≍ a_1.lam.ap m → False
+---
+error: Unknown constant `plus.match_1.congr_eq_1`
+-/
+#guard_msgs in #print sig plus.match_1.congr_eq_1