Better name inference for anonymous givens

Compiler
1

While testing two separate implementations of a queue, I ended up defining two givens:

   given pub: IntQueue[singlepublic.ConcurrentQueue[Int]] with ...
   given priv: IntQueue[singleprivate.ConcurrentQueue[Int]] with ...

I initially tried to keep them anonymous, but the compiler refused:

given_IntQueue_ConcurrentQueue$ is already defined ...

Not a big deal, but maybe the package name could be taken into account when generating identifiers for anonymous givens.

3 Likes
2

There’s a tradeoff here: We want synthesized names to be readable and writable, e.g. for debugging. So they should be reasonably short, and simple to remember. Adding package names would make them longer and more unwieldy since we’d have to replace . by $ or some such. The current design tries to strike a balance between wide enough applicability and readability.

1 Like
3

Fair enough. Like I said, it’s not a big deal, and the workaround is straightforward.

1 Like