Why `#check` succeed with mvars when there is an `instance`

Stream: lean4

[Dexin Zhang]

Why #check succeed with mvars when there is an unrelated instance, but fail if no such instance?

set_option pp.all true
axiom k : Type
axiom α : Type
axiom β : Type

class C (k α : Type)
def C.rel (k : Type) (α β : Type) [C k α] [C k β] := Unit
instance : C k α where
instance : C k β where
#check C.rel _ α β
-- @C.rel ?m.3298 α β ?m.3299 ?m.3300 : Type

However, if I remove the two instances, it becomes

failed to synthesize
  C ?m.3278 α

Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Kyle Miller]

Typeclass inference itself will throw an error if no instances can possibly apply.

The #check command configures things to try synthesizing what can possibly be synthesized, but it allows stuck typeclass problems to not cause an error. "Stuck" means "there's some metavariable that's making it unclear whether there aren't any instances that could apply".

[Kyle Miller]

These instances are certainly not unrelated; using k for the metavariable would cause them to apply.

[Kyle Miller]

The reason #check allows stuck instances is that it's inconvenient when #check doesn't show you anything at all.

Maybe it should still generate the error... That's doable.

[Dexin Zhang]

Kyle Miller said:

These instances are certainly not unrelated; using k for the metavariable would cause them to apply.

Oh thanks, does that mean the instance ?m2 : C ?m1 α may unify with something else, which triggers an assignment of ?m? But if so, why not also create a ?m2 even when there is no instance for C k α?

[Kyle Miller]

When you write C.rel _ α β, Lean elaborates this as @C.rel ?k α β ?inst1 ?inst2 and adds ?inst1 : C ?k α and ?inst2 : C ?k β as pending instance problems.

Eventually it will then start trying to synthesize ?inst1 and ?inst2. When there are metavariables, it will try to decide whether the instance problem is stuck, in which case it will defer until later, if possible, or otherwise if there are no instances that could ever apply to this situation, it immediately throws a "failed to synthesize" error.

[Dexin Zhang]

Kyle Miller said:

When you write C.rel _ α β, Lean elaborates this as @C.rel ?k α β ?inst1 ?inst2 and adds ?inst1 : C ?k α and ?inst2 : C ?k β as pending instance problems.

Eventually it will then start trying to synthesize ?inst1 and ?inst2. When there are metavariables, it will try to decide whether the instance problem is stuck, in which case it will defer until later, if possible, or otherwise if there are no instances that could ever apply to this situation, it immediately throws a "failed to synthesize" error.

Thanks, I got it. So ?inst1 : C ?k α will stuck if there is any instance for C xxx α (although ?k might be unrelated with xxx) but will fail immediately if there is no such instance.

[Kyle Miller]

Yes.

However, what do you mean by "unrelated" precisely? The metavariable might be able to unify with xxx, so that instance could apply if there were more information.

[Dexin Zhang]

I still feel they are not quite related, since the assignment of ?k is not triggered by the existence of instance C xxx α.

[Dexin Zhang]

The instance is applied only after ?k is assigned with xxx by some other things, isn't it?

[Kyle Miller]

Yes, though ?k represents the absence of an expression, so it has potential to be xxx, among other things.