Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Instance diamonds in has_to_pexpr


Eric Wieser (Jun 22 2022 at 17:05):

I was struggling to wrap my head around how antiquotations work, and discoverred that it was because there is an instance diamond:

import meta.expr

#eval show tactic unit, from do
  let i1 : has_to_pexpr pexpr := pexpr.has_to_pexpr,
  let i2 : has_to_pexpr pexpr := has_reflect.has_to_pexpr,
  let e := ``(1),
  let p1 := @to_pexpr _ i1 e,
  let p2 := @to_pexpr _ i2 e,
  guard (p1 = p2) -- fails

Eric Wieser (Jun 22 2022 at 17:06):

The conflicting instances are docs#has_reflect.has_to_pexpr and docs#pexpr.has_to_pexpr

Eric Wieser (Jun 22 2022 at 17:07):

I think the intent of the former (introduced in #3477) is to make %%x a shorthand for %%`(x), but that's confusing for pexpr where the first spelling already has a different meaning.

Floris van Doorn (Jun 22 2022 at 18:47):

Oh, that probably shouldn't be a (global) instance then. I don't remember why I added it anymore. Feel free to remove it, if it doesn't cause a massive amount of failures.

Eric Wieser (Jun 22 2022 at 19:11):

Done in #14901

Eric Wieser (Jun 22 2022 at 19:11):

Almost nothing depended on it


Last updated: Dec 20 2023 at 11:08 UTC