Providing type-class explicitly

Stream: lean4

[Calle Sönne]

Is there a way I can provide a type-class instance to a function explicitly without using the @-notation? Or is there a way in which I can make the missing type class instance into a separate goal, instead of lean complaining that it can't synthesize the instance? I have a definition as follows:

noncomputable def inducedMap (p : 𝒳 ⥤ 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b)
    [IsCartesian p f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = g ≫ f)
    (φ' : a' ⟶ b) [IsHomLift p f' φ'] : a' ⟶ a := sorry

So basically a definition with a lot of parameters, and I want to apply it in a setting where lean can't infer the last parameter IsHomLift p f' φ', but aesop can prove it. I know I could make a have statement to obtain this instance before trying to use this definition, but the type of the missing instance is somewhat ugly to write down, so it would be a lot cleaner if I could avoid that.

[František Silváši 🦉]

If you have control of the def, naming the type class parameter (e.g. [IsHom : IsHomLift p f' φ']) lets you do induceMap (IsHom := ...).

If you do not, then the only way I can think of is to define an abbrev induceMap' that names the parameter and delegates to induceMap -- then you can use the trick above.

[Calle Sönne]

Thanks! The linter complains when I try to give a name to IsHomLift in the definition, since I don't use it explicitly in the construction, but the abbrev is a good trick!

[František Silváši 🦉]

Linter is a heuristic - it's sometimes perfectly legitimate to set_option linter.unusedVariables false in <your def> :).

[Calle Sönne]

František Silváši 🦉 said:

Linter is a heuristic - it's sometimes perfectly legitimate to set_option linter.unusedVariables false in <your def> :).

That makes sense, thanks!