From 32db3161666325b704ef9d4876f9ee9718e03bb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jun 2022 17:57:16 -0700
Subject: [PATCH] fix: enumeration type `noConfusion` was not registered

This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.28kernel.29.20function.20expected.20.2EnoConfusion/near/284634050
---
 src/Lean/Meta/Constructions.lean         |  1 +
 tests/lean/run/enumNoConfusionIssue.lean | 13 +++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 tests/lean/run/enumNoConfusionIssue.lean

diff --git a/src/Lean/Meta/Constructions.lean b/src/Lean/Meta/Constructions.lean
index 5865d4b0b2..ee9ecfcdb7 100644
--- a/src/Lean/Meta/Constructions.lean
+++ b/src/Lean/Meta/Constructions.lean
@@ -114,6 +114,7 @@ where
         hints       := ReducibilityHints.abbrev
       }
       setReducibleAttribute declName
+      modifyEnv fun env => markNoConfusion env declName
 
 def mkNoConfusion (declName : Name) : MetaM Unit := do
   if (← isEnumType declName) then
diff --git a/tests/lean/run/enumNoConfusionIssue.lean b/tests/lean/run/enumNoConfusionIssue.lean
new file mode 100644
index 0000000000..5324dd263c
--- /dev/null
+++ b/tests/lean/run/enumNoConfusionIssue.lean
@@ -0,0 +1,13 @@
+inductive MyBool :=
+  | MyTrue
+  | MyFalse
+
+inductive T :=
+  | mk (b: MyBool) (u: Unit)
+
+inductive isTrue: T → Type :=
+  | intro: isTrue (.mk .MyTrue ())
+
+example {τ: T} (h: isTrue τ): Unit :=
+  match τ, h with
+  | .mk .MyTrue (), .intro => ()