Declaration has free variables in mk.injEq

[semorrison]

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

There is an unexpected error on structures parametrised by certain equality proofs:

-- (kernel) declaration has free variables 'O.mk.injEq'
structure O (c : False = False) where
  m : Prop

Expected behavior:

Accept the declaration

Actual behavior:

Error (kernel) declaration has free variables 'O.mk.injEq'.

Reproduces how often:

@digama0 pointed out the curious workaround:

set_option genInjectivity false in
structure O (c : False = False) where
  m : Prop
gen_injective_theorems% O

Versions

Lean (version 4.0.0-nightly-2023-03-31, commit 742d053a97bd, Release)