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

Stream: mathlib4

[Scott Morrison]

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]

There's inferTypeQ:

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

[Gabriel Ebner]

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]

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]

@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]

I noticed this when I found I needed:

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