A Qq gotcha

Stream: metaprogramming / tactics

[Eric Wieser]

This one surprised me slightly:

import Mathlib
open Qq

def foo (x : Q(Nat) := by assumption) : Q(Nat) := q(Nat.factorial $x)

-- (kernel) application type mismatch
example : 0 ≤ (by_elab let z : Q(String) := q("wat"); return foo) := by
  sorry

[Aaron Liu]

well assumption has a higher transparency

[Eric Wieser]

For my purposes, by exact q(delta% inferInstance) seems to behave better

[Aaron Liu]

what's delta%?

[Eric Wieser]

So I guess by exact q(by assumption) is probably correct

[Eric Wieser]

delta% inferInstance is "infer the instance and don't add a silly inferInstance term"

[Eric Wieser]

(which is what by apply_instance did in Lean 3)

[Kyle Miller]

I'm wondering if there should be an infer_instance% term elaborator, which elaborates to the instance itself. The infer_instance tactic could be a macro for exact infer_instance%.

Could someone come up with some case to be made for this? And also a justification for why the inferInstance term might be better in some cases, to balance it out?

[Aaron Liu]

inferInstance gives you an expected type hint, like docs#Lean.Meta.mkExpectedTypeHint

[Eric Wieser]

I'll note that my code above doesn't actually work well with Qq after all, as the autoParam metavariable is not getting populated by Qq, and is instead left unassigned.

[Robert Maxton]

Kyle Miller said:

I'm wondering if there should be an infer_instance% term elaborator, which elaborates to the instance itself. The infer_instance tactic could be a macro for exact infer_instance%.

Could someone come up with some case to be made for this? And also a justification for why the inferInstance term might be better in some cases, to balance it out?

I would like this to exist! Primarily, I encounter it when working with TopologicalSpaces, where often the simplest way to, say, prove that a set is open is to unfold the typeclass instance and then reason about what's usually a (co)induced topology; if I'm doing this in the middle of a construction, though, then it's quite likely I'll end up with opaque inferInstances and I won't know how to proceed without simp [inferInstance] or similarly cursed things.

[Kyle Miller]

It's an extra step, but you should be able to hover over inferInstance in the infoview to see the instance. Is there a reason that doesn't work for you?