Zulip Chat Archive

Stream: mathlib4

Topic: Using `QQ` when you only have an `Expr`


Scott Morrison (Oct 11 2022 at 00:47):

A question for @Gabriel Ebner, about your example from QQ:

import Qq
open Qq Lean

partial def summands {α : Q(Type $u)} (inst : Q(Add $α)) :
    Q($α)  MetaM (List Q($α))
  | ~q($x + $y) => return ( summands inst x) ++ ( summands inst y)
  | n => return [n]

If I have a mere e : Expr, which I happen to believe is a term of some type α for which Add α is available, how do I call summands on e?

I'm presuming I need to infer the type of e, and synthesize an Add instance, but this doomed attempt

def foo (e : Expr) : MetaM (List Expr) := do
  let ty  inferType e
  dbg_trace ty
  let inst  synthInstance ( mkAppM ``Add #[ty])
  dbg_trace inst
  summands inst e

quite reasonably fails (with don't know how to synthesize implicit argument @summands (?m.69032 e ty x✝¹ a✝ inst x✝) (?m.69033 e ty x✝¹ a✝ inst x✝) inst e, phew!).

I'm missing the step where I first get inside the QQ world, so that I can use q(inferInstance) to type-safely produce the instance.

Gabriel Ebner (Oct 11 2022 at 01:12):

There's inferTypeQ:

let (u, α, e)  inferTypeQ e
let inst : Q(Add $α)  synthInstanceQ q(Add $α)

Gabriel Ebner (Oct 11 2022 at 01:13):

Note that q(inferInstance) only works when you can statically determine the instance. Since we don't have ∀ α, Add α, this won't be the case here.

Scott Morrison (Oct 11 2022 at 01:56):

Thanks! inferTypeQ didn't quite work for me, as you get α : Q(Sort u), but then q(Add $a) doesn't typecheck, because Add expects Type rather than Sort.

def inferTypeQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Type $u)) × Q($α)) := do
  let α  inferType e
  let .sort (.succ u)  whnf ( inferType α) | throwError "not a type{indentExpr α}"
  pure u, α, e

presumably works as a work-around, but perhaps there's a better solution?

Scott Morrison (Oct 17 2022 at 03:09):

@Gabriel Ebner, is there some better way to use Qq here:

import Qq

open Qq Lean

def foo : MetaM Q(Inhabited Nat) := synthInstanceQ q(Inhabited Nat) -- works
def bar (α : Q(Sort u)) : MetaM Q(Inhabited $α) := synthInstanceQ q(Inhabited $α) -- fails: `incompatible metavariable`
def baz (α : Q(Sort u)) : MetaM Q(Inhabited $α) := @synthInstanceQ (.max (.succ .zero) u) q(Inhabited $α) -- works

Scott Morrison (Oct 17 2022 at 03:11):

I noticed this when I found I needed:

example (α : Q(Type u)) : MetaM Q(CommSemiring $α) := @synthInstanceQ (.succ u) q(CommSemiring $α)

Last updated: Dec 20 2023 at 11:08 UTC