Duplicate names in generated Dafny code when model contains "Error" shape

[justplaz]

I am working on adding S3 to the aws-sdk TestModels. My WIP code is here: https://github.com/smithy-lang/smithy-dafny/pull/349

The polymorph_dafny and polymorph_net commands succeed. When running transpile_dotnet, I get the error below:

Model/ComAmazonawsS3Types.dfy(4042,11): Error: duplicate name of top-level declaration: Error [Related location] Model/ComAmazonawsS3Types.dfy(2229,11)
Model/ComAmazonawsS3Types.dfy(4078,34): Error: member 'Opaque?' does not exist in datatype 'Error'
2 resolution/type errors detected in the_program
make: *** [transpile_implementation] Error 2

Based on some offline discussion, this is happening because the S3 smithy-model contains a shape named Error, which clashes with smithy-dafny's Error datatype.

Excerpt from model:

"com.amazonaws.s3#Error": {
            "type": "structure",
            "members": {
                "Key": {
                    "target": "com.amazonaws.s3#ObjectKey",
                    "traits": {
                        "smithy.api#documentation": "<p>The error key.</p>"
                    }
                },
                "VersionId": {
                    "target": "com.amazonaws.s3#ObjectVersionId",
                    "traits": {
                        "smithy.api#documentation": "<p>The version ID of the error.</p>\n         <note>\n            <p>This functionality is not supported for directory buckets.</p>\n         </note>"
                    }
                },
                "Code": {
                    "target": "com.amazonaws.s3#Code",
                    "traits": {
                       "smithy.api#documentation": "<p>The error code is a string that uniquely identifies an error condition..."
                    }
                },
                "Message": {
                    "target": "com.amazonaws.s3#Message",
                    "traits": {
                        "smithy.api#documentation": "<p>The error message contains a generic description of the error condition in English. It\n         is intended for a human audience. Simple programs display the message directly to the end\n         user if they encounter an error condition they don't know how or don't care to handle.\n         Sophisticated programs with more exhaustive error handling and proper internationalization\n         are more likely to ignore the error message.</p>"
                    }
                }
            },
            "traits": {
                "smithy.api#documentation": "<p>Container for all error elements.</p>"
            }
        },
        "com.amazonaws.s3#ErrorCode": {
            "type": "string"
        },
        "com.amazonaws.s3#ErrorDocument": {
            "type": "structure",
            "members": {
                "Key": {
                    "target": "com.amazonaws.s3#ObjectKey",
                    "traits": {
                        "smithy.api#documentation": "<p>The object key name to use when a 4XX class error occurs.</p>\n         <important>\n            <p>Replacement must be made for object keys containing special characters (such as carriage returns) when using \n         XML requests. For more information, see <a href=\"https://docs.aws.amazon.com/AmazonS3/latest/userguide/object-keys.html#object-key-xml-related-constraints\">\n            XML related object key constraints</a>.</p>\n         </important>",
                        "smithy.api#required": {}
                    }
                }
            },
            "traits": {
                "smithy.api#documentation": "<p>The error information.</p>"
            }
        },
        "com.amazonaws.s3#ErrorMessage": {
            "type": "string"
        },
        "com.amazonaws.s3#Errors": {
            "type": "list",
            "member": {
                "target": "com.amazonaws.s3#Error"
            }
        },

The Error shape is used as part of the Errors list, which is used in batch API operations, where the operation always succeeds and success/failure is detailed for each batch item in the response object.

It is unclear whether other service models also contain an "Error" shape or not.

[robin-aws]

Thanks @justplaz!

More background from offline discussion: this is an issue because the Dafny code generation always creates its own Error datatype for all possible errors from all operations in a service, even though there is typically no shape in the Smithy model named "Error". Other Smithy code generators tend to qualify such types with names like SomeOperationError and/or placing them in separate namespaces, so they don't conflict with types generated from names that ARE in the Smithy model.

In this case I'd suggest changing the Dafny code generation to call the datatype <ServiceName>Error instead, as a relatively small change to make this collision far less likely, if still not impossible. Moving Error to a separate module would avoid all possible collisions but is likely too much disruption to be worth it right now.

[robin-aws]

Alternatively, we could treat Error as if it was a reserved word in Dafny and escape "Error" if it appears in a model. That has to be done for legit reserved words in each language anyway, so we have to be able to handle generated symbols sometimes being different from what's in the model in documentation etc.