Explicit constructor arguments become implicit

Stream: lean4

[Kyle Miller]

I was wondering whether it was expected that constructor arguments could be forced to become implicit:

inductive thing : Type _ → Type _
| nil (α : Type _) : thing α

#print thing.nil
-- constructor thing.nil.{u_1} : {α : Type u_1} → thing α

This happens when it's in this form too:

inductive thing : Type _ → Type _
| nil : (α : Type _) → thing α

[Leonardo de Moura]

Are you using the latest version? I get

thing.nil.{u_1} : (α : Type u_1) → thing α

in both cases.

[Kyle Miller]

Oh, sorry for the noise, I forgot my lean4:nightly was almost two weeks old -- it works fine on the latest version. Thanks.

[Yury G. Kudryashov]

I'm trying to define a structure with an unused type argument (it will be used for class instances):

structure MySigma {α : Type _} (β : Type _) (γ : α → Type _) where
  fst : α
  snd : γ fst

Is it possible to make β in MySigma.mk explicit without turning it into an inductive and manually defining projections?

[Yury G. Kudryashov]

In Lean 3 it was possible to write

structure my_sigma {α : Type*} (β : Type*) (γ : α → Type*) := mk [] ::
(fst : α)
(snd : γ fst)

[Yury G. Kudryashov]

What are other options? Define a reducible MySigma.mk' that takes an explicit argument β? Something else?