hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
198 stars 20 forks source link

Add phase: trait method name disambiguation #61

Open W95Psp opened 1 year ago

W95Psp commented 1 year ago

Two traits in the same namespace in Rust can share method names. This is not true in some backends (for instance F*).

We need a phase that globally adds prefixes or suffixes to such methods whose name collides.

The F* case

In F, a trait is translated as a typeclass. F treats typeclasses as records, but generates a top-level let for each field (aka trait methods), with an implicit meta argument that takes care of resolving the correct instance when called.

The issue is thus that two typeclasses sharing a method name will attempt to generate two let bindings with the same name.

If we have #20, we can stop relying on F* typeclasses entirely and this issue will disappear.

Workaroung

Rewrite:

pub trait foo = { fn f(self); }
pub trait bar = { fn f(self); }

Into:

trait foo = { fn f(self); }
mod trait_bar {
  pub trait bar = { fn f(self); }
}
pub use trait_bar::*;
github-actions[bot] commented 4 weeks ago

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.