class FunLike (F : Sort _) (β : outParam <| Nat → Sort _) where
  coe : F → ∀ a, β a

inductive Secret
def Wrapper := Secret
inductive Bla | z
instance : FunLike Bla (fun _ => Wrapper) := sorry

instance (priority := 100) {F β} [FunLike F β] :
  CoeFun F fun _ => ∀ a : Nat, β a where coe := FunLike.coe

#check Bla.z 0 -- FunLike.coe Bla.z 0 : (fun x => Wrapper) 0
#check Bla.z ∘ id -- FunLike.coe Bla.z ∘ id : Nat → Secret

This shows two different but possibly related issues:

1. The first #check results in a term whose type is a beta redex. Most likely there is a missing headBeta.
2. The second #check is the real issue: even though ↑Bla.z : Nat → Wrapper and there are no hard unification problems in the way, the inferred type of ↑Bla.z ∘ id is Nat → Secret, which can cause a failure later if Secret and Wrapper have different typeclasses on them.

Reported by @semorrison on Zulip.