From 1a7535263e355d51d98883d8575cc05b2cd541b8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Feb 2021 17:54:41 -0800
Subject: [PATCH] fix: unfolding class projections at `simp`

---
 src/Lean/Meta/Tactic/Simp/Main.lean | 10 ++++++++--
 tests/lean/run/simp7.lean           | 27 +++++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 2fc522d14e..b4d3217a93 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -83,7 +83,13 @@ private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do
     return e
 
 private def unfold? (e : Expr) : SimpM (Option Expr) := do
-  if e.getAppFn.isConst && (← read).toUnfold.contains e.getAppFn.constName! then
+  let f := e.getAppFn
+  if !f.isConst then
+    return none
+  let fName := f.constName!
+  if (← isProjectionFn fName) then
+    return none -- should be reduced by `reduceProjFn?`
+  if (← read).toUnfold.contains e.getAppFn.constName! then
     withDefault <| unfoldDefinition? e
   else
     return none
@@ -97,7 +103,7 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   -- TODO: eta reduction
   if cfg.proj then
     match (← reduceProjFn? e) with
-    | some e => return (← reduce e)
+    | some e => trace[Meta.debug]! "reduceProjFn? result {e}"; return (← reduce e)
     | none   => pure ()
   if cfg.iota then
     match (← reduceRecMatcher? e) with
diff --git a/tests/lean/run/simp7.lean b/tests/lean/run/simp7.lean
index c5da87dc76..0557b6c5bf 100644
--- a/tests/lean/run/simp7.lean
+++ b/tests/lean/run/simp7.lean
@@ -37,3 +37,30 @@ def foo := 10
 theorem ex5 (x : Nat) : foo + x = 10 + x := by
   simp [foo]
   done
+
+def g (x : Nat) : Nat := do
+  let x ← pure x
+  return x
+
+theorem ex6 : g x = x := by
+  simp [g, bind, pure]
+
+def f1 : StateM Nat Unit := do
+  modify fun x => g x
+
+def f2 : StateM Nat Unit := do
+  let s ← get
+  set <| g s
+
+theorem ex7 : f1 = f2 := by
+  simp [f1, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, pure, set, StateT.set, modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet]
+
+def h (x : Nat) : Sum (Nat × Nat) Nat := Sum.inl (x, x)
+
+def bla (x : Nat) :=
+  match h x with
+  | Sum.inl (y, z) => y + z
+  | Sum.inr _ => 0
+
+theorem ex8 (x : Nat) : bla x = x + x := by
+  simp [bla, h]