local instance cannot find synthesization order in porting

Stream: mathlib4

[Gabin Kolly]

I'm currently trying to port ModelTheory.DirectLimit.lean, and there is a "cannot find synthesization order" error on attribute [local instance] DirectLimit.setoid, where DirectLimit.setoid has type:

FirstOrder.Language.DirectLimit.setoid.{v, w, u_1, u_2} {L : Language} {ι : Type v} [inst✝ : Preorder ι]
  (G : ι → Type w) [inst✝¹ : (i : ι) → Structure L (G i)] (f : (i j : ι) → i ≤ j → G i ↪[L] G j)
  [inst✝² : DirectedSystem G fun i j h ↦ ↑(f i j h)] [inst✝³ : IsDirected ι fun x x_1 ↦ x ≤ x_1] :
  Setoid ((i : ι) × G i)

The error says:

cannot find synthesization order for instance @DirectLimit.setoid with type
  {L : Language} →
    {ι : Type v} →
      [inst : Preorder ι] →
        (G : ι → Type w) →
          [inst_1 : (i : ι) → Structure L (G i)] →
            (f : (i j : ι) → i ≤ j → G i ↪[L] G j) →
              [inst_2 : DirectedSystem G fun i j h ↦ ↑(f i j h)] →
                [inst : IsDirected ι fun x x_1 ↦ x ≤ x_1] → Setoid ((i : ι) × G i)
all remaining arguments have metavariables:
  (i : ι) → Structure ?L (G i)
  @DirectedSystem ι inst✝³ G fun i j h ↦ ↑(?f i j h)

I'm a bit at a loss, I don't know how to solve this.

[Kevin Buzzard]

This came up recently -- search for "cannot find synthesization order" on this Zulip and someone I think mentioned a way of overriding this check

[Gabin Kolly]

I searched before, but I was very confused by the discussions. The solutions that appeared were:

1. Adding set_option synthInstance.checkSynthOrder false but was considered to be just hiding the problem, not solving it.
2. Adding (semi)outParam somewhere? I tried to place it at random places, but I don't really understand the confusion in my case, so I don't know where to put it.
3. Adding hints, but again, I don't know what Lean wants.
4. Remove the instance.
   It seems to be confused by L, which is supposed to be a Language, and f, which is a function with L as a parameter.

[Xavier Roblot]

You should look at where the intance is used. If it is used at a very few places, preferably once, you can do as I did in !4#4228 and just delete the instance and just declare it by hand where it is used.

[Gabin Kolly]

If I try to remove it, I go from 11 to 47 errors, so it is very much used :sweat_smile:

[Xavier Roblot]

Indeed. Well, I can have a look later on if you want

[Xavier Roblot]

Ok, The problem is that the statement of DirectLimit.setoid is about Σi, G i but Lean needs also to know what is L. Thus the instance fails because Lean cannot infer that from only Σi, G i. One way to fix that, suggested there, would be create an alias definition that also contains f( from which all the required information can be inferred) and that is defeq to Σi, G I and use it in the statement of DirectLimit.setoid. Something like:

def SigmaG (f : ∀ i j, i ≤ j → G i ↪[L] G j) := Σi, G i

But that solution would require to make significative change to the rest of this file and I don't know enough about this part of Mathlib to see if it is good idea.

If somebody with more expertise could give their opinion, that would be great.

[Gabin Kolly]

Thank you!
Interesting. I will wait on opinion from experts.
Perhaps @Aaron Anderson ?

[Aaron Anderson]

This is a direct limit construction - these are unique up to unique isomorphism, so the actual type could easily be a synonym. However, the definition of the setoid only depends on the actual functions underlying the maps, and works the same way as direct limits in algebra. Should we just define the direct limit of a family of functions, and then put different algebraic/first-order structures on that?

[Xavier Roblot]

Yes, that is probably the best way to solve the problem. But such a major refactor would have to wait for after the port. I would advise to use the simplest fix using set_option synthInstance.checkSynthOrder false and add a porting note explaining the situation and the fact that a proper fix would come later on.

[Yaël Dillies]

It's not a major refactor, is it? That file is almost leaf (only file#model_theory/fraisse depends on it), and adding a type synonym is routine.

[Xavier Roblot]

Yes, it is not a major refactor but still it requires to change/add some definition, statements and proofs. I am on the phone right now so I can’t really see how much work would be necessary. It depends also if anyone is motivated… @Aaron Anderson ?

[Gabin Kolly]

I've finished the rest of the porting and just put a set_option synthInstance.checkSynthOrder false for the moment, see https://github.com/leanprover-community/mathlib4/pull/4391.

[Xavier Roblot]

Don’t forget to add a porting note explaining the situation and the need for a refactor later on.

[Jireh Loreaux]

!4#4476 is stuck on a synthesization order problem. Basically, part way through the file it has a bit about finite dimensional spaces. We want Lean to automatically conclude these are complete using docs4#FiniteDimensional.complete and in Lean 3 this worked by making this declaration a priority-20 local instance. In Lean 4, it (correctly) triggers the synthesization order problem, but just turning off checkSynthOrder doesn't help because Lean can find the instance when it needs it.

So, how should we deal with this? I see two options, neither of which are optimal:

1. Add optParams using FiniteDimensional.complete, but this is an actual change to the declarations.
2. Insert a bunch of haveIs in the statements and proofs, which does not actually change the declarations.

Are there other options I'm missing? If not, which of these should we go for?

[Jireh Loreaux]

ah, nevermind, I just realized I needed to turn off that check for the entire section.

[Eric Wieser]

3. Add [complete V] to the statements (post-port)

[Eric Wieser]

That instance is definitely a bad one, k can't be found other than by exhaustive search!

[Eric Wieser]

Oh never mind, you said _local_ instance

[Aaron Anderson]

Xavier Roblot said:

Yes, it is not a major refactor but still it requires to change/add some definition, statements and proofs. I am on the phone right now so I can’t really see how much work would be necessary. It depends also if anyone is motivated… Aaron Anderson ?

I think I solved this at branch#direct_limit_refactor

[Aaron Anderson]

Is it worth trying to PR this refactor now?

[Xavier Roblot]

I think it is fine if you're ready to also forward port the changes to Mathlib4