feat: (experiment) have synth order defer "mixin" instances

src/Lean/Meta/Instances.lean

@@ -111,8 +111,7 @@ For example:
 
 (The type of `inst` must not contain mvars.)
 
-Remark: `projInfo?` is `some` if the instance is a projection.
-We need this information because of the heuristic we use to annotate binder
+Remark: Projections need special support because of the heuristic we use to annotate binder
 information in projections. See PR #5376 and issue #5333. Before PR
 #5376, given a class `C` at
 ```
@@ -133,11 +132,18 @@ After the PR, we have
 C.toB {inst : A 20000} [self : @C inst] : @B ...
 ```
 Note the attribute `inst` is now just a regular implicit argument.
-To ensure `computeSynthOrder` works as expected, we should take
-this change into account while processing field `self`.
-This field is the one at position `projInfo?.numParams`.
+To ensure `computeSynthOrder` works as expected, we take this change into account
+while processing the self field.
+In particular, we say a *projection* is any instance with a type of the form
+```
+{a1 : A1} → ... → {an : An} → [C a1 ... an] → ...
+```
+where the first n parameters are not instance implicit
+(we show implicit parameters above, but explicit is accepted as well).
+This definition of a projection captures all the kinds of projections
+that the `structure`/`class` commands declare (both field and parent projections).
 -/
-private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -154,6 +160,15 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
     else
       return #[]
 
+  -- Gets positions of all instance implicit arguments of `classTy`.
+  let getMixinPositionsOf (classTy : Expr) : MetaM (Array Nat) := do
+    forallTelescopeReducing (← inferType classTy.getAppFn) fun args _ => do
+      let mut pos := #[]
+      for arg in args, i in [:args.size] do
+        if (← arg.fvarId!.getDecl).binderInfo.isInstImplicit then
+          pos := pos.push i
+      return pos
+
   -- Create both metavariables and free variables for the instance args
   -- We will successively pick subgoals where all non-out-params have been
   -- assigned already. After picking such a "ready" subgoal, we assign the
@@ -181,23 +196,30 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   -- non-out-params are mvar-free.
   let mut synthed := #[]
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
+  -- Not every instance argument will have instance implicits. Record the positions of instance arguments for mixin calculations.
+  let instArgs ← List.range argMVars.size |>.filterM (fun i => return (← Meta.isClass? (← inferType argMVars[i]!)).isSome)
   while !toSynth.isEmpty do
-    let next? ← toSynth.findM? fun i => do
+    let next? ← toSynth.findSomeM? fun i => do
       let argTy ← instantiateMVars (← inferType argMVars[i]!)
-      if let some projInfo := projInfo? then
-        if projInfo.numParams == i then
-          -- See comment regarding `projInfo?` at the beginning of this function
-          assignMVarsIn argTy
-          return true
       forallTelescopeReducing argTy fun _ argTy => do
       let argTy ← whnf argTy
       let argOutParams ← getSemiOutParamPositionsOf argTy
+      let argMixinParams ← getMixinPositionsOf argTy
       let argTyArgs := argTy.getAppArgs
+      let mut mixins : Array Nat := #[]
       for i in [:argTyArgs.size], argTyArg in argTyArgs do
-        if !argOutParams.contains i && argTyArg.hasExprMVar then
-          return false
-      return true
-    let next ←
+        if argOutParams.contains i then
+          pure ()
+        else if argMixinParams.contains i then
+          let mvars ← getMVars argTyArg
+          for mvar in mvars do
+            if let some idx := argMVars.findIdx? (· == .mvar mvar) then
+              if instArgs.contains idx && !mixins.contains idx then
+                mixins := mixins.push idx
+        else if argTyArg.hasExprMVar then
+          return none
+      return some (i, mixins)
+    let (next, mixins) ←
       match next? with
       | some next => pure next
       | none =>
@@ -208,9 +230,10 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
           throwError m!"\
             cannot find synthesization order for instance {inst} with type{indentExpr instTy}\n\
             all remaining arguments have metavariables:{typeLines}"
-        pure toSynth[0]!
+        pure (toSynth[0]!, #[])
+    let mixins := mixins |>.filter (!synthed.contains ·)
     synthed := synthed.push next
-    toSynth := toSynth.filter (· != next)
+    toSynth := toSynth.filter (fun i => i != next && !mixins.contains i) ++ mixins
     assignMVarsIn (← inferType argMVars[next]!)
     assignMVarsIn argMVars[next]!
 
@@ -228,8 +251,7 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let projInfo? ← getProjectionFnInfo? declName
-  let synthOrder ← computeSynthOrder c projInfo?
+  let synthOrder ← computeSynthOrder c
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

tests/lean/run/2611.lean

@@ -22,19 +22,20 @@ class C [A] extends B
 class D extends A, B, C
 end Ex2
 
-/-!
-A test that this still works even when there are parameters on the structure.
--/
-namespace Ex3
-class A where
-  x : Nat
-class B [A] where
-  x : Nat
-class C (α : Type) extends A, B where
-  y : α
-/-- info: Ex3.C.toB {α : Type} [self : C α] : @B (@C.toA α self) -/
-#guard_msgs in set_option pp.explicit true in #check C.toB
-end Ex3
+-- The parent projection can't be an instance
+-- /-!
+-- A test that this still works even when there are parameters on the structure.
+-- -/
+-- namespace Ex3
+-- class A where
+--   x : Nat
+-- class B [A] where
+--   x : Nat
+-- class C (α : Type) extends A, B where
+--   y : α
+-- /-- info: Ex3.C.toB {α : Type} [self : C α] : @B (@C.toA α self) -/
+-- #guard_msgs in set_option pp.explicit true in #check C.toB
+-- end Ex3
 
 /-!
 A test that this still works even when there are parameters on the parents.

tests/lean/run/3807.lean

@@ -954,7 +954,7 @@ structure AddMonoidHom (M : Type _) (N : Type _) [AddZeroClass M] [AddZeroClass
 
 infixr:25 " →+ " => AddMonoidHom
 
-class AddMonoidHomClass (F M N : Type _) [AddZeroClass M] [AddZeroClass N] [FunLike F M N] : Prop
+class AddMonoidHomClass (F : Type _) (M N : outParam (Type _)) [AddZeroClass M] [AddZeroClass N] [FunLike F M N] : Prop
   extends AddHomClass F M N, ZeroHomClass F M N
 
 section One

tests/lean/synthorder.lean

@@ -24,3 +24,28 @@ class Three (α : Type) (β : outParam Type) [One β] [Two β]
 -- should both be accepted and synthesize `Three α β` first:
 class Four (α : Type) (β : outParam Type) [One β] [TwoHalf β] extends Three α β
 instance [One β] [TwoHalf β] [Three α β] : Four α β where
+
+/-!
+The structure elaborator needs to be able to define non-subobject projections with the same
+signatures as subobject parents. This is a test to see that the synth order can still be computed.
+-/
+class C1 (α : Type) [Inhabited α]
+-- Simulating a projection to another parent.
+instance C1.toNonempty {α : Type} {inst : Inhabited α} [C1 α] : Nonempty α := ⟨default⟩
+-- The parameters must come in a fixed order to be recognized as a projection. (TODO: not true now)
+instance C1.toNonempty' {α : Type} [DecidableEq α] {inst : Inhabited α} [C1 α] : Nonempty α := ⟨default⟩
+
+instance [Inhabited α] : C1 α := {}
+
+#synth C1 Nat
+
+class MyNonempty (α : Type _) : Prop where
+  nonempty : ∃ _ : α, True
+
+class C2 (α : Type) [Inhabited α]
+instance C2.toNonempty' {α : Type} [DecidableEq α] {inst : Inhabited α} [C1 α] : MyNonempty α := ⟨⟨default, trivial⟩⟩
+
+instance [Inhabited α] : C1 α := {}
+
+-- This synthesizes
+#synth MyNonempty Nat

tests/lean/synthorder.lean.expected.out

@@ -19,3 +19,20 @@ all remaining arguments have metavariables:
       Three α β
       One β
       TwoHalf β
+[Meta.synthOrder] synthesizing the arguments of @C1.toNonempty in the order [2, 1]:
+      C1 α
+      Inhabited α
+[Meta.synthOrder] synthesizing the arguments of @C1.toNonempty' in the order [1, 3, 2]:
+      DecidableEq α
+      C1 α
+      Inhabited α
+[Meta.synthOrder] synthesizing the arguments of @instC1 in the order [1]:
+      Inhabited α
+instC1
+[Meta.synthOrder] synthesizing the arguments of @C2.toNonempty' in the order [1, 3, 2]:
+      DecidableEq α
+      C1 α
+      Inhabited α
+[Meta.synthOrder] synthesizing the arguments of @instC1_1 in the order [1]:
+      Inhabited α
+C2.toNonempty'