Qq and `have`/`let`

Stream: general

[Jovan Gerbscheid]

Qq has this weird quirk where sometimes you have to write have instead of let, because Qq sometimes unfolds your let variables. Even though I know this I spent quite some time stuck on such a situation again recently. Is there a reason why this can't be fixed? My example is this, with an extremely confusing error message:

import Qq

open Lean Qq

def obtainExists (e : Expr) : MetaM String := do
  let_expr c@Exists α p := e | failure
  let u := c.constLevels![0]! -- use `have` instead of `let` to fix the error
  have α : Q(Sort $u) := α
  have p : Q($α → Prop) := p
  withLocalDeclDQ `α α fun a => do
  withLocalDeclDQ `h q($p $a) fun h => do
  let proof : Q(Exists $p) := q(Exists.intro $a $h)
/-
type mismatch
  Exists.intro «$a» «$h»
has type
  Exists «$p» : Prop
but is expected to have type
  Exists «$p» : Prop
-/
  sorry

[Eric Wieser]

The rule is that let is supposed to be reducible, but Qq doesn't know what to do if you unfold to a non-Qq object

[Anand Rao Tadipatri]

Here's another way of constructing the term that avoids the have statements:

import Qq

open Lean Qq

def obtainExists (e : Expr) : MetaM String := do
  let ⟨1, ~q(Prop), ~q(@Exists $α $p)⟩ ← inferTypeQ e |
    throwError "Expected {e} to be of the form `Exists ..`"
  withLocalDeclDQ `α α fun a => do
  withLocalDeclDQ `h q($p $a) fun h => do
  let proof : Q(Exists $p) := q(Exists.intro $a $h)
  sorry

[Jovan Gerbscheid]

Eric Wieser said:

The rule is that let is supposed to be reducible, but Qq doesn't know what to do if you unfold to a non-Qq object

But surely Qq could add a setting of Config.zetaDelta := false when elaborating?

[Eric Wieser]

What I mean is that this is intended behavior for let

[Eric Wieser]

With pp.all you get something a little stranger here:

type mismatch
  @Exists.intro.{_private.Init.GetElem.0.List.get!Internal._uniq.1289} «$α» «$p» «$a» «$h»
has type
  @Exists.{_private.Init.GetElem.0.List.get!Internal._uniq.1289} «$α» «$p» : Prop
but is expected to have type
  @Exists.{_private.Init.GetElem.0.List.get!Internal._uniq.1304} «$α» «$p» : Prop

[Jovan Gerbscheid]

I doubt that it is intended behaviour that in this example the second identical line fails:

import Qq

open Lean Qq

def obtainExists (e : Expr) : MetaM String := do
  let_expr c@Exists α p := e | failure
  let u := c.constLevels![0]!
  let α : Q(Sort $u) := α
  have p : Q($α → Prop) := p
  have p : Q($α → Prop) := p
  sorry

[Eric Wieser]

Right, let α : Q(Sort $u) := α is not allowed because the RHS is an Expr

[Eric Wieser]

If you type-cast between Expr and Qq, you have to use have

[Eric Wieser]

Using let tells Qq it is allowed to unfold, but if it unfolds then it finds itself with no type info

[Eric Wieser]

Obviously the error message is lousy

[Jovan Gerbscheid]

But my problem is that it does work (sometimes) to use let instead of have, so for a user it is really confusing. I didn't know that you always had to use have

[Jovan Gerbscheid]

And I don't understand the andvantage of unfolding lets

[Eric Wieser]

So you can do let x : Q(Nat) := q($y + $z), and get for free that $x is defeq to $y + $z

[Eric Wieser]

I also don't understand why in your example you get away with let the first time but not the second