projection instance binderinfo problem

Stream: lean4

[Jovan Gerbscheid]

There is something wrong with either the synthesization order check, or the projection instance binder info. In lean#5376 a change was made to the projection instance binder info to be implicit.

But in the following, if I try to define an instance exactly like the projection instance, Lean complains

class Nontrivial (α : Type) : Prop where
class Group (α : Type) where

class IsSimpleGroup (G : Type) [Group G] : Prop extends Nontrivial G where

/-
IsSimpleGroup.toNontrivial {G : Type} {inst✝ : Group G} [self : IsSimpleGroup G] : Nontrivial G
-/
#check IsSimpleGroup.toNontrivial

/-
cannot find synthesization order for instance @instNontrivialOfIsSimpleGroup with type
  ∀ {G : Type} {x : Group G} [self : IsSimpleGroup G], Nontrivial G
all remaining arguments have metavariables:
  @IsSimpleGroup G ?x✝
-/
instance {G : Type} {_ : Group G} [self : IsSimpleGroup G] : Nontrivial G := sorry

[Aaron Liu]

The Group G argument is not determined exactly.

[Aaron Liu]

Since it is implicit now, it won't be solved for by typeclass.

[Jovan Gerbscheid]

I agree, and this means that the automatically generated IsSimpleGroup.toNontrivial is problematic.

[Kyle Miller]

I just noticed this issue last week, and I have some ideas for fixes that I hope will land by the end of the quarter.

[Kyle Miller]

It came up when trying to give all parent instances (even non-subobject parents) the same implicit argument rules for the type's parameters. These are basically user-defined instances.

[Kyle Miller]

Note that IsSimpleGroup.toNontrivial is not problematic since the synth order algorithm has special support for direct projections.

[Kyle Miller]

Edit: no, I read too quickly and misremembered the current algorithm, it's problematic.

[Kyle Miller]

I haven't run the proposal by anyone yet, since I wanted to test it first and see if it causes a performance impact, but here it is for your consideration:

The rough idea:

• The synth order algorithm will see every implicit argument that's an instance as a true instance implicit argument. This allows projections to be used as instances, without needing to special case projections in the algorithm. Rationale: With projections, you don't want to resynthesize the type's parameters, since they're all determined by the self argument and should be solved for by unification. Rationale: non-subobject parents are not true projections, but they should be handled in the same way.
• If an instance argument has "mixin arguments" (which I am loosely defining as any instance arguments that appear anywhere in its type), then those mixin arguments will be synthesized after that argument. Heuristic: instances are supposed to be canonical, and the observation of lean#5376 was that most of the time they seem to be solved for by unification anyway. Heuristic: the argument's mixins give much less information about whether the instance will succeed than the argument itself.

[Jovan Gerbscheid]

I like this idea. How do you plan to deal with the more awkward cases where a "mixin argument" can't be determined by unification? For example in

NoMaxOrder.infinite {α : Type*} [Preorder α] [Nonempty α] [NoMaxOrder α] : Infinite α

The parameter Preorder α appears in the parameter NoMaxOrder α, but only as a LT argument. This is annoying because it means that to failing to synthesize Infinite _ (or Nontrivial _, Nonempty _) requires traversing the entire Preorder hierarchy.

[Jovan Gerbscheid]

I think what could happen is:

We first synthesize NoMaxOrder α, and either this gives us as LT instance based on a Preorder instance, in which case we are happy because unification gives us the result.

Or, unification gets stuck, which forces unification to resolve the stuck metavariable of type Preorder α using a nested type class search.

[Jovan Gerbscheid]

I also like that the synth order treats implicit/instance implicit binders the same. In the status quo, there are a bunch of instances that can be optimized by replacing the [..] binder by {_ : ..}, but that isn't nice to write or look at. I presume that the projection instance binder annotations can then go back to what they were before lean#5376, because the difference doesn't really matter anymore.

[Kyle Miller]

For this example, the proposed algorithm would say the synth order is Nonempty α, NoMaxOrder α, and then Preorder α. Suppose we've found a Nonempty instance. My rough understanding then is:

• If there's obviously no NoMaxOrder that can apply, we are done.
• Otherwise, if there is a possible NoMaxOrder, it will try unifying the LT arguments. In this case it's @Preorder.toLT α ?preorderInst. Unifying against that is indeed a case of a stuck metavariable. However, class projections are special, and this does not trigger a nested type class search (see docs#Lean.Meta.getStuckMVar?).
• It then goes on to try to synthesize the Preorder α instance.

[Jovan Gerbscheid]

Actually looking at docs#Lean.Meat.getStuckMVar?, I see that it specifically does trigger a nested type class search "if e is a type class projection that is stuck because the instance has not been synthesized yet."

[Kyle Miller]

Huh, you're right, I read it backwards. Earlier I tried making a example from NoMaxOrder.infinite that would trigger a nested type class search but I was having some trouble.

Would you be interested in trying to verify whether it does or doesn't actually trigger a nested typeclass search with this example? You may need to turn off the synthOrder error and then override the synth order. I think it should be possible to do without modifying Lean; just some attributes and a set_option.

[Jovan Gerbscheid]

Yes, in this example setting the synthOrder to be #[2,3] does indeed trigger a nested type class search

import Mathlib

/-!
# Specify the synthesization order for instances
-/

namespace Lean.Meta

/-- Specify the synthesization order for instances. -/
def Instances.setSynthOrder (declName : Name) (synthOrder : Array Nat) : CoreM Unit := do
  let some entry := Meta.instanceExtension.getState (← getEnv) |>.instanceNames.find? declName |
    throwError "'{declName}' does not have [instance] attribute"
  instanceExtension.add { entry with synthOrder } entry.attrKind

end Lean.Meta

namespace Lean.Elab.Command

open Meta

/-- Specify the synthesization order for instances. -/
elab "set_synth_order " name:ident synthOrder:term : command => do
  let q := Term.MatchExpr.toDoubleQuotedName name
  elabCommand (← `(command| run_meta Instances.setSynthOrder $q $synthOrder))

end Lean.Elab.Command

attribute [instance high] NoMaxOrder.infinite
set_synth_order NoMaxOrder.infinite #[2,3]


variable (α : Type) [Preorder α] [Nonempty α] [NoMaxOrder α]

set_option trace.Meta.synthInstance true

#synth Infinite α
/-
[Meta.synthInstance] ✅️ Infinite α ▼
  [] new goal Infinite α ▶
  [] ✅️ apply @NoMaxOrder.infinite to Infinite α ▶
  [] ✅️ apply inst✝¹ to Nonempty α ▶
  [resume] propagating Nonempty α to subgoal Nonempty α of Infinite α ▶
  [] ✅️ apply inst✝ to NoMaxOrder α ▼
    [tryResolve] ✅️ NoMaxOrder α ≟ NoMaxOrder α ▼
      [] ✅️ Preorder α ▼
        [] new goal Preorder α ▶
        [] ✅️ apply inst✝² to Preorder α ▶
        [] result inst✝²
    [answer] ✅️ NoMaxOrder α
  [] ✅️ Preorder α ▶
  [resume] propagating NoMaxOrder α to subgoal NoMaxOrder α of Infinite α ▶
  [] result NoMaxOrder.infinite
-/

[Jovan Gerbscheid]

Looking more closely, I am confused why the nested type class search is triggered

[isDefEq] ✅️ @NoMaxOrder α (@Preorder.toLT α ?m.52464) =?= @NoMaxOrder α (@Preorder.toLT α inst✝²) ▼
  [] ✅️ α =?= α
  [synthInstance] ✅️ Preorder α ▶
  [] ✅️ @Preorder.toLT α inst✝² =?= @Preorder.toLT α inst✝² ▶

Because this unification problem is perfectly solvable with simple unification.

[Jovan Gerbscheid]

So I think that a fix to the unification algorithm is required, so that it only tries nested type class search when this is actually necessary.

[Jovan Gerbscheid]

Another bad instance that was recently added is

CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape.{w, v₁, u₁} {C : Type u₁} {inst✝ : Category.{v₁, u₁} C}
  (κ : Cardinal.{w}) {inst✝¹ : Fact κ.IsRegular} [self : HasCardinalFilteredColimits C κ] (J : Type w) [SmallCategory J]
  [IsCardinalFiltered J κ] : Limits.HasColimitsOfShape J C

Where lean should complain that there is no way of determining κ. But I guess it doesn't complain because this function is a class projection.

[Jovan Gerbscheid]

In lean#9582 I made an attempt at implementing the synth order algorithm that you hinted at. But CI keeps running forever, so it doesn't give me a mathlib testing branch. Does anyone know what's going on?

[Kim Morrison]

lean#9582

[Kim Morrison]

I've cancelled and restarted, but sorry, no, I don't know what's happening.

[Jovan Gerbscheid]

@Kyle Miller, I've now tried this, in a new PR where CI did work (lean#9638).

• I reverted the binderInfo of projection instances back to what they should be

• I changed the synthOrder algorithm to skip instances that appear as direct arguments in other instances. In the case of projection instances, which are of the form A.toB {x₁ x₂ ... xₙ} [self : @A x₁ x₂ ... xₙ] : B, all of the x₁, x₂, ... xₙ are direct arguments to the self instance, so we only need to synthesize self.
  But the same principle applies to other instances such as [Group G] [IsKleinFour G] : IsAddKleinFour (Additive G), where the instance of Group G is a direct argument to IsKleinFour G, so we don't need to bother synthesizing Group G.

• An exception is made for instances that have outParams. We don't skip synthesizing them because we need to make sure that the synthesized outParam is correct (and some other things went wrong too with such instances)

I encountered some issues

1. Due to the special handling of projection instances, there are some cases that (in old versions of Lean) used to give a warning, but now don't. A few of these bad uses of extends have appeared since then. In particular batteries#1359, #27941 and #mathlib4 > IsModuleFiltration.
2. The premise for the optimization in the synthOrder (either just in projection instances, or in general) is that instance arguments of type classes act like semiOutParams, in the sense that they are allowed to be left as metavariables in type class search goals, and that they will be filled in by the type class search.
   For this reason, I also added a check to verify that instances satisfy this property. But unfortunately there are some instances in mathlib that rely on an instance argument being given. Some examples are docs#CategoryTheory.Monoidal.fromInducedMonoidal, docs#CategoryTheory.Functor.Linear, docs#SMul.comp.isScalarTower (which is added as a local instance somewhere) and docs#CategoryTheory.BundledHom.hasForget . Do you think it makes sense to check for this, and to fix breakages with set_option synthInstance.checkSynthOrder false? Or should we accept that the above premise simply doesn't always hold? (Or maybe we can have some kind of exensible mechanism to determine for which classes the optimization is allowed; currently it just isn't allowed for classes with outParams)

[Jovan Gerbscheid]

I have now also made two issues for the problems I'm trying to solve: lean#9727 and lean#9726