Functions are fun_like

Stream: general

[Anatole Dedecker]

Would the following break anything?

instance Pi.fun_like {α : Sort*} {β : α → Sort*} : fun_like (Π a, β a) α β :=
{ coe := id,
  coe_injective' := λ x y h, h }

(or the equivalent with has_coe_to_fun, I don't care)

[Yaël Dillies]

I suggest trying it out. My bet is on it going wrong horribly and quickly, but I can't be sure!