Qq doesn't specialize expression with inferred type

Stream: metaprogramming / tactics

[Robert Maxton]

Consider the following:

import Qq

open Lean Elab Term Expr Qq


def assertTypeQ (e : Expr) {u : Level} (ty : Q(Sort $u)) : MetaM Q($ty) := do
  let typE ← checkTypeQ e ty
  if let some e' := typE then pure e'
  else throwError s!"expected type {ty}, got {←inferTypeQ e}"

set_option linter.constructorNameAsVariable false in
elab "ext% " thm:term : term => do
  let thm ← elabTerm thm none
  Meta.mapForallTelescope (fun body ↦ do
    let ⟨0, ~q(@Eq ((x  : $μ) → $ν x) $f $g), ~q($eq)⟩ ← inferTypeQ body |
      throwError "ext% tactic failed, expected a lemma proving `Eq ((x : α) → β x) f g`, got {body} : {← Meta.inferType body}"
    let eq ← assertTypeQ eq q($f = $g)
    return q((eq_iff_iff.mpr funext_iff) ▸ $eq)) thm

If we comment out the line let eq ← assertTypeQ eq q($f = $g), then this fails -- eq comes out of the let-match with an opaque/inaccessible type,  Q($x✝³), rather than with the expected type Q(@Eq ((x : $μ) → $ν x) $f $g) . $μ, $ν, $f, $g all get their types assigned properly, it's only the value that fails.