feat: let synth order checker detect generalized projections

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
 
@@ -169,6 +175,16 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
         mvarId.assign argVars[i]!
       assignMVarsIn (← inferType (.mvar mvarId))
 
+  -- Before anything, detect if this is a (generalized) projection.
+  -- See the comment about projections in this function's docstring.
+  if let some idx := argBIs.findIdx? (·.isInstImplicit) then
+    let argTy ← inferType argVars[idx]!
+    argTy.withApp fun c tyArgs => do
+      -- If this is of the form `C argVars[0] argVars[1] ... argVars[idx-1]`,
+      -- then we treat this instance as a projection; the arguments before this one are the type's parameters
+      if c.isConst && tyArgs.size == idx && Nat.all idx fun i _ => argVars[i]! == tyArgs[i]! then
+        assignMVarsIn (← inferType argMVars[idx]!)
+
   -- We start by assigning all metavariables in non-out-params of the return value.
   -- These are assumed to not be mvars during TC search (or at least not assignable)
   let tyOutParams ← getSemiOutParamPositionsOf ty
@@ -184,11 +200,6 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? 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
@@ -228,8 +239,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/synthorder.lean

@@ -24,3 +24,13 @@ 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.
+instance C1.toNonempty' {α : Type} [DecidableEq α] {inst : Inhabited α} [C1 α] : Nonempty α := ⟨default⟩

tests/lean/synthorder.lean.expected.out

@@ -19,3 +19,9 @@ all remaining arguments have metavariables:
       Three α β
       One β
       TwoHalf β
+[Meta.synthOrder] synthesizing the arguments of @C1.toNonempty in the order [2]:
+      C1 α
+synthorder.lean:36:0-36:104: error: cannot find synthesization order for instance @toNonempty' with type
+  ∀ {α : Type} [inst : DecidableEq α] {inst : Inhabited α} [inst : C1 α], Nonempty α
+all remaining arguments have metavariables:
+  @C1 α ?inst