Instance diamonds in has_to_pexpr

Stream: metaprogramming / tactics

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

Done in #14901

[Eric Wieser]

Almost nothing depended on it