Synth `OfNat A n` for mvar `A`

Stream: general

[Max Nowak 🐉]

I am making a DSL, and have numeric literals which may be of different type, so I thought I'd use what Lean does and try to synthesize OfNat. My first attempt was:

def elabDsl (A : Q(Type)) : Syntax -> TermElabM Q($A)
| `($n:num) => do
  let n : Nat := n.getNat
  let ofNat <- synthInstance q(OfNat $A $n)
  return q(($ofNat).ofNat)

However, since the expected type A can be unknown, we fail to synthesize the OfNat instance. (It could be Int, BitVec _, etc.). I need to postpone synthesizing OfNat, HAdd, etc until after expected type is known. For this, I found mkInstMVar and used that in place of synthInstance. However, now my instance mvars are never instantiated.

There is probably an idiomatic way of doing this, I just can't find it.

[Henrik Böving]

Sounds like a good use of tryPostponeIfNoneOrMVar on your expected type to me:

def elab : TermElab := fun stx typ? => do
  tryPostponeIfNoneOrMVar typ?
  let some typ := typ? | throwError "some informative message"

[Max Nowak 🐉]

I'm not sure how to use this. That looks like it just aborts my elaboration altogether if my inst is an mvar? I want my instance to be an mvar, because sometimes I legit don't know the expected type A. I am not sure how to make Lean finish TC synthesis once those mvars are known.

[Max Nowak 🐉]

mkInstMVar sounds like what I want, but it has no documentation and I wasn't able to find much about it here on Zulip.

[Kyle Miller]

mkInstMVar is right (and in fact docs#Lean.Elab.Term.elabNumLit uses it for constructing the OfNat instance)

[Kyle Miller]

To finish elaboration, you have to either wrap your elaboration routine in withSynthesize or have a synthesizeSyntheticMVarsNoPostponing checkpoint

[Max Nowak 🐉]

Oh wow that did it. Perfect. Awesome. Thanks a ton!

[Kyle Miller]

For a mini case study, here's part of the change tactic: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Change.lean#L21

The runTermElab itself is responsible for doing synthesizeSyntheticMVarsNoPostponing before returns. On line 30, there's a partial checkpoint that allows typeclass problems to be postponed, allowing the isDefEq to try to solve for pending instances.

Then, elaboration is complete, so it's safe to use the next method, which does isDefEq inside a context where synthetic opaque metavariables become assignable. (That let's change assign ?m metavariables for example.)