declaration has metavariables

Stream: lean4

[pcpthm]

I read somewhere that Lean4 improved the elaboration algorithm and we can use the field notation in more places so:

#check (fun n => n.succ) Nat.zero

works in Lean4.
But the expression above doesn't work when used inside an inductive type definition:

-- > (kernel) declaration has metavariables 'Test.mk'
inductive Test : Nat → Type
| mk : Test ((fun n => n.succ) Nat.zero)

Is it a bug?

[Sebastian Ullrich]

Fixed in https://github.com/leanprover/lean4/commit/d4dc54a724

[Simon Winwood]

That commit broke this (I think):

inductive SortedMap {α : Type u} {β : Type v} [LessOrder α] : List (α × β) → Prop
  | nil : SortedMap []
  | cons : ∀ (k : α) (v : β) (l : List (α × β)),
           SortedMap l →
           l.Forall (λ (kv : (α × β)) => k < kv.fst) →
           -- N.B., HasLessOrder combined with this Forall implies
           -- no duplicate keys.
           SortedMap ((k,v)::l)

deps/galois_stdlib/src/Galois/Data/List.lean:54:10: error: typeclass instance problem contains metavariables
  LessOrder ?m.2558

[Simon Winwood]

This works in before this patch