import Init.Data.HashMap

def f (a : HashMap Nat Nat) : HashMap Nat Nat :=
a

def t (as : List Nat) :=
let xs := {};
/- We can't elaborate r.insert at this point because we don't know the type of `r`.
   Our plan is to suspend it by creating a metavariable, and resume later when we have
   more information. -/
let ys := as.foldl (fun r a => r.insert a) xs;
/- After elaborating `f xs`, we learn that `xs` has type `HashMap Nat Nat`. Then,
   we have enough information for resuming the elaboration of `r.insert a` -/
let zs := f xs;
ys