Universe issue when building expression

Stream: lean4

[Patrick Massot]

In

import Lean

open Lean Meta Elab Command Term

declare_syntax_cat mydecl
syntax "(" ident ":" term ")" : mydecl

def getIdent : TSyntax `mydecl → Ident
| `(mydecl| ($n:ident : $_t:term)) => n
| _ => default

def getType : TSyntax `mydecl → Term
| `(mydecl| ($_n:ident : $t:term)) => t
| _ => default

/-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
where `s` is preceded with universal quantifiers `∀ i : t`. -/
def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
| [] => return s

elab "Foo" decls:mydecl* ":" goal:term  : command => do
  let g ← liftMacroM $ mkGoalSyntax goal (decls.map (λ decl => (getIdent decl, getType decl))).toList
  dbg_trace (← liftTermElabM $ elabTerm g none)

Foo (x : Nat) (y : Nat) (h : y = x + 7) : 2*(x + 7) = 2*(x + 7)

I try to create in a complicated way the stupid expression ∀ (x y : Nat), y = x + 7 → 2*(x + 7) = 2*(x + 7) but, as can be seen from the dbg_trace output, Lean doesn't get the universe of Nat.

[Patrick Massot]

How could I fix that?

[Mario Carneiro]

It seems to have worked fine, you need to call instantiateMVars to remove the mvars from the expression though

[Patrick Massot]

Thanks!