fix: add workaround to prevent code explosion at deriving for FromJson

fixes #569

src/Init/Control/Except.lean

@@ -47,6 +47,11 @@ variable {ε : Type u}
   | Except.ok a    => Except.ok a
   | Except.error e => handle e
 
+def orElseLazy (x : Except ε α) (y : Unit → Except ε α) : Except ε α :=
+  match x with
+  | Except.ok a    => Except.ok a
+  | Except.error e => y ()
+
 instance : Monad (Except ε) where
   pure := Except.pure
   bind := Except.bind

src/Lean/Elab/Deriving/FromToJson.lean

@@ -124,7 +124,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
         let fromJsonFuncId := mkIdent ctx.auxFunNames[0]
         let discrs ← mkDiscrs header indVal
         let alts ← mkAlts indVal fromJsonFuncId
-        let mut auxCmd ← alts.foldrM (fun xs x => `($xs <|> $x)) (←`(Except.error "no inductive constructor matched"))
+        let mut auxCmd ← alts.foldrM (fun xs x => `(Except.orElseLazy $xs (fun _ => $x))) (←`(Except.error "no inductive constructor matched"))
         if ctx.usePartial then
           let letDecls ← mkLocalInstanceLetDecls ctx ``FromJson header.argNames
           auxCmd ← mkLet letDecls auxCmd

tests/lean/run/569.lean

@@ -0,0 +1,26 @@
+import Lean
+open Lean
+
+inductive Foo             -- 0.898 ms
+  | _01 (a b : Nat) : Foo -- 6.25 ms
+  | _02 (a b : Nat) : Foo -- 12.6 ms
+  | _03 (a b : Nat) : Foo -- 18.6 ms
+  | _04 (a b : Nat) : Foo -- 33.1 ms
+  | _05 (a b : Nat) : Foo -- 42.7 ms
+  | _06 (a b : Nat) : Foo -- 44.1 ms
+  | _07 (a b : Nat) : Foo -- 54.3 ms
+  | _08 (a b : Nat) : Foo -- 68 ms
+  | _09 (a b : Nat) : Foo -- 103 ms
+  | _11 (a b : Nat) : Foo -- 125 ms
+  | _12 (a b : Nat) : Foo -- 156 ms
+  | _13 (a b : Nat) : Foo -- 245 ms
+  | _14 (a b : Nat) : Foo -- 389 ms
+  | _15 (a b : Nat) : Foo -- 695 ms
+  | _16 (a b : Nat) : Foo -- 1.02 s
+  | _17 (a b : Nat) : Foo -- 1.82 s
+  | _18 (a b : Nat) : Foo -- 3.70 s
+  | _19 (a b : Nat) : Foo -- 9.95 s
+  | _20 (a b : Nat) : Foo -- 16.6 s
+  | _21 (a b : Nat) : Foo -- 34.2 s
+  | _22 (a b : Nat) : Foo -- 78.5 s
+  deriving FromJson