noncomputable structure defaults cannot be marked noncomputable

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following code:

noncomputable def ohno := 1

structure OhNo where
  x := ohno

gives the error

failed to compile definition, consider marking it as 'noncomputable' because it depends on 'ohno', and it does not have executable code

As directed by the error message, after some consideration I tried to mark it noncomputable, but the following is not legal syntax:

noncomputable def ohno := 1

structure OhNo where
  x := noncomputable ohno

Neither OhNo.mk nor OhNo.x are noncomputable here; only the metadata used to populate the default arguments.

Context

Discussed on Zulip.
This example is contrived, but there are a very large number of noncomputable definitions in mathlib (many of which are only marked noncomputable because this avoids a very slow compilation pass).
Default structure initializers are rarely used in mathlib, so the impact is low

Steps to Reproduce

Run the code above

Expected behavior: Either lean emits no diagnostics, or it emits an error telling me how to fix the problem.

Actual behavior: Lean rejects the code above and leaves me with an unsolvable riddle about how to fix it.

Versions

[Output of lean --version in the folder that the issue occured in]
[OS version]

Impact

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