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<X>) (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

dafny-lang / dafny