Relax restrictions for constants in value traits #6314
Conversation
keyboardDrummer
changed the title
|
Actually I don't need this anymore, so putting this on hold. |
There was a problem hiding this comment.
I think this restriction relaxing is sound, as it existed for reference traits before, and value traits are not that different in the sense that they still require a proper implementation. To my knowledge, we don't postulate anywhere the existence of values of a value trait.
| @@ -1,4 +1,4 @@ | |||
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" | |||
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype | |||
There was a problem hiding this comment.
Good call, could you use the most generic version so that you can also test for newtypes?
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype | |
| // RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=all |
| } | ||
|
|
||
| trait PossiblyDatatypeTrait { | ||
| static const StaticField: Y // error: Y is not nonempty |
There was a problem hiding this comment.
| static const StaticField: Y // error: Y is not nonempty | |
| static const StaticField: Y |
Is the error appearing both in the static const declaration and the datatype, or just in the datatype? If the latter, this comment can be removed.
| const InstanceField: Y | ||
| } | ||
|
|
||
| datatype PossiblyDatatypeTraitImpl extends PossiblyDatatypeTrait = PossiblyDatatypeTraitImpl { } // error |
There was a problem hiding this comment.
- example with newtype as well.
| ghost const InstanceField: Y | ||
| } | ||
|
|
||
| datatype PossiblyDatatypeTraitImpl extends PossiblyDatatypeTrait = PossiblyDatatypeTraitImpl { } // error |
There was a problem hiding this comment.
Is there an error here because InstanceField is not initialized?
| git-issue-1148.dfy(80,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value | ||
| 22 resolution/type errors detected in git-issue-1148.dfy | ||
| git-issue-1148.dfy(47,17): Error: static non-ghost const field 'StaticField' of type 'Y' (which does not have a default compiled value) must give a defining value | ||
| git-issue-1148.dfy(51,11): Error: datatype 'PossiblyDatatypeTraitImpl' must not inherit a non-ghost const field 'InstanceField' of type 'Y' (which does not have a default compiled value) without a defining value |
There was a problem hiding this comment.
What about a reformulation that gives two possible resolution outcomes?
| git-issue-1148.dfy(51,11): Error: datatype 'PossiblyDatatypeTraitImpl' must not inherit a non-ghost const field 'InstanceField' of type 'Y' (which does not have a default compiled value) without a defining value | |
| git-issue-1148.dfy(51,11): Error: const field 'InstanceField' of datatype 'PossiblyDatatypeTraitImpl' must either have a non-empty type or a defining value, and `Y` does not have a default compiled value |
That way we have less "must not", "does not", and "without".
| ghost const H: Nonempty := 15 | ||
|
|
||
| const s: PossiblyEmpty // error: requires initialization | ||
| const s: PossiblyEmpty |
There was a problem hiding this comment.
That's possibly the biggest potential issue but I think we are fine, since a trait is a collection of contracts, and someone should at least extend a mocked class that extends these contracts to test them.
What was changed?
How has this been tested?
git-issue-1148.dfywith new casesBy submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.