Optional parameters make nested inductives fail to elaborate

[kmill]

Description

If a nested inductive goes through a type that has an optional parameter, there is an "application type mismatch" failure from the inductive command.

Steps to Reproduce

inductive A (α : Type)
 | mk (x : Option α := none)

inductive B where
  | node (children : A B)

Expected behavior: No errors

Actual behavior:

application type mismatch
  optParam _nested.Option_2 none
argument has type
  Option B
but function has type
  _nested.Option_2 → Type

Versions

Lean 4.11.0 nightly from 7/22/2024

Impact

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