Error: unknown free variable and Qq

Stream: lean4

[Arend Mellendijk]

I ran into the following error message yesterday while writing meta code with Qq: unknown free variable '_fvar.541'. I spent far too much time scratching my head trying to see what I did wrong. I've minimised the issue down to this

import Qq

set_option autoImplicit false

open Lean Qq

inductive ExSum : Type
  | add {v : Level} (A : Q(Type v)) {a : Q($A)} : ExSum

def f {v : Level} (A : Q(Type v)) (a : Q($A)) : Unit × (Q($a = $a)) := sorry

example {v : Level} {A : Q(Type v)} {a : Q($A)} :
    ExSum → Unit
  | .add A =>
    let ⟨_, _⟩ := f A a
    ()

The problem here is that the a in the let statement belongs to the A that has been shadowed by the match statement. What I had intended to write was .add A (a := a), but the error message made this mistake difficult to debug.

I haven't been able to minimise any further. Removing the universe levels removes the error message completely, and removing Qq gives the expected type error.

Is this a known bug?

[Vasilii Nesterov]

The real problem is that v in the example's type and v in the type of A in the matching branch are not the same. This works for example:

example : ExSum → Unit
  | @ExSum.add _ A a =>
    let ⟨_, _⟩ := f A a
    ()

[Jovan Gerbscheid]

If you want Lean to automatically figure out that the v in ExSum.add is the same v then you should make v and A an argument of the type ExSum:

import Qq

set_option autoImplicit false

open Lean Qq

inductive ExSum (v : Level) (A : Q(Type v)) : Type
  | add (a : Q($A)) : ExSum v A

def f {v : Level} (A : Q(Type v)) (a : Q($A)) : Unit × (Q($a = $a)) := sorry

example {v : Level} {A : Q(Type v)} {a : Q($A)} :
    ExSum v A → Unit
  | .add a =>
    let ⟨_, _⟩ := f A a
    ()

[Arend Mellendijk]

This was actually the case in the un-minimised code. Here's something slightly less minimised that still gives the same error. It seems it's able to figure out that the v and A are the same as in the type of the ExSum but struggles with the a:

import Qq
open Lean Qq

inductive ExSum : ∀ {v: Lean.Level} (A : Q(Type v)), (e : Q($A)) → Type
  | zero {w : Lean.Level} {A : Q(Type w)} (z : Q($A)) : ExSum  A z
  | one : ExSum q(Nat) q((1 : Nat))
  | add {v w : Lean.Level} {A : Q(Type w)} {a : Q($A)} :
      ExSum A q($a)

def f {v : Level} (A : Q(Type v)) (a : Q($A)) : Unit × Q($a = $a) := sorry

example {u v : Level} {A : Q(Type v)} {a : Q($A)}
    (va : ExSum A a) :
    Unit :=
  match va with
  | .zero z =>
    ()
  | .one =>
    ()
  | .add =>
    let ⟨_, _⟩ := f A a
    ()

Weirdly this error is really unstable. Removing any of the constructors either gives a much clearer error message or makes the message go away completely.

To be clear I was eventually able to solve the issue in my case, but the error message made it much harder than it needed to be. I'm really just trying to figure out if this is a failure of error handling.

[Jovan Gerbscheid]

I don't know why, but replacing A with q($A) in the definition of ExSum.add seems to help

[Jovan Gerbscheid]

I've also often seen unknown variables when using Qq in the form of some _fvar.451 appearing in the expression, but without having an actual error.

[Eric Wieser]

In general replacing x with q($x) leads to better behavior in Qq, as it forces x to actually be elaborated into the expected type, either emitting error messages or assigning (universe) metavariables

[Eric Wieser]

(obviously this doesn't apply recursively to q($(q($(... x)))))