fix: Account for the optional equality support of map/seq inside newtypes #5980
Conversation
| thingsChanged = true; | ||
| } else if (type.SupportsEquality) { | ||
| // nothing to do | ||
| } else if (type.Normalize() is UserDefinedType userDefinedType) { |
There was a problem hiding this comment.
Why do you need this normalization? I thought that AsMapType and AsSeqType would actually do that.
There was a problem hiding this comment.
This type.Normalize() cuts through any type proxies that may be sitting around the UserDefinedType.
AsMapType and AsSeqType call NormalizeExpand(), which cuts through both proxies and type synonyms. But that's too much, because a type synonym can also have an explicit (==) declaration.
There was a problem hiding this comment.
If a type synonym does not have an explicit (==) annotation, it's still sound, right?
In general, I don't think you can conclude faster that a type synonym supports equality anyway. It seems that (==) is only a way to catch errors earlier.
There was a problem hiding this comment.
An explicit (==) is also a way to advertise equality support to importers of the enclosing module. Without an explicit (==), an export provides of the type would not let importers use the type as supporting equality.
| @@ -96,13 +96,21 @@ public Type RhsWithArgument(List<Type> typeArgs) { | |||
| public TopLevelDecl AsTopLevelDecl => this; | |||
| public TypeDeclSynonymInfo SynonymInfo { get; set; } | |||
|
|
|||
| public TypeParameter.EqualitySupportValue EqualitySupport { | |||
| private IndDatatypeDecl.ES equalitySupport = IndDatatypeDecl.ES.NotYetComputed; | |||
There was a problem hiding this comment.
The Rust compiler will also need to have precise equality support, as it's the only backend that needs to distinguish between type-parameter conditional equality and no equality possible.
Hence, it's not only solving a soundness issue, it's also making the compilation to Rust possible.
| @@ -30,27 +30,16 @@ boogie: ${DIR}/boogie/Binaries/Boogie.exe | |||
| tests: | |||
| (cd "${DIR}"; dotnet test Source/IntegrationTests) | |||
|
|
|||
| # make test name=<part of the path of an integration test> | |||
| # make test name=<integration test filter> | |||
There was a problem hiding this comment.
These changes to the makefile make it much much easier to test single files without having to rebuild, and also to update individual outputs without having to run the IDE or a complex command (or Lit, which we are not always supporting)
| return TypeParameter.EqualitySupportValue.Unspecified; | ||
| if (equalitySupport == IndDatatypeDecl.ES.NotYetComputed) { | ||
| var thingsChanged = false; | ||
| if (ModuleResolver.SurelyNeverSupportEquality(BaseType)) { |
There was a problem hiding this comment.
Because the types are topologically sorted, this will only be executed when the types this newtype depends on have been resolved.
| @@ -400,6 +400,12 @@ public override bool SupportsEquality { | |||
| i++; | |||
| } | |||
| return true; | |||
| } else if (ResolvedClass is NewtypeDecl newtypeDecl) { | |||
| if (newtypeDecl.IsRevealedInScope(Type.GetScope())) { | |||
| return newtypeDecl.RhsWithArgument(TypeArgs).SupportsEquality; | |||
There was a problem hiding this comment.
Because of my change, we could also do the same treatment as for the datatypes, if you preferred. I'm fine with both approaches and to switch if you prefer.
| (anotherIndDt != null && anotherIndDt.EqualitySupport == IndDatatypeDecl.ES.Never) || | ||
| arg.Type.IsCoDatatype || | ||
| arg.Type.IsArrowType) { | ||
| if (arg.IsGhost || SurelyNeverSupportEquality(arg.Type)) { |
There was a problem hiding this comment.
We need this type traversal to be recursive, otherwise soundness issue 5972c.dfy
| thingsChanged = true; | ||
| } else if (type.SupportsEquality) { | ||
| // nothing to do | ||
| } else if (type.Normalize() is UserDefinedType userDefinedType) { |
There was a problem hiding this comment.
If a type synonym does not have an explicit (==) annotation, it's still sound, right?
In general, I don't think you can conclude faster that a type synonym supports equality anyway. It seems that (==) is only a way to catch errors earlier.
…dafny into issue-5972-addendum
This PR extends fix #5973 of issue #5972 to also handle newtypes, subset types, and type synonyms wrapped around map and sequence types.
Fixes #5978
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.