From 170166efbf6f5c31f76455a0ae406bcafe1a7958 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 17 Sep 2024 17:39:20 -0700
Subject: [PATCH] fix: modify projection instance binder info

closes #5333

This PR tries to address issue #5333.

My conjecture is that the binder annotations for `C.toB` and `Algebra.toSMul` are not ideal. `Algebra.toSMul` is one of declarations where the new command `set_synth_order` was used. Both classes, `C` and `Algebra`, are parametric over instances, and in both cases, the issue arises due to projection instances: `C.toB` and `Algebra.toSMul`. Let's focus on the binder annotations for `C.toB`. They are as follows:

```
C.toB [inst : A 20000] [self : @C inst] : @B ...
```

As a projection, it seems odd that `inst` is an instance-implicit argument instead of an implicit one, given that its value is fixed by `self`. We observe the same issue in `Algebra.toSMul`:

```
Algebra.toSMul {R : Type u} {A : Type v} [inst1 : CommSemiring R] [inst2 : Semiring A]
   [self : @Algebra R A inst1 inst2] : SMul R A
```

The PR changes the binder annotations as follows:

```
C.toB {inst : A 20000} [self : @C inst] : @B ...
```

and

```
Algebra.toSMul {R : Type u} {A : Type v} {inst1 : CommSemiring R} {inst2 : Semiring A}
    [self : @Algebra R A inst1 inst2] : SMul R A
```

In both cases, the `set_synth_order` is used to force `self` to be processed first.

In the MWE, there is no instance for `C ...`, and `C.toB` is quickly discarded. I suspect a similar issue occurs when trying to use `Algebra.toSMul`, where there is no `@Algebra R A ... ...`, but Lean spends unnecessary time trying to synthesize `CommSemiring R` and `Semiring A` instances. I believe the new binder annotations make sense, as if there is a way to synthesize `Algebra R A ... ...`, it will tell us how to retrieve the instance-implicit arguments.

Not sure what the impact will be on Mathlib.
---
 src/Lean/Meta/Instances.lean             |  9 +++++++--
 src/library/constructions/projection.cpp |  2 ++
 tests/lean/run/5333.lean                 | 20 ++++++++++++++++++++
 tests/lean/synthorder.lean.expected.out  |  7 -------
 4 files changed, 29 insertions(+), 9 deletions(-)
 create mode 100644 tests/lean/run/5333.lean

diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 604fc06d7d82..0fcdca9c5abe 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -195,8 +195,13 @@ def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : Meta
   let c ← mkConstWithLevelParams declName
   let keys ← mkInstanceKey c
   addGlobalInstance declName attrKind
-  let synthOrder ← computeSynthOrder c
-  instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
+  if let some info ← getProjectionFnInfo? declName then
+    trace[Meta.debug] "addInstance: {declName}, numParams: {info.numParams}"
+    let synthOrder := #[info.numParams]
+    instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
+  else
+    let synthOrder ← computeSynthOrder c
+    instanceExtension.add { keys, val := c, priority := prio, globalName? := declName, attrKind, synthOrder } attrKind
 
 builtin_initialize
   registerBuiltinAttribute {
diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp
index b9b964474463..a234c172fdb3 100644
--- a/src/library/constructions/projection.cpp
+++ b/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);
diff --git a/tests/lean/run/5333.lean b/tests/lean/run/5333.lean
new file mode 100644
index 000000000000..53f764e57391
--- /dev/null
+++ b/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
diff --git a/tests/lean/synthorder.lean.expected.out b/tests/lean/synthorder.lean.expected.out
index 707c333edea2..2f600056b123 100644
--- a/tests/lean/synthorder.lean.expected.out
+++ b/tests/lean/synthorder.lean.expected.out
@@ -11,13 +11,6 @@ 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 α
-      TwoHalf α
-[Meta.synthOrder] synthesizing the arguments of @Four.toThree in the order [4, 2, 3]:
-      Four α β
-      One β
-      TwoHalf β
 [Meta.synthOrder] synthesizing the arguments of @instFourOfThree in the order [4, 2, 3]:
       Three α β
       One β