Missing F* implicit argument with multiple `impl` args

[maximebuyse]

fn f(arg1: impl Clone, arg2: impl Clone) {}

Open this code snippet in the playground

The generated F* for this is:

let f
      (#impl_517411079_ #impl_517411079_:
          Type0)
      (#[FStar.Tactics.Typeclasses.tcresolve
            ()]
          i2:
          Core.Clone.t_Clone
          impl_517411079_)
      (#[FStar.Tactics.Typeclasses.tcresolve
            ()]
          i3:
          Core.Clone.t_Clone
          impl_330573305_)
      (arg1: impl_517411079_)
      (arg2: impl_330573305_)
    : Prims.unit = ()

impl_517411079_ is declared twice and impl_330573305_ is never declared.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[clementblaudeau]

The same issue also appears in Lean. Such implicit parameters should be named differently in a (small) engine phase.

[clementblaudeau]

The workaround is to name the implicit parameters, turning

fn f(arg1: impl Clone, arg2: impl Clone) {}

into

fn f<T1 : Clone,T2 : Clone>(arg1: T1, arg2: T2) {}

Open this code snippet in the playground