fix: fixes #1852

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

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