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.