Update src/Lean/Meta/Instances.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

src/Lean/Meta/Instances.lean

@@ -113,8 +113,34 @@ For example:
     (because A B are out-params and are only filled in once we synthesize 2)
 
 (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
+information in projections. See PR #5376 and issue #5333. Before PR
+#5376, given a class `C` at
+```
+class A (n : Nat) where
+
+instance [A n] : A n.succ where
+
+class B [A 20050] where
+
+class C [A 20000] extends B where
+```
+we would get the following instance
+```
+C.toB [inst : A 20000] [self : @C inst] : @B ...
+```
+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`.
 -/
-private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
+private partial def computeSynthOrder (inst : Expr) (projInfo? : Option ProjectionFunctionInfo) : MetaM (Array Nat) :=
   withReducible do
   let instTy ← inferType inst
 
@@ -151,7 +177,8 @@ private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   let tyOutParams ← getSemiOutParamPositionsOf ty
   let tyArgs := ty.getAppArgs
   for tyArg in tyArgs, i in [:tyArgs.size] do
-    unless tyOutParams.contains i do assignMVarsIn tyArg
+    unless tyOutParams.contains i do
+      assignMVarsIn tyArg
 
   -- Now we successively try to find the next ready subgoal, where all
   -- non-out-params are mvar-free.
@@ -159,7 +186,13 @@ private partial def computeSynthOrder (inst : Expr) : MetaM (Array Nat) :=
   let mut toSynth := List.range argMVars.size |>.filter (argBIs[·]! == .instImplicit) |>.toArray
   while !toSynth.isEmpty do
     let next? ← toSynth.findM? fun i => do
-      forallTelescopeReducing (← instantiateMVars (← inferType argMVars[i]!)) fun _ argTy => 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 argTyArgs := argTy.getAppArgs
@@ -195,7 +228,8 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let synthOrder ← computeSynthOrder c
+  let projInfo? ← getProjectionFnInfo? declName
+  let synthOrder ← computeSynthOrder c projInfo?
   instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize

src/Lean/ProjFns.lean

@@ -21,7 +21,7 @@ structure ProjectionFunctionInfo where
   i : Nat
   /-- `true` if the structure is a class. -/
   fromClass : Bool
-  deriving Inhabited
+  deriving Inhabited, Repr
 
 @[export lean_mk_projection_info]
 def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=

src/library/constructions/projection.cpp

@@ -63,6 +63,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
             // 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit.
             // 2. It is not originally an outparam. Outparams must be implicit.
             bi = mk_binder_info();
+        } else if (is_inst_implicit(bi_orig) && inst_implicit) {
+            bi = mk_implicit_binder_info();
         }
         expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi);
         cnstr_type = instantiate(binding_body(cnstr_type), param);

tests/lean/run/5333.lean

@@ -0,0 +1,20 @@
+class A (n : Nat) where
+
+instance [A n] : A n.succ where
+
+class B [A 20050] where
+
+set_option trace.Meta.debug true
+
+class C [A 20000] extends B where
+
+#check C.toB
+
+instance : A 20050 where
+
+class D where
+
+instance inst1 : D where
+instance inst2 [B] : D where
+
+#synth D

tests/lean/run/synthOrderRegression.lean

@@ -0,0 +1,19 @@
+-- Artificial example for exposing a regression introduced while working on PR #5376
+-- fix: modify projection instance binder info
+
+class Foo (α : Type) [Add α] where
+   bla : [Mul α] → BEq α
+
+attribute [instance] Foo.bla
+
+inductive Boo where
+  | unit
+
+instance : Add Boo where
+  add _ _ := .unit
+
+instance : Mul Boo where
+  mul _ _ := .unit
+
+def f [Foo Boo] (a b : Boo) : Bool :=
+  a == b

tests/lean/synthorder.lean.expected.out

@@ -11,13 +11,10 @@ all remaining arguments have metavariables:
       Foo A B
       Foo B C
 [Meta.synthOrder] synthesizing the arguments of @instFooOption in the order []:
-[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [1, 2]:
-      One α
+[Meta.synthOrder] synthesizing the arguments of @TwoHalf.toTwo in the order [2]:
       TwoHalf α
-[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4, 2, 3]:
+[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4]:
       Four α β
-      One β
-      TwoHalf β
 [Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
       Three α β
       One β