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

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.

Start by running the minimal Pointed examples from the issue against the reported Lean nightly version and compare them with constructors whose parameters are implicit. Trace the anonymous constructor notation elaboration and ensure explicit constructor parameters are handled so both examples compile without errors.