LCNF local context contains unused local variable declaratio

Stream: lean4

[Marc Huisinga]

MWE:

class NameableType (τ : Type) where
  name : String

instance : NameableType String where
  name := "String"

instance [inst : NameableType α] : NameableType (Array α) where
  name :=
    if inst.name.contains ' ' then
      s!"Array ({inst.name})"
    else
      s!"Array {inst.name}"

-- LCNF local context contains unused local variable declaration `_x.10`
def foo : String :=
  NameableType.name (Array String)

[Leonardo de Moura]

Fixed https://github.com/leanprover/lean4/commit/135790f41a4d937941acda0173760d2d70ca7d8a