anonymous ctor notation fails on constructors of type families with explicit params

[cppio]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The anonymous constructor notation ⟨...⟩ fails to pass parameters to the constructor when the constructor requires that parameters be passed explicitly.

Steps to Reproduce

inductive Pointed : Type → Type
  | mk α : α → Pointed α

example : Pointed Bool := ⟨false⟩
example : Pointed (String × Nat) := ⟨"", 0⟩

Expected behavior: The code should succeed with no errors, as it does when α is an implicit parameter to mk.

Actual behavior: The code results in the following errors:

application type mismatch
  Pointed.mk false
argument
  false
has type
  Bool : Type
but is expected to have type
  Type : Type 1

invalid constructor ⟨...⟩, expected type must be an inductive type 
  Type

Versions

Lean 4.16.0-nightly-2025-01-06
Appears in Lean 4.0.0-m5, though I did not check before this.

Impact

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

[nomeata]

With the explicit parameter I'd have expected

example : Pointed Bool := ⟨Bool, false⟩

to work, but that doesn't work.

NB: your example works with

inductive Pointed : Type → Type
  | mk {α} : α → Pointed α

Is that a suitable workaround for you?

[cppio]

The current implementation and error messages mention explicit fields rather than parameters, but it would be fine either way. I would expect one of ⟨⟩ and ⟨_⟩ to work in place of rfl.

[nomeata]

Is it maybe the case that the implementation assumes a structure, as in

structure Pointed (α : Type) : Type where
 val : α

/-- info: Pointed.mk {α : Type} (val : α) : Pointed α -/
#guard_msgs in
#check Pointed.mk

example : Pointed Bool := ⟨false⟩
example : Pointed (String × Nat) := ⟨"", 0⟩

and the fact that it even supports non-structures is the oversight here?

Ah, but https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#anonymous-constructor-syntax is pretty explicit that this feature should work for inductive as well.

If we take the reference manual at the source of truth, then I’d say that

example : Pointed Bool := ⟨Bool, false⟩

should work.