[Bug]: Name clashes in compilation of datatypes

[RustanLeino]

Dafny version

3.9.1.41027

Code to produce this issue

datatype X<X> = X(X: X)

/* In Go, there's an additional problem with

datatype X<X> = X(x: X)

*/

Command to run and results

dafny test.dfy /compileTarget:cs
dafny test.dfy /compileTarget:java
dafny test.dfy /compileTarget:go

Each of these three generates malformed code, because of the duplicated names. To fix the problem, care needs to be taken in these compiler targets to suitably rename or qualify the names.

What happened?

dafny test.dfy /compileTarget:cs

Dafny program verifier finished with 0 verified, 0 errors
Errors compiling program into test
(4844,18): error CS0694: Type parameter 'X' has the same name as the containing type, or method

dafny test.dfy /compileTarget:java

Dafny program verifier finished with 0 verified, 0 errors
Wrote textual form of target program to test-java/test.java
Additional target code written to test-java/_System/nat.java
Additional target code written to test-java/_System/X.java
test-java/_System/X.java:39: error: unexpected type
public static X Default(X _default_X) {
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in method Default
test-java/_System/X.java:43: error: unexpected type
public static dafny.TypeDescriptor<X> _typeDescriptor(dafny.TypeDescriptor _td_X) {
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in method _typeDescriptor
test-java/_System/X.java:46: error: unexpected type
public static X create(X X) {
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in method create
test-java/_System/X.java:18: error: unexpected type
X o = (X)other;
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in class _System.X
test-java/_System/X.java:18: error: unexpected type
X o = (X)other;
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in class _System.X
test-java/_System/X.java:44: error: unexpected type
return (dafny.TypeDescriptor<X>) (dafny.TypeDescriptor) dafny.TypeDescriptor.referenceWithInitializer(X.class, () -> Default(_td_X.defaultValue())); ^ required: class found: type parameter X where X is a type-variable: X extends Object declared in method _typeDescriptor(TypeDescriptor) test-java/_System/X.java:44: error: cannot select from a type variable return (dafny.TypeDescriptor>) (dafny.TypeDescriptor) dafny.TypeDescriptor.referenceWithInitializer(X.class, () -> Default(_td_X.defaultValue()));
^
test-java/_System/X.java:47: error: unexpected type
return new X(X);
^
required: class
found: type parameter X
where X is a type-variable:
X extends Object declared in method create(X)
8 errors
Error while compiling Java files. Process exited with exit code 1

dafny test.dfy /compileTarget:go

Dafny program verifier finished with 0 verified, 0 errors
Wrote textual form of target program to test-go/src/test.go
Additional target code written to test-go/src/dafny/dafny.go
Additional target code written to test-go/src/System_/System_.go

command-line-arguments

test-go/src/test.go:38:10: X (variable of type interface{}) is not a type

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

Mac

[RustanLeino]

The file https://github.com/dafny-lang/dafny/blob/master/Test/git-issues/git-issue-1815.dfy contains a declaration that triggers this bug in Go. Alas, the test ignores the error code for Go and the successful test has no output, so this test has been succeeding incorrectly.