Return type in FunLike.coe not beta reduced

Stream: mathlib4

[Tomas Skrivan]

edit: the question is moot ... I'm not running latest mathlib and this seems to be fixed :)

The return type in FunLike.coe does not seem to be beta reduced. Why is that and can we do something about it? I believe there is some custom elaborator for FunLike/coercion to function, where can I find it?

Example

import Mathlib.Data.FunLike.Basic
variable (x y : ℕ) {F : Type} (f : F) [FunLike F ℕ (fun _ => ℕ)]

set_option pp.all true in
set_option pp.universes false in
#check (f x) -- FunLike.coe F Nat (fun (a : Nat) => (fun (x : Nat) => Nat) a) inst f x : (fun (x : Nat) => Nat) x

The issue is the type (fun (a : Nat) => (fun (x : Nat) => Nat) a) which just beta reduces to fun (x : Nat) => Nat.

I run into this issue when using simp with dsimp:=false

import Mathlib.Data.FunLike.Basic

variable (x y : ℕ) {F : Type} (f : F) [FunLike F ℕ (fun _ => ℕ)]

example : f (id x) = f x :=
by
  conv =>
    lhs
    -- fails to simplify `id`
    simp (config := {dsimp:=false,failIfUnchanged:=false})
    trace_state -- f (id x)
    simp (config := {dsimp:=true})
    trace_state -- f x

[Kyle Miller]

Yep :-) I think it might be this commit: https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20mathlib4.3Amaster/near/402340291