Unexpected "invalid universe level" error using implicit variables

[mdempsky]

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

Using an implicit variable (e.g., variable {cvar : kind -> Type}) leads to an unexpected "invalid universe level" later on.

Context

I'm trying to port Ur/Web's "Featherweight Ur" specification (https://github.com/urweb/urweb/tree/master/src/coq) from Coq to Lean to gain familiarity with Lean, and I ran into this unexpected error message.

Steps to Reproduce

1. Minimal reproducer:

inductive kind : Type where
| KType

section subs

variable {cvar : kind -> Type}

inductive con: kind -> Type where
| CVar : forall {k}, cvar k -> con k

variable {k1} (c1 : con k1)

inductive subs : forall {k2}, (cvar k1 -> con k2) -> con k2 -> Type where
| S_Unchanged : forall {k2} (c2 : con k2), subs (fun _ => c2) c2

end subs

Expected behavior: [Clear and concise description of what you expect to happen]

The definition is accepted.

Actual behavior: [Clear and concise description of what actually happens]

Lean reports:

invalid universe level in constructor 'subs.S_Unchanged', parameter has type
  {k2 : kind} → kind → Type
at universe level
  2
it must be smaller than or equal to the inductive datatype universe level
  1

Versions

[Output of #eval Lean.versionString]

"4.11.0"

[OS version, if not using live.lean-lang.org.]

macOS Sequoia 15.1

Additional Information

The error message goes away if cvar k1 -> con k2 is changed to cvar k1 -> @con cvar k2, as in:

inductive subs : forall {k2}, (cvar k1 -> @con cvar k2) -> con k2 -> Type where
...

Note that this appears to be the only instance of con k2 that needs its cvar parameter explicitly provided.

Impact

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