fix: fixes #620

src/Lean/Meta/Reduce.lean

@@ -32,9 +32,10 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
             else
               args ← args.modifyM i visit
           pure (mkAppN f args)
-        | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
-        | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
-        | _               => return e
+        | Expr.lam ..        => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
+        | Expr.forallE ..    => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
+        | Expr.proj n i s .. => return mkProj n i (← visit s)
+        | _                  => return e
   visit e |>.run
 
 end Lean.Meta

tests/lean/620.lean

@@ -0,0 +1,7 @@
+structure Foo (α : Type) where foo : α
+class Bar (α β : Type) where coe : α → β
+
+variable {α : Type} (x : Foo (Foo α))
+
+#reduce @Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x -- x.1
+#reduce (@Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x).1 -- (Coe.coe x).1 instead of x.1.1

tests/lean/620.lean.expected.out

@@ -0,0 +1,2 @@
+x.1
+x.1.1