Feeding instances to QQ

Stream: lean4

[Patrick Massot]

How do you make QQ aware of an instance you just synthesized? The MWE below depends on mathlib but I hope it's enough to make the question clear:

import Mathlib.Tactic.NormNum.Core

open Qq Lean Meta Mathlib Meta NormNum

example (e : Expr) : MetaM Unit :=
do let α : Q(Type) ← inferType e
   let sα ← synthInstance q(LinearOrderedField $α)
   have al := (← mkOfNat α sα <| mkRawNatLit 0).1
   have ar := (← mkOfNat α sα <| mkRawNatLit 1).1
   let al_pos : Q(Prop) := q($al < $ar)
   pure ()

This fails at q($al < $ar) with message failed to synthesize instance LT «$α», q isn't seeing the linear ordered field instance.

[Patrick Massot]

Note it may be that I'm completely misunderstanding how QQ should be used.

[Tomas Skrivan]

What about adding have inst := $sa to the term where you want the instance to be available?

[Adam Topaz]

Yeah, you could do something like this:

example (e : Expr) : MetaM Unit :=
do let α : Q(Type) ← inferType e
   let sα : Q(LinearOrderedField $α) := ← synthInstance q(LinearOrderedField $α)
   have al := (← mkOfNat α sα <| mkRawNatLit 0).1
   have ar := (← mkOfNat α sα <| mkRawNatLit 1).1
   let al_pos : Q(Prop) := q(letI : LinearOrderedField $α := $sα ; $al < $ar)
   pure ()

But I hope there's a better way without a let

[Adam Topaz]

Oh actually it just works:

example (e : Expr) : MetaM Unit :=
do let α : Q(Type) ← inferType e
   let sα : Q(LinearOrderedField $α) := ← synthInstance q(LinearOrderedField $α)
   have al := (← mkOfNat α sα <| mkRawNatLit 0).1
   have ar := (← mkOfNat α sα <| mkRawNatLit 1).1
   let al_pos : Q(Prop) := q($al < $ar)
   pure ()

[Adam Topaz]

And I guess you could clean it up even more:

example (e : Expr) : MetaM Unit :=
do let α : Q(Type) ← inferType e
   let sα : Q(LinearOrderedField $α) := ← synthInstance q(LinearOrderedField $α)
   have al : Q($α) := q(0)
   have ar : Q($α) := q(1)
   let al_pos : Q(Prop) := q($al < $ar)
   pure ()

[Patrick Massot]

Oh I see, I simply needed to tell Lean that sα is also in the QQ world with a type ascription.

[Patrick Massot]

Thanks Tomas and Adam!

[Eric Wieser]

I think if you use docs4#Qq.synthInstanceQ then you can skip adding some of the ascriptions here

[Eric Wieser]

Oh, I guess Qq doesn't get shown in doc-gen

[Henrik Böving]

Indeed, although that could be done

[Alex Keizer]

I'm not so sure that synthInstanceQ removes the need for type ascription. In my experience, Qq refuses to reflect let-bindings without type ascription, even if the type is completely unambiguous

[Eric Wieser]

I just tested, replacing synthInstance in the original mwe with synthInstanceQ solves the problem

[Moritz Doll]

Henrik Böving said:

Indeed, although that could be done

I would be happy if this was the case.