From 9d8b324f8dc9253da362d98220b07b209b8bfd26 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 24 Nov 2022 11:55:45 -0800
Subject: [PATCH] fix: fixes #1869

Better support for simplifying class projections.
---
 src/Lean/Meta/Tactic/Simp/Main.lean | 37 +++++++++++++++++++++--------
 tests/lean/run/1869.lean            | 20 ++++++++++++++++
 2 files changed, 47 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/run/1869.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 90feeaa589..9f33bd8b09 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -82,21 +82,38 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
     match (← getProjectionFnInfo? cinfo.name) with
     | none => return none
     | some projInfo =>
-      if projInfo.fromClass then
-        if (← read).isDeclToUnfold cinfo.name then
-          -- We only unfold class projections when the user explicitly requested them to be unfolded.
-          -- Recall that `unfoldDefinition?` has support for unfolding this kind of projection.
-          withReducibleAndInstances <| unfoldDefinition? e
-        else
-          return none
-      else
-        -- `structure` projection
-        match (← unfoldDefinition? e) with
+      /- Helper function for applying `reduceProj?` to the result of `unfoldDefinition?` -/
+      let reduceProjCont? (e? : Option Expr) : SimpM (Option Expr) := do
+        match e? with
         | none   => pure none
         | some e =>
           match (← reduceProj? e.getAppFn) with
           | some f => return some (mkAppN f e.getAppArgs)
           | none   => return none
+      if projInfo.fromClass then
+        -- `class` projection
+        if (← read).isDeclToUnfold cinfo.name then
+          /-
+          If user requested `class` projection to be unfolded, we set transparency mode to `.instances`,
+          and invoke `unfoldDefinition?`.
+          Recall that `unfoldDefinition?` has support for unfolding this kind of projection when transparency mode is `.instances`.
+          -/
+          withReducibleAndInstances <| unfoldDefinition? e
+        else
+          /-
+          Recall that class projections are **not** marked with `[reducible]` because we want them to be
+          in "reducible canonical form". However, if we have a class projection of the form `Class.projFn (Class.mk ...)`,
+          we want to reduce it. See issue #1869 for an example where this is important.
+          -/
+          unless e.getAppNumArgs > projInfo.numParams do
+            return none
+          let major := e.getArg! projInfo.numParams
+          unless major.isConstructorApp (← getEnv) do
+            return none
+          reduceProjCont? (← withDefault <| unfoldDefinition? e)
+      else
+        -- `structure` projections
+        reduceProjCont? (← unfoldDefinition? e)
 
 private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do
   if cfg.zeta then
diff --git a/tests/lean/run/1869.lean b/tests/lean/run/1869.lean
new file mode 100644
index 0000000000..16153196f5
--- /dev/null
+++ b/tests/lean/run/1869.lean
@@ -0,0 +1,20 @@
+universe v u u'
+
+class CategoryStruct (C : Type u) :=
+  (Hom : C → C → Type v)
+  (id : ∀ X, Hom X X)
+  (comp : ∀ {X Y Z : C}, Hom X Y → Hom Y Z → Hom X Z)
+
+class Category (C : Type u) extends CategoryStruct.{v} C :=
+  (comp_id : ∀ {X Y : C} (f : Hom X Y), comp f (id Y) = f)
+
+open CategoryStruct
+open Category
+
+attribute [simp] comp_id
+
+instance (C : Type u) [Category.{v} C] : Category.{v} (ULift.{u'} C) where
+  Hom := λ X Y => Hom X.down Y.down
+  id := λ X => id X.down
+  comp := λ f g => comp f g
+  comp_id := λ f => by simp