synth bug, not inferring instance defined just above

Stream: lean4

[RustyYato]

For context, I'm working on a clone of mathlib with some of my own changes for my own learning purposes.

I ran into a bug where Lean is unable to synthesize an instance that was declared just above it. Due to how deep this is in my project, and my unfamiliarity with #synth, I'm not able to create a nice MVE. But I have saved this bug into a branch linked below.

https://github.com/RustyYato/lean4-math/blob/4bfa4a8e14d94c28acd6b96c06d12b50789799bf/Math/Topology/MetricSpace/Defs.lean#L127-L137

The relevant portion looks like this, with the following error showing up in VSCode

instance : IsMetricSpace (α × β) := Prod.metricSpaceSup

#synth IsMetricSpace (α × β)

failed to synthesize
  IsMetricSpace (α × β)

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

My lean version

Lean (version 4.19.0-nightly-2025-03-24, x86_64-unknown-linux-gnu, commit 635af865bf52, Release)

I wanted to check to see if this was something I was doing before filing a bug report. Does anyone know what might be going on?

[Kyle Miller]

Does this work?

example : IsMetricSpace (α × β) := inferInstance

Also, if you hover over the keyword instance in instance : IsMetricSpace (α × β) := Prod.metricSpaceSup, what type do you see?

[RustyYato]

no, inferInstance is in the same boat (and that's actually how I found this, since I wasn't able to synthesize this instance for some reason, and while trying to reduce that bug I ran into this more weird bug).

Also, if you hover over the keyword instance in instance : IsMetricSpace (α × β) := Prod.metricSpaceSup, what type do you see?

This type, which is correct as far as I can tell.

instIsMetricSpaceProd.{u_1, u_2, u_3} {α : Type u_2} {γ : Type u_3} {β : Type u_1} [Dist α γ] [Dist β γ] [LE γ] [LT γ]
[AddMonoidOps γ] [IsOrderedAddCommMonoid γ] [Sup γ] [IsSemiLatticeSup γ] [IsAddCancel γ] [IsMetricSpace α]
[IsMetricSpace β] : IsMetricSpace (α × β)

I forgot to put this in my example above, but I also have these variables in scope

variable
  [Dist α γ] [Dist β γ]
  [LE γ] [LT γ] [AddMonoidOps γ]
  [IsOrderedAddCommMonoid γ]
  [Sup γ] [IsSemiLatticeSup γ]
  [IsAddCancel γ]
  [IsMetricSpace α] [IsMetricSpace β]

[Aaron Liu]

RustyYato said:

I forgot to put this in my example above, but I also have these variables in scope

variable
  [Dist α γ] [Dist β γ]
  [LE γ] [LT γ] [AddMonoidOps γ]
  [IsOrderedAddCommMonoid γ]
  [Sup γ] [IsSemiLatticeSup γ]
  [IsAddCancel γ]
  [IsMetricSpace α] [IsMetricSpace β]

If I put that at the top of my scope, I get an error, because docs#Dist only takes one type argument.

[Kevin Buzzard]

Maybe lean is failing to synthesise gamma? Is it an outparam?

[RustyYato]

If I put that at the top of my scope, I get an error, because docs#Dist only takes one type argument.

Yes, that's because this isn't Mathlib :), this is from my own project which is quite similar to mathlib (since I'm using it as a reference for my own learning,).

Maybe lean is failing to synthesise gamma? Is it an outparam?

yes it's in outparam in Dist, IsPseudoMetricSpace and IsMetricSpace.

And now that I think of it, why is it an outparam in IsPseudoMetricSpace and IsMetricSpace? That seems suspect.

[RustyYato]

Wow, removing outparam on the Is*MetricSpace type-classes fixed the issue. I still don't understand why that is. Is there a special interaction that I'm not aware of?

the relevant snippet is this one

class Dist (α: Type*) (β: outParam Type*) where
  dist: α -> α -> β

class IsPseudoMetricSpace (α: Type*) {β: Type*} -- before β was also marked as an outParam, and that seemed to cause the issue
  [LT β] [LE β] [AddMonoidOps β] [IsOrderedAddCommMonoid β]
  [Dist α β] : Prop extends IsLinearOrder β where

[Aaron Liu]

Meybe set_option trace.Meta.synthInstance true will be able to help you

[RustyYato]

Thanks for all the help! Looks like I'll need to figure out how to properly use outParam :smiley:. I thought I had understood it, but it looks like there are some subtleties I need to figure out.

[Kyle Miller]

I think you're running into a (known) bug where it's failing to report that IsPseudoMetricSpace has a questionable parent projection instance.

The parent projection to IsLinearOrder β needs to somehow figure out what α is to apply. How can it do this? (Take a look at IsPseudoMetricSpace.toIsLinearOrder to see the instance.) Could you try set_option trace.Meta.synthOrder true and report back on the synth order for the arguments to this instance?

I believe what you need to do instead is not extend IsLinearOrder β, and instead add it as an [IsLinearOrder β] argument.

[RustyYato]

Could you try set_option trace.Meta.synthOrder true and report back on the synth order for the arguments to this instance?

[Meta.synthOrder] synthesizing the arguments of @instIsMetricSpaceProd in the order [3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13]:
      Dist α γ
      Dist β γ
      LE γ
      LT γ
      AddMonoidOps γ
      IsOrderedAddCommMonoid γ
      Sup γ
      IsSemiLatticeSup γ
      IsAddCancel γ
      IsMetricSpace α
      IsMetricSpace β

I think you're running into a (known) bug where it's failing to report that IsPseudoMetricSpace has a questionable parent projection instance.

I see, is this because there's no reliable way to work backwards from IsLinearOrder Y to IsMetricSpace A (with Dist A Y)?

[Kyle Miller]

Yeah, there's no way to infer A.

I think the only reason it's looking like it works at the moment is that instances that come from the local context (e.g. ones from variables or binders) use slightly different rules, and the consequence is that it's solving for A by unification. I didn't do an experiment to validate this in your case.

[Kyle Miller]

(The bug is that the synthOrder checker ignores issues with parent projection type parameters. It assumes they're all solvable by unification, which is not true in general.)

[RustyYato]

Ok that makes sense, I'll probably switch over to [IsLinearOrder] soon then. Thanks for the heads up!

[RustyYato]

I think you're running into a (known) bug where it's failing to report that IsPseudoMetricSpace has a questionable parent projection instance.

Oh wow, I ran into this exact issue somewhere else in my project, it would have taken forever to debug without your heads up! Thanks again @Kyle Miller