Synthesize of typeclass from its parameter

Stream: lean4

[Shuhao Song]

I'm trying to formalize modal logic in Lean 4, and I finished formalizing Gödel's ontological proof in this link https://github.com/znssong/lean-modal-logic/blob/main/god_exists.lean. I found the formalization of modal logic will be very easy if typeclass can be synthesized from its parameter; for example, in current nightly version of Lean 4, the following code

class C where n : Nat
#synth [a : C] → [b : C] → C

will fail and report that typeclass can't be synthesized.

We use typeclass to represent the "current" possible world: @[class] axiom World : Type and variable [w : World]. The necessary modality takes a &Prop (notation for [World] → Prop), and outputs a Prop which uses the current world w:

def Necessary (p : &Prop) := ∀ w', Accessible w w' → p@.w'

where @. is the instantiation of &Prop at a certain possible world. So, when you write □∀x, p x, the elaborator will know ∀x, p x is a Prop and □ needs a &Prop, so it will automatically introduce the parameter [World] in &Prop := [World] → Prop into the context as w✝. Moreover, because the lastly introduced local instance will get more priority (see the source code of Lean.Meta.SynthInstance.getInstances), so w✝ will become the new "current world", and the proposition p in □p will automatically uses the world implicitly mentioned in □. That is, when I'm writing ∀x, p x for p : [w : World] → @Object w → Prop, it will be instantiated as ∀x, @p w x where w be the section variable (current world), and when writing □∀x, p x, it will be instantiated as ∀w', Accessible w w' → ∀x, @p w' x, because the synthesizer will choose newly introduced w✝ as the instance of class World.

But another things happens. Without this modification, the compilation will fail at positive_possible_exists, when elaborating ◇∃ x, P x. That is because the type of x is a metavariable during elaboration, and we need to fill the metavariable; for example, it is ?m.49386 P w✝ now. However, ?m.49386 is of type {P : Property} → [w : World] → Sort ?u.49372, and its context is only the global context w : World, where the newly introduced variable P and w✝ turned to parameters in the type of metavariable. So in isDefEq, ?m.49386 will be filled using w instead of w✝, since the type class inference only cares about LCtx of metavariables and ignores [w : World] in the parameter of its type. So it will report an error: synthesized type class instance is not definitionally equal to expression inferred by typing rules.

I modified the Lean source code for fixing this, and the snippet was contained in the proof. I wonder whether this snippet could be merged into the mainline. May I open a PR for this?

[Kim Morrison]

I'm struggling to understand what you're asking. Can you give an example of whatever problem you're seeing without using axiom?

In general, proposals to touch anything to do with typeclass synthesis are received with considerable skepticism. :-)

[Shuhao Song]

Kim Morrison said:

I'm struggling to understand what you're asking. Can you give an example of whatever problem you're seeing without using axiom?

In general, proposals to touch anything to do with typeclass synthesis are received with considerable skepticism. :-)

Why you need "without using axiom"? Postulating axiom or variable in examples are common. For example, when you want to consider an abstract class as example, you may use @[class] axiom C : Type.

[Kevin Buzzard]

Mathlib has many variables but no axioms. So postulating axioms in mathematics in lean is arguably extremely rare, not common.