Extern names (inconsistently) escaped to avoid target language keywords

[robin-aws]

Dafny version

4.8.1

Code to produce this issue

module {:extern "Time"} Time {
  method {:extern} GetCurrentTime() returns (x: int)
}

method Main() {
  var t := Time.GetCurrentTime();
}

Command to run and resulting output

% dafny translate go Scratch.dfy

Dafny program verifier finished with 1 verified, 0 errors

Observed that inside the translated `Main` method, the call is `Time.GetCurrentTime()`, but at the same time Dafny produces a `Time_/Time_.go` file containing a `_Time` package.

What happened?

The explicitly requested target language symbol of Time was partially escaped when it shouldn't be. There are multiple resolutions to this:

1. Decide this is an invalid program and have dafny translate go intentionally error.
2. Consistently use Time throughout, even if it may result in a broken program.
3. Decide that extern names SHOULD be escaped consistently and document that clearly.

The general problem applies to the other backends as well - AFAICT we generally escape extern names.

cc @alex-chew who is working on a redesign of the extern attribute.

What type of operating system are you experiencing the problem on?

Mac