projection notation with {}

Stream: general

[Kevin Buzzard]

def P : ℕ → Prop := sorry

-- imagine this is in core so I can't change the {} choice
structure bar (α : Type*) :=
(h : ∀ {x : ℕ}, P x)

-- This is my cool structure
structure foo (α : Type*) :=
(n : ℕ)

-- This is my cool map from my structure to the core one
def foo.to_bar {α : Type*} (f : foo α) : bar α := sorry

-- So now, given a term of type `foo α` I can make a term of type `bar α`
-- and hence deduce `P x` for all `x : ℕ

example {α : Type*} (f : foo α) : P 3 :=
--f.to_bar.h -- type mismatch
--f.to_bar.h 3 -- function expected
-- @(f.to_bar.h) 3 -- syntax error
bar.h f.to_bar -- works

Do I have to give up on projection notation in situations like this, or is there a clever way to insert the @? I couldn't figure it out.

[Floris van Doorn]

I think you have to give up on projection notation in this case. I have also noticed this annoying behavior sometimes.