invalid reference to undefined universe level parameter with inductiveCheckResultingUniverse false

[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

When using bootstrap.inductiveCheckResultingUniverse false, there is a kernel error when building a structure

Context

Related Zulip message

Steps to Reproduce

1. Run

   set_option bootstrap.inductiveCheckResultingUniverse false in
   structure Wrap.{u} (α : Sort u) : Sort u where
     val : α

Expected behavior: No diagnostics

Actual behavior:

(kernel) invalid reference to undefined universe level parameter 'u'

Surprisingly, #check Wrap works fine; so the error is coming from generation of some auxiliary declaration.

Versions

4.6.0-rc1

Impact

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

[Kha]

bootstrap comes without warranty :)