Moved GoModule.dfy to wishlist as negative test

Test/comp/GoModule.dfy → Test/wishlist/GoModule.dfy

@@ -1,10 +1,40 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 /unicodeChar:0 "%s" /compileTarget:go > "%t"
+// RUN: %exits-with 3 %dafny /compile:3 /spillTargetCode:2 /unicodeChar:0 "%s" /compileTarget:go 2> "%t"
 // note: putting /compileTarget:go after "%s" overrides user-provided option
 // RUN: %diff "%s.expect" "%t"
 
+// This test used to work only because of a questionable Go-only feature
+// of mapping a Dafny string directly to a Go string when passed in or out of
+// an extern method. It barely worked in one direction and not in the other
+// (see https://github.com/dafny-lang/dafny/issues/2989),
+// and even when it did, equating these two types was not actually sound in all cases anyway.
+// This feature has been disabled since Dafny 4.0,
+// and unfortunately I found that rewriting the test to work without it was very
+// difficult for unrelated reasons.
+// In particular this version should work but produces unused imports
+// which the Go compiler complains about
+// (see https://github.com/dafny-lang/dafny/issues/2953).
+// Instead I've converted this into a negative test.
+
+// "url" is a built-in package, so it should be accessible to the
+// test suite without further requirements on the setup.
+module {:extern "url", "net/url"} URL {
+
+ class URL {
+ var {:extern "Host"} host: string
+ var {:extern "Path"} pathname: string
+ var {:extern "RawQuery"} search: string
+ }
+
+ trait {:extern "", "error"} Error { }
+}
+
+module {:extern "GoModuleConversions"} GoModuleConversions {
+ import opened URL
+ method {:extern "ParseURL"} Parse(address: string) returns (url: URL, error: Error?)
+}
+
 module Test {
 
- import URL
  import GoModuleConversions
 
  method TryUrl(address: string) {
@@ -25,22 +55,3 @@ module Test {
  TryUrl("http:https://localhost:8080/default.htm%");
  }
 }
-
-// "url" is a built-in package, so it should be accessible to the
-// test suite without further requirements on the setup.
-module {:extern "url", "net/url"} URL {
-
- class URL {
- var {:extern "Host"} host: string
- var {:extern "Path"} pathname: string
- var {:extern "RawQuery"} search: string
- }
-
- trait {:extern "", "error"} Error { }
-}
-
-module {:extern "GoModuleConversions"} GoModuleConversions {
- import opened URL
- method {:extern "ParseURL"} Parse(address: string) returns (url: URL, error: Error?)
-}
-

Test/wishlist/GoModule.dfy.expect

@@ -0,0 +1,2 @@
+# GoModuleConversions
+GoModule-go/src/GoModuleConversions/GoModuleConversions.go:10:3: imported and not used: "net/url"