CoeFun causes types to be unfolded

[digama0]

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.

[gebner]

(1) is expected, the type of FunLike.coe is ∀ β [FunLike F β] a, β a after all. inferType does not do beta-reduction.

[gebner]

(2) is a side-effect of unification, I believe. We need to unify (a : Nat) → (fun _ => Wrapper) a (a dependent forall) with ?m → ?n (a non-dependent forall). As far as I can tell, we do WHNF to see if the rhs of the forall doesn't include the binder.

structure Secret
def Wrapper := Secret
def f (a : Nat) : (fun _ => Wrapper) a := ⟨⟩
#check f ∘ id -- also exposes the Secret

[semorrison]

I think this issue (or something related) is making porting Order.WithBot a real hassle. Option is leaking through everywhere.

[digama0]

(1) is expected, the type of FunLike.coe is ∀ β [FunLike F β] a, β a after all. inferType does not do beta-reduction.

I don't think that adequately explains what's happening, because #check FunLike.coe Bla.z 0 yields Wrapper as expected (and #check FunLike.coe Bla.z ∘ id also works). My understanding is that the app elaborator does head beta somewhere, I'm not sure where. Otherwise these spurious beta redexes would be everywhere.

[leodemoura]

While inferring the type we need to solve a unification constraint of the form

?m =?= (fun x => Wrapper) a

We cannot simply assign ?m := (fun x => Wrapper) a because a is not part of the local context associated with ?m.
At this point, isDefEq falls back to approximate solutions, and one of the succeeds after applying whnf.
I am pushing a fix that handles the failures at ?m := (fun x => Wrapper) a by trying beta-reduction. Note that this is not a full solution since it will not try more expensive reductions (e.g., delta, iota, etc) to make the assignment valid. It seems a good compromise. The beta-redex is very common.