Incorrect translation of duplicate binder names

[dranov]

The following file:

import Smt

theorem funextEq {α β : Type} (f g : α → β) :
  (f = g) = ∀ x, f x = g x := by
  apply propext
  constructor
  { intro h ; simp only [h, implies_true] }
  { intro h ; apply funext h }

theorem extracted {node round value : Type}
  (rel : node → round → round → value → Bool)
  (upd_rel : node → round → round → value → Bool)
  (hnext : upd_rel = rel)
  : True := by
  simp only [funextEq] at hnext
  -- After the simplification, `hnext` is pretty-printed as:
  -- (hnext : (∀ (x : node) (x_1 x_2 : round) (x_3 : value), upd_rel x x_1 x_2 x_3 = rel x x_1 x_2 x_3))
  -- but the binders actually all have name `x`
  smt [hnext]

Crashes with this error:

Lean server printed an error: libc++abi: terminating due to uncaught exception of type cvc5::parser::ParserException:
argument type is not the type of the function's argument type:
argument: x has type: value not type: node in term : (upd_rel x x x x)

To better illustrate what's happening:

-- The actual expression is something like this:
open Lean Lean.Expr in
def f : Expr :=
  forallE `x (const `node [])
    (forallE `x (const `round [])
      (forallE `x (const `value [])
        (mkAppN (const `rel [])
          #[bvar 0, bvar 1, bvar 2])
      BinderInfo.default)
    BinderInfo.default)
  BinderInfo.default

def g : Unit := dbg_trace s!"{f}" ; ()
#eval g
-- Which gets pretty printed to:
-- forall (x : node) (x_1 : round) (x_2 : value), rel x_2 x_1 x

I suspect the solution is to use the pretty-printer to generate names, rather than use the raw information in the binder.

[dranov]

I tried to de-elaborate and then elaborate the expression before translating it, but that breaks a lot of tests...