Lean.FromJson does not use default value when parsing structures

[lenianiva]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When a structure is deriving Lean.FromJson and has default values for its fields, parsing a json with those values missing will lead to an error.

Steps to Reproduce

Run the snippet with lean --run example.lean

import Lean.Data.Json

structure Small where
  id: Int := 0
  deriving Lean.ToJson
structure Big where
  id: Int := 0
  name: String := "name"
  deriving Lean.FromJson

def main: IO Unit := do
  let small: Small := { id := 123 }
  let src := Lean.toJson small
  IO.println src
  let obj: Except String Big := Lean.fromJson? src
  match obj with
  | .error error => IO.println s!"Cannot parse Json! {error}"
  | .ok obj => IO.println s!"Can parse json with name {obj.name}"

Expected behavior: Can parse json with name name

Actual behavior: Cannot parse Json! Big.name: String expected

Reproduces how often: Always

Versions

• Lean: Lean (version 4.0.0-nightly-2023-05-06, commit 445fd417be4d, Release)
• OS: 6.2.11-arch1-1

Additional Information

The last update to FromToJson.lean was 8 months ago so the version should be recent enough

[Kha]

I believe the JSON implementation was designed to be round-tripping, which means optional fields must be Options. In general, declarations in the Lean namespace are designed only for the purposes of Lean itself.

[Vtec234]

As far as using optional fields, keep in mind also that there is special treatment of fields postfixed with ?:

structure Test1 where
  a : Nat
  b : Option Nat := none
  c? : Option Nat := none
  deriving Lean.FromJson, Lean.ToJson

/- {"b": null, "a": 37} -/
#eval Lean.toJson { a := 37 : Test1 }