fix: add checkSystem and withIncRecDepth to withAutoBoundImplicit

Fix stack overflow crash.

Closes #4117

The fix can be improved: we could try to avoid creating hundreds of
auto implicits before failing.

src/Lean/Elab/Term.lean

@@ -1523,7 +1523,8 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
   let flag := autoImplicit.get (← getOptions)
   if flag then
     withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) do
-      let rec loop (s : SavedState) : TermElabM α := do
+      let rec loop (s : SavedState) : TermElabM α := withIncRecDepth do
+        checkSystem "auto-implicit"
         try
           k
         catch

tests/lean/4117.lean

@@ -0,0 +1 @@
+structure D:=(t:A)(c N:={s with} 0

tests/lean/4117.lean.expected.out

@@ -0,0 +1 @@
+4117.lean:2:0: error: unexpected end of input; expected ')'

tests/lean/run/simpDiag.lean

@@ -35,8 +35,8 @@ info: [simp] used theorems (max: 1201, num: 3):
   ⏎
   Nat.reduceAdd (builtin simproc) ↦ 771
   ⏎
-  ack.eq_1 ↦ 768[simp] tried theorems (max: 1974, num: 2):
-    ack.eq_3 ↦ 1974, succeeded: 1201
+  ack.eq_1 ↦ 768[simp] tried theorems (max: 1973, num: 2):
+    ack.eq_3 ↦ 1973, succeeded: 1201
   ⏎
   ack.eq_1 ↦ 768, succeeded: 768use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
 ---