additional test

src/Lean/Elab/App.lean

@@ -1357,7 +1357,7 @@ private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) :
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  /-- A weak version of forallTelescopeReducing that only uses whnfCore. -/
+  /-- A weak version of forallTelescopeReducing that only uses whnfCore, to avoid unfolding definitions except by `unfoldDefinition?` below. -/
   withForallBody {α} (type : Expr) (k : Expr → TermElabM α) : TermElabM α :=
     forallTelescope type fun _ body => do
       let body ← whnfCore body

tests/lean/run/4761.lean

@@ -6,3 +6,12 @@ def Foo : Prop := ∀ a : Nat, a = a
 
 protected theorem Foo.intro : Foo := sorry
 example : Foo := .intro
+
+/-!
+Making sure that the type synonym `Foo'` still works.
+This used to be unfolded during `forallTelescopeReducing`,
+and now it is "manually" unfolded in the elaboration algorithm.
+-/
+example : Nat → Option Nat := .some
+def Foo' := Nat → Option Nat
+example : Foo' := .some