Skip to content

Relax restrictions for constants in value traits #6314

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
keyboardDrummer wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Relax restrictions for constants in value traits #6314

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
8e4a2c2
Allow empty ghost const field
keyboardDrummer Jul 21, 2025
aafee80
Allow assigning to array elements in ghost code
keyboardDrummer Jul 21, 2025
5c77593
Fixes
keyboardDrummer Jul 22, 2025
30f060a
Revert one change
keyboardDrummer Jul 23, 2025
9026ac6
Update test
keyboardDrummer Jul 23, 2025
4749835
Fix expect file
keyboardDrummer Jul 23, 2025
c62e0b8
Add release note
keyboardDrummer Jul 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions Source/DafnyCore/Resolver/ModuleResolver.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1543,6 +1543,21 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
CheckIsOkayWithoutRHS(f, false);
}
}
foreach (var member in cl.InheritedMembers) {
if (member is ConstantField f && f.Rhs == null && !f.IsExtern(Options, out _, out _)) {
if (f.IsGhost && !f.Type.IsNonempty) {
reporter.Error(MessageSource.Resolver, cl.Origin,
$"{cl.WhatKindAndName} must not inherit a ghost const field '{f.Name}' of type '{f.Type}' (which may be empty) without a defining value");
break;
}

if (!f.IsGhost && !f.Type.HasCompilableValue) {
reporter.Error(MessageSource.Resolver, cl.Origin,
$"{cl.WhatKindAndName} must not inherit a non-ghost const field '{f.Name}' of type '{f.Type}' (which does not have a default compiled value) without a defining value");
break;
}
}
}
}
continue;
}
Expand All @@ -1553,8 +1568,6 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
if (member is ConstantField f && f.Rhs == null && !f.IsExtern(Options, out _, out _)) {
if (f.IsStatic) {
CheckIsOkayWithoutRHS(f, false);
} else if (!traitDecl.IsReferenceTypeDecl) {
CheckIsOkayWithoutRHS(f, true);
}
}
}
Expand Down
16 changes: 15 additions & 1 deletion Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good call, could you use the most generic version so that you can also test for newtypes?

Suggested change
// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=datatype
// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s" -- --general-traits=all



module AutoInitRegressions {
Expand Down Expand Up @@ -42,6 +42,13 @@ module AutoInitRegressions {
static const Static: Y // error: Y is not auto-init
const Instance: Y // error: Y is not auto-init
}

trait PossiblyDatatypeTrait {
static const StaticField: Y // error: Y is not nonempty
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
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
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • example with newtype as well.

}

module NonemptyRegressions {
Expand Down Expand Up @@ -79,4 +86,11 @@ module NonemptyRegressions {
ghost static const Static: Y // error: Y is not nonempty
ghost const Instance: Y // error: Y is not nonempty
}

trait PossiblyDatatypeTrait {
ghost static const StaticField: Y // error: Y is not nonempty
ghost const InstanceField: Y
}

datatype PossiblyDatatypeTraitImpl extends PossiblyDatatypeTrait = PossiblyDatatypeTraitImpl { } // error
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there an error here because InstanceField is not initialized?

}
28 changes: 16 additions & 12 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1148.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,15 +9,19 @@ git-issue-1148.dfy(36,17): Error: static non-ghost const field 'Static' of type
git-issue-1148.dfy(37,10): Error: non-ghost const field 'Instance' of type 'Y' (which does not have a default compiled value) must give a defining value
git-issue-1148.dfy(42,17): Error: static non-ghost const field 'Static' of type 'Y' (which does not have a default compiled value) must give a defining value
git-issue-1148.dfy(43,10): Error: non-ghost const field 'Instance' of type 'Y' (which does not have a default compiled value) must give a defining value
git-issue-1148.dfy(56,14): Error: static ghost const field 'Global' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(52,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(53,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(59,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(58,8): Error: class 'Class' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor
git-issue-1148.dfy(64,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(68,8): Error: class 'TraitImpl' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor
git-issue-1148.dfy(73,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(74,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(79,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
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
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about a reformulation that gives two possible resolution outcomes?

Suggested change
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".

git-issue-1148.dfy(63,14): Error: static ghost const field 'Global' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(59,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(60,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(66,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(65,8): Error: class 'Class' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor
git-issue-1148.dfy(71,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(75,8): Error: class 'TraitImpl' with fields without known initializers, like 'InstanceField' of type 'Y', must declare a constructor
git-issue-1148.dfy(80,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(81,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(86,23): Error: static ghost const field 'Static' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(87,16): Error: ghost const field 'Instance' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(91,23): Error: static ghost const field 'StaticField' of type 'Y' (which may be empty) must give a defining value
git-issue-1148.dfy(95,11): Error: datatype 'PossiblyDatatypeTraitImpl' must not inherit a ghost const field 'InstanceField' of type 'Y' (which may be empty) without a defining value
26 resolution/type errors detected in git-issue-1148.dfy
6 changes: 3 additions & 3 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -216,14 +216,14 @@ module UninitializedConsts {
ghost const A: AutoInit
ghost const B: AutoInit := 15

const g: Nonempty // error: requires initialization
const g: Nonempty
const h: Nonempty := 15
ghost const G: Nonempty
ghost const H: Nonempty := 15

const s: PossiblyEmpty // error: requires initialization
const s: PossiblyEmpty
Copy link
Member

@MikaelMayer MikaelMayer Jul 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

const t: PossiblyEmpty := 15
ghost const S: PossiblyEmpty // error: requires initialization
ghost const S: PossiblyEmpty
ghost const T: PossiblyEmpty := 15
}

Expand Down
5 changes: 1 addition & 4 deletions Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,6 @@ NonReferenceTraits.dfy(192,16): Error: ghost const field 'S' of type 'PossiblyEm
NonReferenceTraits.dfy(202,10): Error: non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value
NonReferenceTraits.dfy(207,10): Error: non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value
NonReferenceTraits.dfy(209,16): Error: ghost const field 'S' of type 'PossiblyEmpty' (which may be empty) must give a defining value
NonReferenceTraits.dfy(219,10): Error: non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object')
NonReferenceTraits.dfy(224,10): Error: non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object')
NonReferenceTraits.dfy(226,16): Error: ghost const field 'S' of type 'PossiblyEmpty' (which may be empty) must give a defining value (consider changing the field to be a function, or restricting the enclosing trait to be a reference type by adding 'extends object')
NonReferenceTraits.dfy(279,8): Error: class 'ClassWithParentWithoutConstructor' with fields without known initializers, like 'g' of type 'Nonempty', must declare a constructor
NonReferenceTraits.dfy(295,17): Error: static non-ghost const field 'g' of type 'Nonempty' (which does not have a default compiled value) must give a defining value
NonReferenceTraits.dfy(300,17): Error: static non-ghost const field 's' of type 'PossiblyEmpty' (which does not have a default compiled value) must give a defining value
Expand Down Expand Up @@ -112,4 +109,4 @@ NonReferenceTraits.dfy(460,9): Error: == can only be applied to expressions of t
NonReferenceTraits.dfy(470,9): Error: == can only be applied to expressions of types that support equality (got TraitA)
NonReferenceTraits.dfy(471,9): Error: == can only be applied to expressions of types that support equality (got TraitB)
NonReferenceTraits.dfy(472,14): Error: set argument type must support equality (got TraitA)
62 resolution/type errors detected in NonReferenceTraits.dfy
59 resolution/type errors detected in NonReferenceTraits.dfy
1 change: 1 addition & 0 deletions docs/dev/news/6314.feat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Allow value traits (those that do not extend from object), to declare const fields without initializers.
Loading