Skip to content
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

Jump to bottom

Datatype erasure and traits don't play together #5233

Closed
RustanLeino opened this issue Mar 21, 2024 · 0 comments · Fixed by #5234
Closed

Datatype erasure and traits don't play together #5233

RustanLeino opened this issue Mar 21, 2024 · 0 comments · Fixed by #5234
Assignees
@RustanLeino
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag

Comments

@RustanLeino
Copy link
Collaborator

Dafny version

4.5.0

Code to produce this issue

trait Trait {
  function Value(): string
}

datatype Dt extends Trait = Dt(s: string)
{
  function Value(): string { s }
}

method Main() {
  var d: Dt := Dt("hello");
  var y: Trait := d;
  print d.Value(), " ", y.Value(), "\n";
}

Command to run and resulting output

% dafny run test.dfy --type-system-refresh --general-traits=datatype

Dafny program verifier finished with 2 verified, 0 errors
Errors compiling program into test
source(5726,21): error CS0535: 'Dt' does not implement interface member 'Trait.Value()'

What happened?

Since the datatype has 1 constructor with 1 argument, the compiler optimizes Dt to be just that argument. But this optimization should be used only if the datatype does not implement any traits.

What type of operating system are you experiencing the problem on?

Mac
@RustanLeino RustanLeino added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag labels Mar 21, 2024
@RustanLeino RustanLeino self-assigned this Mar 21, 2024
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Mar 21, 2024
@RustanLeino
fix: Optimize datatype wrappers only in the absence of trait parents
fc7a52c 
Fixes dafny-lang#5233

As a bonus, allow the optimization when there are no _compiled_ fields (previously, the optimization was disabled when _any_ fields were present).
@RustanLeino RustanLeino mentioned this issue Mar 21, 2024
Merged
keyboardDrummer pushed a commit that referenced this issue Mar 22, 2024
@RustanLeino
fix: Optimize datatype wrappers only in the absence of trait parents (#…
ece9b76 
…5234)

This PR makes two changes to when the "erase datatype wrapper"
optimization is engaged.

* The optimization is disabled if the datatype implements any traits.
(Previously, the optimization was still allowed under this condition,
which had caused malformed code, see issue #5233.)
* Allow the optimization in the presence of ghost fields. (Previously,
the optimization was disabled if the datatype contained _any_ fields.
But ghost fields pose no problems for compilation.)

Fixes #5233

### How has this been tested?

The tests (including the test case from the bug report) were added to
`comp/ErasableTypeWrappers.dfy`.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
RustanLeino added a commit to RustanLeino/dafny that referenced this issue Jun 8, 2024
@RustanLeino
fix: Optimize datatype wrappers only in the absence of trait parents
1c7d836 
Fixes dafny-lang#5233

As a bonus, allow the optimization when there are no _compiled_ fields (previously, the optimization was disabled when _any_ fields were present).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: code-generation Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Optimize datatype wrappers only in the absence of trait parents RustanLeino/dafny
1 participant
@RustanLeino