Weird unknown free variable '_uniq.419' error

[alexkeizer]

I'm running into a very weird error when using Qq, where the presence of

let args := a :: args

Causes an unknown free variable '_uniq.419' error in a different, seemingly unrelated line. When I inline the let binding, the error disappears.

I tested this with the latest version of qq (c71f94e) and lean4:nightly-2023-03-17

import Qq

open Qq
open Lean Meta Elab.Term

abbrev TypeFun.{u,v} (n : Nat) : Type ((max u v) + 1)
  := (Fin n → Type u) → Type v

def CurriedTypeFun.{u,v} : Nat → Type ((max u v) + 1)
  | 0   => ULift.{v+1,u+1} (Type u)
  | 1   => Type u → Type v
  | n+1 => Type u → CurriedTypeFun n

def TypeFun.ofCurried (F : CurriedTypeFun n) : TypeFun n
    := by sorry



def this_works : Expr → List Expr → TermElabM Expr
  | Expr.app F a, args => do
    -- let args := a :: args
    let depth : Nat := (a :: args).length
    
    let F : Q(CurriedTypeFun.{0,0} $depth) := F
    QQ.check F
    let F : Q(TypeFun.{0,0} $depth) := q(@TypeFun.ofCurried $depth $F)
    pure F
    
  | _,_ => throwError ""

def this_fails : Expr → List Expr → TermElabM Expr
  | Expr.app F a, args => do
    let args := a :: args
    let depth : Nat := args.length
    
    let F : Q(CurriedTypeFun.{0,0} $depth) := F
    QQ.check F
    let F : Q(TypeFun.{0,0} $depth) := q(@TypeFun.ofCurried $depth $F)
    -- error: unknown free variable '_uniq.419'    ----------------^^
    pure F
    
  | _,_ => throwError ""

EDIT: Ok, what seems to be happening is that Qq doesn't realize the second definition of args (i.e., the let-binding in question) is also of a quote-able type. So, it only add the first, supposed-to-be-inaccessible, definition of args to the local context inside the quotation. Then, since the definition of depth refers to the second definition of args, this is now an unknown free variable in the quotation context.

The local context of this_fails, at the point of error, is

$F✝«$a»: Expr
«$args»: List Expr
«$depth»: Nat := List.length _uniq.840
«$F»: CurriedTypeFun «$depth»
⊢ Nat

But when we add a type annotation to the second definition of args, suddenly the system realizes that it's quoteable.

def this_works₂ : Expr → List Expr → TermElabM Expr
  | Expr.app F a, args => do
    let args : List Expr := a :: args
    --       ^^^^^^^^^^^ Added annotation
    let depth : Nat := args.length
    
    let F : Q(CurriedTypeFun.{0,0} $depth) := F
    QQ.check F
    let F : Q(TypeFun.{0,0} $depth) := q(@TypeFun.ofCurried $depth $F)
    pure F
    
  | _,_ => throwError ""

Hence, the local context in the quotation now is

$F✝«$a»: Expr
$args✝: List Expr
«$args»: List Expr := «$a» :: $args✝
«$depth»: Nat := List.length «$args»
«$F»: CurriedTypeFun «$depth»
⊢ CurriedTypeFun «$depth»