Nested names confuse the typechecker

[mrakgr]

def nat.foldl.fin.template {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, buffer.lt_aux_1 lt ⟩ in f n' (nat.foldl.fin.template n' s f)

def nat.foldl.fin {α : Type} : ∀ (n : nat) (s : α) (f : fin n → α → α), α
| 0 s f := s
| (n+1) s f := 
    let n' : fin (n+1) := ⟨ n, lt_add_one n ⟩ in
    f n' (nat.foldl.fin.template (n+1) n' s f)

invalid field notation, type is not of the form (C ...) where C is a constant
  nat.foldl.fin
has type
  Π (n : ℕ), α → (fin n → α → α) → α

Suppose I do this...

def nat.foldl.qwe {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, buffer.lt_aux_1 lt ⟩ in f n' (nat.foldl.qwe n' s f)

def nat.foldl.fin {α : Type} : ∀ (n : nat) (s : α) (f : fin n → α → α), α
| 0 s f := s
| (n+1) s f := 
    let n' : fin (n+1) := ⟨ n, lt_add_one n ⟩ in
    f n' (nat.foldl.qwe (n+1) n' s f)

It starts working. The following also works for me.

def nat.foldl.fin.template {α : Type} (n' : nat) : ∀ (n : fin n') (s : α) (f : fin n' → α → α), α
| ⟨0, _⟩ s f := s
| ⟨n+1, lt⟩ s f := let n' : fin n' := ⟨n, buffer.lt_aux_1 lt ⟩ in f n' (nat.foldl.fin.template n' s f)

def nat.foldl.fin {α : Type} : ∀ (n : nat) (s : α) (f : fin n → α → α), α
| 0 s f := s
| (n+1) s f := 
    let n' : fin (n+1) := ⟨ n, lt_add_one n ⟩ in
    f n' (@nat.foldl.fin.template _ (n+1) n' s f)

This is Lean 3.42.

[cipher1024]

Can you minimize the example further and post it to https://github.com/leanprover-community/lean please? This is the version where we integrate fixes.