derived Repr don't work with structure with extern fields

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

[Description of the issue]

Steps to Reproduce

Use this repo:
https://github.com/locriacyber/debug-lean-derived-repr-extern

Expected behavior:

{ x := 1.000000, y := 1.000000 }
1.000000
2.000000

Actual behavior:

{ x := 0.000000, y := 0.000000 }
1.000000
2.000000

Reproduces how often: 100%

Versions

Lean (version 4.0.0, Release) (is latest master commit)
Linux x86_64

Additional Information

Pasting the code generated by elaboration works.

structure Vector2 where
  mk ::
  x : Float
  y : Float
deriving Inhabited

-- from
-- set_option trace.Elab.definition true in
-- deriving instance Repr for Vector2
instance : Repr Vector2 where
  reprPrec :=
    fun x prec =>
      Std.Format.bracket "{ "
        (Std.Format.nil ++ Std.Format.text "x" ++ Std.Format.text " := " ++
                    Std.Format.group (Std.Format.nest 5 (repr x.x)) ++
                  Std.Format.text "," ++
                Std.Format.line ++
              Std.Format.text "y" ++
            Std.Format.text " := " ++
          Std.Format.group (Std.Format.nest 5 (repr x.y)))
        " }"

attribute [extern "lean_raylib__Vector2_mk"] Vector2.mk
attribute [extern "lean_raylib__Vector2_x"] Vector2.x
attribute [extern "lean_raylib__Vector2_y"] Vector2.y

Start by reproducing the issue with the linked debug-lean-derived-repr-extern repository and compare the derived Repr output with the pasted elaborated instance. Inspect the generated Repr and the extern attributes for Vector2; done means the derived representation preserves the expected x and y values while the existing reproduction remains valid.