confusing Qq error

Stream: lean4

[David Renshaw]

This does not work:

import Lean
import Qq.Match
open Qq
open Lean

def foo (e : Expr) : MetaM Unit := do
  let e' : Q(Prop) := e
  match e' with
  | ~q($a ≠ $b) => pure ()
  | _ => pure ()

It gives the error

Expected type:
e : Expr
⊢ MetaM Unit
Messages here (1)
29:2:
unquoteExpr: e : Expr
Messages above (2)
25:0:
LocalDecl : Type
27:4:
application type mismatch
  sorryAx (MetaM Unit)
argument has type
  Type
but function has type
  (α : Sort u_1) → optParam Bool false → α

It does work if I add a monadic bind:

def foo' (e : Expr) : MetaM Unit := do
  let e' : Q(Prop) ← pure e
  match e' with
  | ~q($a ≠ $b) => pure ()
  | _ => pure ()

I'm confused about what's going wrong in foo, the first example. I guess maybe the Q() macro is trying to parse more input that I've given it, so it's pulling from the next line too, somehow?

[Gabriel Ebner]

Yes, the q() macro tries to reduce the types, which means that e' gets unfolded to e if it's a let-binding. And then it no longer knows what type the expression e has. (Because it has type Expr and not Q(Prop).)

[Gabriel Ebner]

We've been talking about making let non-dependent for a long time (i.e., so it would be like have), which would address this issue.

[David Renshaw]

hm... so the problem is that the matcher macro ~q has too much information?

[Gabriel Ebner]

Yes!

[David Renshaw]

I'm putting my cursor over that part of the code, and the difference I see is that in the foo case we have

e : Expr
e' : QQ (Expr.sort Level.zero) := e
⊢ MetaM Unit

and in the foo' case we have just

e : Expr
⊢ MetaM Unit

i.e. the e' is gone.

[Gabriel Ebner]

I think you just have the cursor on the wrong position. This is what I get for foo':

▶ expected type (6:9-6:11)
e : Expr
e' : Q(Prop)
⊢ Q(Prop)

[David Renshaw]

Is the bind that I've added (← pure e) the best way to work around this problem for now?

[Gabriel Ebner]

Probably.

[David Renshaw]

I suppose I can finesse my function declarations so that all of the casting happens at function calls to sidestep the problem.

[Mario Carneiro]

I've been using carefully positioned have statements instead of let in QQ programs to make sure it doesn't unfold stuff it shouldn't

[Mario Carneiro]

unfortunately have isn't a doElem though so you have to reorganize things sometimes