Meta helper for filling universe meta-variables?

Stream: lean4

[Siddhartha Gadgil]

These are experiments and probably not the intended way for lean to be used, but I was trying to cache expressions and define using them. My question is does lean have something like isDefEq(in the sense of solving for meta-variables) but which assigns (level) meta-variables to make a well-formed expression.

To clarify, here is the code for saving and loading:

initialize exprCache : IO.Ref (HashMap Name Expr) ← IO.mkRef (HashMap.empty)

def getCached? (name : Name) : IO (Option (Expr)) := do
  let cache ← exprCache.get
  return (cache.find? name)

def cache (name: Name)(e: Expr)  : IO Unit := do
  let cache ← exprCache.get
  exprCache.set (cache.insert name e)
  return ()

syntax (name:= saveexpr) "cache!" term "at" ident : term
@[termElab saveexpr] def cacheImp : TermElab :=
  fun stx expectedType? =>
  match stx with
  | `(cache! $t at $name) =>
    do
      let t ← Term.elabTerm t none
      let t ← whnf t
      let name ← name.getId
      cache name t
      return t
  | _ => throwIllFormedSyntax

syntax (name:= loadexpr) "load!" ident :term
@[termElab loadexpr] def loadImp : TermElab :=
  fun stx expectedType? =>
  match stx with
  | `(load! $name) =>
    do
      let name ← name.getId
      let cache ← exprCache.get
      let e ← cache.find? name
      match e with
      | some e =>
        return  e
      | none => throwError "no such expression"
  | _ => throwIllFormedSyntax

set_option pp.all true

#check cache! (fun (x: Nat) => x * (2: Nat)) at func
#check (load! func)

-- gives fun (x : Nat) => @HMul.hMul.{u_1, u_2, u_3} Nat Nat Nat (@instHMul.{0} Nat instMulNat) x (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) : Nat → Nat

def fff := load! func -- gives rror:
/- application type mismatch
  @HMul.hMul.{u_1, u_2, u_3} Nat
argument has type
  Type
but function has type
  {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → [self : HMul.{u_1, u_2, u_3} α β γ] → α → β → γ
-/

For the expression to be valid assignments u_i =levelOne need to be made. When I had similar issues with mkAppM, the solution I was told (which worked very well, thanks) was to use elabAppArgs. I was wondering if there is an elaborator method for this case of the same nature.

Thanks for any help,
Siddhartha