crash when using "by decide"

Stream: lean4

[Mark Wilhelm]

The last line of the following code causes a server crash in VS-code --

structure BreakfastStats where
  edible: Bool
  drinkable: Bool
  spreadable: Bool

inductive Breakfast: BreakfastStats -> Type where
| burrito: Breakfast {edible:=true, drinkable:=false, spreadable:=false}
| eggs: Breakfast {edible:=true, drinkable:=false, spreadable:=false}
| yogurt: Breakfast {edible:=true, drinkable:=true, spreadable:=true}
| cream_cheese: Breakfast {edible:=true, drinkable:=false, spreadable:=true}
| coffee: Breakfast {edible:=false, drinkable:=true, spreadable:=false}
open Breakfast

def eat (b: Breakfast T) (_: T.edible = true) : String :=
  match b with
  | burrito => "delicious"
  | eggs => "nice"
  | cream_cheese => "good with a bagel"
  | yogurt => "healthy i guess"

#eval eat burrito (by decide)
#eval eat coffee (by decide)

the stderr output is this --

[Error - 11:26:12 AM] Request textDocument/semanticTokens/full failed.
Error: Connection got disposed.
    at Object.dispose (/home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:560633)
    at Object.dispose (/home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:647247)
    at /home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:642942
    at runMicrotasks (<anonymous>)
    at processTicksAndRejections (node:internal/process/task_queues:96:5)
[Error - 11:26:12 AM] Request textDocument/documentSymbol failed.
Error: Connection got disposed.
    at Object.dispose (/home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:560633)
    at Object.dispose (/home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:647247)
    at /home/mark/.vscode-server/extensions/leanprover.lean4-0.0.95/dist/extension.js:2:642942
    at runMicrotasks (<anonymous>)
    at processTicksAndRejections (node:internal/process/task_queues:96:5)
Watchdog error: Got `shutdown` request, expected an `exit` notification
libc++abi: terminating with uncaught exception of type lean::exception: incomplete case
[Error - 11:26:13 AM] Request textDocument/documentSymbol failed.
  Message: Server process for file:///home/mark/pullbacks/Pullbacks.lean crashed, likely due to a stack overflow or a bug.
  Code: -32902

[Newell Jensen]

/me is feeling hungry now

[Gabriel Ebner]

lean4#1697