Type class instance error, synthesised vs inferred

Stream: lean4

[Calle Sönne]

I'm getting the following error:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  h₁
inferred
  FullofFullFiberwise inferInstance

In my code h₁ is defined as

  haveI : h₁ := FullofFullFiberwise inferInstance

So it seems very similar to the "inferred" term in the error message.

Does anyone know what errors like this mean? My code is quite deep in this repository: https://github.com/Paul-Lez/Stacks-project, so its hard for me to generate a mwe. What's the difference between synthesized and inferred in this error message?

[Calle Sönne]

If I try to remove h₁, then it can't synthesise the type class instance at all.

[Sébastien Gouëzel]

What happens if you replace haveI with let?

[Kevin Buzzard]

ie is it data or a prop?

[Calle Sönne]

Sébastien Gouëzel said:

What happens if you replace haveI with let?

It works, thanks a lot!

[Calle Sönne]

Kevin Buzzard said:

ie is it data or a prop?

Okay so whenever I have a type class instance containing data I need to supply it using let?

[Kevin Buzzard]

example : False := by
  let a : Nat := 2
  have b : Nat := 3
  /-
  a : Nat := 2
  b : Nat
  ⊢ False
  -/
  sorry

You can now prove a = 2 with rfl, but proving b = 3 is impossible. let remembers the answer. have is for proofs because you don't need to remember which proof it is, they're all equal.

[Calle Sönne]

Something I found interesting is that if I define h₁ as haveI h₁ := sorry, then I get the exact same error, and not something like

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  h₁
inferred
  something else here

so does it still knows about FullofFullFiberwise inferInstance somehow? But it can't seem to infer that by itself without the let statement.

[Floris van Doorn]

This behavior is super confusing for new users, and should be changed: lean4#3559

[Kevin Buzzard]

Please thumbs-up the issue if you agree! This is a nice quality-of-life issue with a relatively straightforward solution (once the devs have decided which solution to implement!), so it makes using Lean easier.

[Kim Morrison]

I've asked for comments internally at the FRO. Seems like an important papercut to me!

[Damiano Testa]

I wrote a have vs let linter at #12157, in case anyone is interested. I have not yet had a chance to examine what it is flagging in mathlib, though.

[Robert Maxton]

Calle Sönne said:

Does anyone know what errors like this mean? My code is quite deep in this repository: https://github.com/Paul-Lez/Stacks-project, so its hard for me to generate a mwe. What's the difference between synthesized and inferred in this error message?

To give a more general answer: as I understand it there are (at least) two different ways to come up with a typeclass instance when required. First is the usual implicit-argument inference: if some other, explicitly provided argument (or the expected type) references that argument in its definition, then we can just use that definition. For example, if you have

def foo {a : ℕ} (h: a  = 0) := ...

then the type of h only makes sense in the context of some specific a, and providing a proof of h implicitly defines what a has to be.

(Unpopular opinion: This is part of why I actually really like the new autoImplicit feature. AFAICT, it introduces new implicit variables precisely when they would be inferred upon invocation; it's not only convenient, but also a method of checking as you write that your model of what the compiler can infer matches reality.)

The other is the typeclass specific synthesis function. Which, tbqh, I don't understand nearly as well as implicits, but roughly speaking, it looks through all available instances for something of the right type (up to metavariables in the case of (semi)OutParam), looks back at the arguments to those instances, then tries to infer or synthesize the arguments recursively.

In general, these are two distinct methods of generating instances and there's no guarantee they'll give the same result, but they will need to in order for the theorem invocation/function call to be sound -- after all, by the logic of the implicit argument inference, a specific instance is required for a later explicit argument to be defined in the first place. It could try and silently resolve in favor of one or the other (usually the implicit argument, I think), but that would be a bit of a footgun that would give surprising results -- this almost always means that there's an error in your code somewhere (usually an 'extra' or insufficiently-detailed instance definition), so better to 'fail fast' and report that error as soon as possible.

[Calle Sönne]

Robert Maxton said:

Calle Sönne said:

Does anyone know what errors like this mean? My code is quite deep in this repository: https://github.com/Paul-Lez/Stacks-project, so its hard for me to generate a mwe. What's the difference between synthesized and inferred in this error message?

To give a more general answer: as I understand it there are (at least) two different ways to come up with a typeclass instance when required. First is the usual implicit-argument inference: if some other, explicitly provided argument (or the expected type) references that argument in its definition, then we can just use that definition. For example, if you have

def foo {a : ℕ} (h: a  = 0) := ...

then the type of h only makes sense in the context of some specific a, and providing a proof of h implicitly defines what a has to be.

(Unpopular opinion: This is part of why I actually really like the new autoImplicit feature. AFAICT, it introduces new implicit variables precisely when they would be inferred upon invocation; it's not only convenient, but also a method of checking as you write that your model of what the compiler can infer matches reality.)

The other is the typeclass specific synthesis function. Which, tbqh, I don't understand nearly as well as implicits, but roughly speaking, it looks through all available instances for something of the right type (up to metavariables in the case of (semi)OutParam), looks back at the arguments to those instances, then tries to infer or synthesize the arguments recursively.

In general, these are two distinct methods of generating instances and there's no guarantee they'll give the same result, but they will need to in order for the theorem invocation/function call to be sound -- after all, by the logic of the implicit argument inference, a specific instance is required for a later explicit argument to be defined in the first place. It could try and silently resolve in favor of one or the other (usually the implicit argument, I think), but that would be a bit of a footgun that would give surprising results -- this almost always means that there's an error in your code somewhere (usually an 'extra' or insufficiently-detailed instance definition), so better to 'fail fast' and report that error as soon as possible.

Thanks, this exlains a lot! Do typeclasses always have to be "synthesized"? Could it be that it finds no available instance of the right type, but it can infer one implicitly, then it just uses the inferred one? I'm guessing no, because if that was the case I should have just be able to delete the haveI line, and get no errors.

[Robert Maxton]

That gets into "I would like to know that too", honestly ^.^;. (c.f. my question at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Help.20with.20instance.20search.20and.20.28semi.29OutParam, for example, where despite having exactly one instance in scope instance search can't find it.) inferInstance doesn't quite do the same thing as normal synthesis; it's more targeted, and its purpose is to bring an inference into 'scope' for typeclass inference.

Something to keep in mind though is that the use of implicit arguments is AFAIK explicitly about whether or not the argument is determined by later arguments to the same function -- in my case, for example, the fact that there's only one possible argument because there's only one instance in scope is only relevant to typeclass synthesis, it's expected that implicit-argument-inference won't find it in a case like that unless it's specifically used, directly or indirectly, by another argument.