using @ with expressions that are not definitions

Stream: general

[Chris Hughes]

Is there a way to get this to work nicely

constant F : Type

constant F_to_fun (f : F) : Π {X : Type}, X → X

example (f : F) (h : (Π (X : Type), X → X) → ℕ) : ℕ :=
h (F_to_fun f)

There is nowhere I can put an @ to make the type of F_to_fun f into Π (X : Type), X → X instead of ?m_1 -> ?m_1

[Alex J. Best]

Maybe I'm misunderstanding the question but

constant F : Type

constant F_to_fun (f : F) : Π {X : Type}, X → X

noncomputable
example (f : F) (h : (Π (X : Type), X → X) → ℕ) : ℕ :=
h (@F_to_fun f)

checks fine for me

[Chris Hughes]

Thanks. That didn't work in my other example because F_to_fun had some other implicit arguments, but some extra underscores fixed that. I was also confused by the squiggly lines telly me _example was noncomputable, I should have actually read the error.