confusing error with quote4

Stream: lean4

[Tomas Skrivan]

I wanted to try out quote4 library but I'm having hard time using its antiquotations. I really do not understand why am I getting the error here:

import Qq open Qq Lean

def FinExpr :=
  let n := q(10)
  q(Fin $n) -- works fine

def FinExpr' : Q(Type) :=
  let n := q(10)
  q(Fin $n) -- unknown identifier '«$n»'

[Kyle Miller]

Maybe let bindings are handled differently depending on whether there's an expected type or not (both for the whole let and for the thing being defined)?

These work for example:

def FinExpr' : Q(Type) :=
  let n : Q(Nat) := q(10)
  q(Fin $n)

def FinExpr'' (n : Q(Nat)) : Q(Type) :=
  q(Fin $n)

[Tomas Skrivan]

Odd, this also does not work

def n : Q(Nat) := q(10)
def FinExpr''' : Q(Type) := q(Fin $n)

[Mario Carneiro]

that's expected, the quote macro only lifts things in the local context into the inner state

[Tomas Skrivan]

Ok that makes sense.

Another odd thing:

This works:

#eval show MetaM Unit from do
  let a? ← mkFreshExprMVar q(Nat)
  let b? ← mkFreshExprMVar q(Nat)
  pure ()

This does not:

#eval show MetaM Unit from do
  let a? ← mkFreshExprMVarQ q(Nat)
  let b? ← mkFreshExprMVarQ q(Nat) -- incompatible metavariable _uniq.146616
  pure ()

What is the difference?

[Mario Carneiro]

One thing to watch out for is that there is a difference between QQ e and QQ (QQ.qq e) but these are pretty printed the same way. QQ.qq is an identity wrapper which is used for pretty printing(?) and is generated by q(e) expressions. When you use Q(e) it just creates QQ e, but if you have a function def foo (A : Q(Type)) : QQ A then foo q(e) will have type QQ (QQ.qq e)

[Mario Carneiro]

In your first example the type of FinExpr is QQ (QQ.qq e) and in the second one it is QQ e

[Tomas Skrivan]

Mario Carneiro said:

In your first example the type of FinExpr is QQ (QQ.qq e) and in the second one it is QQ e

How can I see that? I set set_option pp.all false and I still see Q(Type) as the type of FinExpr

[Mario Carneiro]

you want pp.all true

[Mario Carneiro]

That doesn't seem to explain the difference though, you get the same result with a type ascription of QQ q(Type) instead of Q(Type)

[Mario Carneiro]

BTW, when looking at Qq.QQ (@Qq.QQ.qq ...) I am reminded of https://esolangs.org/wiki/OOo_CODE...

[Gabriel Ebner]

def FinExpr' : Q(Type) :=
  let n := q(10)
  q(Fin $n) -- unknown identifier '«$n»'

This is an unfortunate issue with elaboration order. Apparently we don't yet know the type of n when elaborating the q(Fin $n), so quote4 doesn't know that it can unquote that hypothesis. We should probably postpone until the types of all assumptions are known.

[Gabriel Ebner]

The reason it works in the first example is presumably because we postpone to wait for the expected type.

[Tomas Skrivan]

How do I get this working? Even with explicit types it does not work:

#eval show MetaM Unit from do
  let f? : Q(Nat→Nat) ← mkFreshExprMVar q(Nat→Nat)
  let lhs : Q((Fin 10 → Nat)→Nat) := q(λ (x : Fin 10 → Nat) i => $f x i) -- unknown identifier '«$f»'
  IO.println s!"{← Meta.ppExpr lhs}"

[Gabriel Ebner]

Tomas Skrivan said:

Odd, this also does not work

def n : Q(Nat) := q(10)
def FinExpr''' : Q(Type) := q(Fin $n)

This is a bug, at the moment we assume that $n refers to a free variable. You can write $((n)) as a workaround.

[Gabriel Ebner]

QQ.qq is an identity wrapper which is used for pretty printing(?)

The wrapper is used to tag an expression with a type; if you have a bare Expr you don't know if it's supposed to denote a Nat or something else. At some point in the past QQ used to be a structure, and qq was its constructor. Maybe we should get back to that.

[Gabriel Ebner]

Tomas Skrivan said:

How do I get this working? Even with explicit types it does not work:

#eval show MetaM Unit from do
  let f? : Q(Nat→Nat) ← mkFreshExprMVar q(Nat→Nat)
  let lhs : Q((Fin 10 → Nat)→Nat) := q(λ (x : Fin 10 → Nat) i => $f x i) -- unknown identifier '«$f»'
  IO.println s!"{← Meta.ppExpr lhs}"

You've got a typo here. It needs to be $f? and not $f. Also lhs doesn't type-check ($f? takes one argument, not two).

[Mario Carneiro]

I think if Q(e) generated a term of the form QQ (QQ.qq e) then there would be fewer discrepancies here

[Gabriel Ebner]

there is a difference between QQ e and QQ (QQ.qq e)

Does this cause any issues? If anything, it should always be QQ e since e is an argument of type Expr.

[Tomas Skrivan]

Gabriel Ebner said:

You've got a typo here. It needs to be $f? and not $f. Also lhs doesn't type-check ($f? takes one argument, not two).

Good, totally my mistake. It works:

#eval show MetaM Unit from do
  let f? : Q(Nat→Nat) ← mkFreshExprMVar q(Nat→Nat)
  let lhs := q(λ (x : Fin 10 → Nat) i => $f? (x i))
  let rhs := q(λ (x : Fin 10 → Nat) i => Nat.succ (x i))
  IO.println s!"{← isDefEq lhs rhs}: {← Meta.ppExpr lhs} =?= {← Meta.ppExpr rhs}"

I'm trying to use it to test out some unification problems.

[Mario Carneiro]

Gabriel Ebner said:

there is a difference between QQ e and QQ (QQ.qq e)

Does this cause any issues? If anything, it should always be QQ e since e is an argument of type Expr.

It does; a lot of the time when I call synthInstanceQ or other similar functions I have to write something like let inst : Q(e) <- synthInstanceQ q(e) and I have to repeat the e, because if I leave off the : Q(e) then the binding gets the doubled QQ type and it won't be picked up by later q(_) invocations

[Gabriel Ebner]

let inst : Q(e) <- synthInstanceQ q(e)

That pattern occurs only three times in mathlib, and in all three instances it's a workaround for the "incompatible metavariable" issue. Do you have another example?

[Mario Carneiro]

Yes, I noticed that as well upon searching. On the other hand, I notice that synthInstanceQ always needs a type ascription as in synthInstanceQ (q(OrderedRing $α) : Q(Type u)), do you know whether this is related?

[Gabriel Ebner]

Yes that's the incompatible metavariable issue. Quote4 expects all metavariables to have the same local context, but abstracting local variables can change the local context of an maar (at least that's what I think is happening here)