From 51a29098aba4fedb665e11d0063e7b2d06b55a46 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Nov 2022 09:35:51 -0800
Subject: [PATCH] fix: fixes #1852

---
 src/Lean/Class.lean      | 5 +++--
 tests/lean/run/1852.lean | 5 +++++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1852.lean

diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index f996ff1b5d4..38edc2a5e0a 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -88,13 +88,14 @@ def hasOutParams (env : Environment) (declName : Name) : Bool :=
 -/
 private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except String (Array Nat) :=
   match type with
-  | .forallE _ d b _ =>
+  | .forallE _ d b bi =>
     if d.isOutParam then
       let fvarId := { name := Name.mkNum `_fvar outParamFVarIds.size }
       let fvar      := mkFVar fvarId
       let b         := b.instantiate1 fvar
       checkOutParam (i+1) (outParamFVarIds.push fvarId) (outParams.push i) b
-    else if d.hasAnyFVar fun fvarId => outParamFVarIds.contains fvarId then
+    /- See issue #1852 for a motivation for `!bi.isInstImplicit` -/
+    else if !bi.isInstImplicit && d.hasAnyFVar fun fvarId => outParamFVarIds.contains fvarId then
       Except.error s!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`"
     else
       checkOutParam (i+1) outParamFVarIds outParams b
diff --git a/tests/lean/run/1852.lean b/tests/lean/run/1852.lean
new file mode 100644
index 00000000000..868f079fdb4
--- /dev/null
+++ b/tests/lean/run/1852.lean
@@ -0,0 +1,5 @@
+class foo (F : Type) where
+  foo : F
+
+class foobar (F : outParam Type) [foo F] where
+  bar : F