Help with simple macro

Stream: lean4

[Calle Sönne]

I want to write a very simple macro, which takes 3 terms, and calls another tactic with these three terms. However, I'm having some trouble getting it to work. This is what I want to write:

/-- `subst_hom_lift p f φ` tries to substitute `f` with `p(φ)` by using `p.IsHomLift f φ` -/
macro "subst_hom_lift" p:term f:term φ:term : tactic =>
  `(tactic| obtain ⟨⟩ := Functor.IsHomLift.cond (p := $p) (f := $f) (φ := $φ))

However, when I try to call it with a functor p : 𝒳 ⥤ 𝒮, and two morphisms f and φ, I get the error:

function expected at
  p
term has type
  𝒳 ⥤ 𝒮

I am not sure how to make sense of this error., but I assume it is because I am not substituting in the terms correctly. Will I need to do some preprocessing to make this work?

Previously I just wrote the macro with idents instead of terms, but then I will not be able to use the macro on more complicated expressions (such as when f is of the form F.map g). If you want to run it your self, the ident version is in CategoryTheory/FiberedCategory/HomLift in mathlib.

[Marcus Rossel]

What the error message is (indirectly) telling you is that when you write subst_hom_lift a b c, it's interpreting a b c as the first term (named p in your macro). Therefore a is expected to be a function with b and c being arguments to a. The way to fix this is by writing p:term:max f:term:max φ:term:max in your macro.

[Calle Sönne]

Thanks a lot!