From 4dbb3e6db1af91c653820d33417b6fc42a349e07 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Aug 2021 06:54:34 -0700
Subject: [PATCH] fix: add workaround to prevent code explosion at `deriving`
 for `FromJson`

fixes #569
---
 src/Init/Control/Except.lean           |  5 +++++
 src/Lean/Elab/Deriving/FromToJson.lean |  2 +-
 tests/lean/run/569.lean                | 26 ++++++++++++++++++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/569.lean

diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 13fd5ec154..01554eb2d5 100644
--- a/src/Init/Control/Except.lean
+++ b/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
diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 973748f7d0..08905d93f1 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/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
diff --git a/tests/lean/run/569.lean b/tests/lean/run/569.lean
new file mode 100644
index 0000000000..f8e7e93826
--- /dev/null
+++ b/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