default_implementation should enforce public_name

[dra27]

I used the internal name of a library for default_implementation rather than the public_name. I initially didn't notice because the library was vendored, but did unexpectedly notice when I pinned the package in opam and built that way, since the dune-package file then contains a name which isn't in scope.

If the library referenced has a public_name, shouldn't Dune either insist on its being used in the default_implementation field or should it silently convert it to the public_name when it writes a dune-package file?

[ghost]

To be consistent with the treatment of library dependencies, dune should silently convert the name