[Bug]: Go compiler can't convert extern string to seq<char>

[alex-chew]

Dafny version

3.9.1.41027

Code to produce this issue

method Main() {
  var s := Foo();
}

method {:extern "foo"} Foo() returns (s: string)

method Bar() returns (s: string) {
  return "hello";
}

Command to run and results

# With code as written
$ dafny translate Tmp.dfy -t go

Dafny program verifier finished with 1 verified, 0 errors
Tmp.dfy(2,14): Error: Cannot convert from string to seq<char>
Wrote textual form of partial target program to Tmp-go/src/Tmp.go

# If replacing the call to Foo with a call to Bar
$ dafny translate Tmp.dfy -t go

Dafny program verifier finished with 1 verified, 0 errors

What happened?

A call to an extern method returning a string, is not successfully compiled to Golang. The compiler complains that it Cannot convert from string to seq<char>. The same code compiles as expected to C#, Java, Javascript, and Python.

The same happens if the extern method is declared to return seq<char>, which is unsurprising since it is synonymous with string, but then again this seems to matter to the Golang compiler.

What type of Operating System are you seeing the problem on?

Mac

[robin-aws]

When attempting to reproduce this with a debug source build, I actually hit an exception:

Process terminated. Assertion failed.
   at Microsoft.Dafny.Type.Equal_Improved(Type a, Type b) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/AST/Types.cs:line 1149
   at Microsoft.Dafny.Type.SameHead(Type t, Type u) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/AST/Types.cs:line 1005
   at Microsoft.Dafny.Compilers.SinglePassCompiler.IsTargetSupertype(Type to, Type from, Boolean typeEqualityOnly) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Compilers/SinglePassCompiler.cs:line 733
   at Microsoft.Dafny.Compilers.SinglePassCompiler.EmitDowncastIfNecessary(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Compilers/SinglePassCompiler.cs:line 712
   at Microsoft.Dafny.Compilers.SinglePassCompiler.TrCallStmt(CallStmt s, String receiverReplacement, ConcreteSyntaxTree wr) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Compilers/SinglePassCompiler.cs:line 4173

The root cause is that the Go compiler tries to special-case extern declarations that accept or return string values, attempting to directly map the Dafny string type to the native Go string type, and coerce between them. The problem is that the SpecialNativeType subclass of UserDefinedType used to represent the native Go string type doesn't have all the expected values for a resolved type, which caused the above assertion failure if assertions are checked. In the release build, the symptom is just failing to recognize that two types are actually the same.

[alex-chew]

Ah, good catch. I'd seen this while trying to debug, but didn't realize it only appeared with a debug build - I was trying to reproduce this error in the VSCode IDE to no avail.

[robin-aws]

For the record, the root cause here is that this feature is not deeply and rigorously implemented, and to my knowledge none of the other compilers attempt to support this style of automatic equivalence of types for externs. My strong preference is to remove the implementation, being as careful as necessary about the fact that it is a breaking change. I've flagged this as a breaking change and conservatively added it to the Dafny 4.0 milestone in case we treat it as such.

@hmijail is any of your code depending on this behavior at this point, or would it benefit from the more consistent behavior of a Dafny string appearing as a dafny.Seq of characters in Go code?

[hmijail]

We're just getting started with the Go part, so we don't really care at this point.
Also, we're hoping to keep multiple target languages, so consistent behavior would probably be a good thing.