From 0d5c5e0191e112e4ff976041a2c6f2b8be4f51f6 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 7 Jul 2023 17:30:58 +1000
Subject: [PATCH] feat: relax test in checkLocalInstanceParameters to allow
 instance implicits

---
 src/Lean/Elab/Binders.lean | 5 ++++-
 tests/lean/run/2311.lean   | 4 ++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/2311.lean

diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 6ba8fbdb84..6f5ab35c6d 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -182,7 +182,10 @@ register_builtin_option checkBinderAnnotations : Bool := {
 /-- Throw an error if `type` is not a valid local instance. -/
 private partial def checkLocalInstanceParameters (type : Expr) : TermElabM Unit := do
   let .forallE n d b bi ← whnf type | return ()
-  if !b.hasLooseBVar 0 then
+  -- We allow instance arguments so that local instances of the form
+  -- `variable [∀ (a : α) [P a], Q a]`
+  -- are accepted, per https://github.com/leanprover/lean4/issues/2311
+  if bi != .instImplicit && !b.hasLooseBVar 0 then
     throwError "invalid parametric local instance, parameter with type{indentExpr d}\ndoes not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter."
   withLocalDecl n bi d fun x => checkLocalInstanceParameters (b.instantiate1 x)
 
diff --git a/tests/lean/run/2311.lean b/tests/lean/run/2311.lean
new file mode 100644
index 0000000000..1eb86c84ac
--- /dev/null
+++ b/tests/lean/run/2311.lean
@@ -0,0 +1,4 @@
+class P (n : Nat)
+class Q (n : Nat)
+variable [∀ (n : Nat) [P n], Q n]
+example [P 7] : Q 7 := inferInstance