kernel error in inductive

Stream: lean4

[Jovan Gerbscheid]

I ran into the following strange bug:

structure A (α : Type) where
  private mk :: val : α

inductive B where
| b : A B → B
/-
(kernel) constant has already been declared '_private.«external:file:///MathlibDemo/MathlibDemo.lean».0.A.mk'
-/

[Mac Malone]

This is lean4#10789. Feel free to upvote that issue!