unknown free variable in v4.8.0

Stream: lean4

[pandaman]

Hi. I updated my project to v4.8.0 and started to get an unknown free variable: _kernel_fresh.19 error. Here is the MWE:

structure NFA where
  nodes : Array Nat

def get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Nat :=
  nfa.nodes[i]

-- "unknown free variable: _kernel_fresh.19" at instance
instance : GetElem NFA Nat Nat (fun nfa i => i < nfa.nodes.size) where
  getElem := get

Spelling out all arguments of getElem like getElem nfa i h := get nfa i h seems to fix the issue though.

[Kim Morrison]

@pandaman, can you please report this as an issue on the lean4 repository?

[pandaman]

Opened https://github.com/leanprover/lean4/issues/4418

[Kim Morrison]

Could you please add which version you were upgrading from (i.e. where this code used to work?)

[pandaman]

Added the original version (v4.6.0)!