default value of structure which is not produced by a tactic

Description

constructor of structure does not accept defalut value of field whose type is not Prop.

structure NonEmptyString where
  value : String
  another_value : Int := 0
  ev : value.length > 0 := by decide
deriving Repr

-- works
def eg : NonEmptyString := { value := "hello" }

-- does not work
def eg' : NonEmptyString := NonEmptyString.mk "hello"

-- default value of `another_value` is missing
/-
NonEmptyString.mk (value : String) (another_value : Int) (ev : value.length > 0 := by decide) : NonEmptyString
-/
#check NonEmptyString.mk

Steps to Reproduce

Expected behavior: accept defalut value for all types

Actual behavior: accept only Prop-value

Versions

nightly

Additional Information

reported on Zulip: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/default.20value.20of.20structure.20fields

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing the issue with the NonEmptyString example and inspect how structure constructors handle default-valued fields. Confirm the fix by checking that NonEmptyString.mk "hello" accepts the non-Prop default and that the existing Prop default still works.