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.

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

Compilation incompleteness for general traits #5951

Open
MikaelMayer opened this issue Dec 2, 2024 · 0 comments
Open

Compilation incompleteness for general traits #5951

MikaelMayer opened this issue Dec 2, 2024 · 0 comments
Assignees
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

trait GeneralTrait {
}

datatype Test = Test(x: GeneralTrait)

newtype I extends GeneralTrait = x: int | true

method AcceptType<T(==)>(a: T, b: T) returns (c: bool) {
  return a == b;
}

method Caller(t: Test) returns (b: bool) {
  b := AcceptType<Test>(t, t);
}

method Main() {
  var b := Caller(Test(1 as I));
  print b;
}

Command to run and resulting output

$ dafny run -t:cs --type-system-refresh --general-traits=full generalTrait.dfy

Dafny program verifier finished with 4 verified, 0 errors
Failed to compile C# source code using 'dotnet build C:\Users\mimayere\Documents\Dafny tests\generalTrait.csproj -o C:\Users\mimayere\Documents\Dafny tests'. Command output was:
  Determining projects to restore...
  All projects are up-to-date for restore.
C:\Users\mimayere\Documents\Dafny tests\generalTrait.cs(5718,7): warning CS0162: Unreachable code detected [C:\Users\mimayere\Documents\Dafny tests\generalTrait.csproj]
C:\Users\mimayere\Documents\Dafny tests\generalTrait.cs(5732,32): error CS1503: Argument 1: cannot convert from 'System.Numerics.BigInteger' to '_module.GeneralTrait' [C:\Users\mimayere\Documents\Dafny tests\generalTrait.csproj]

Build FAILED.

C:\Users\mimayere\Documents\Dafny tests\generalTrait.cs(5718,7): warning CS0162: Unreachable code detected [C:\Users\mimayere\Documents\Dafny tests\generalTrait.csproj]
C:\Users\mimayere\Documents\Dafny tests\generalTrait.cs(5732,32): error CS1503: Argument 1: cannot convert from 'System.Numerics.BigInteger' to '_module.GeneralTrait' [C:\Users\mimayere\Documents\Dafny tests\generalTrait.csproj]
    1 Warning(s)
    1 Error(s)

Time Elapsed 00:00:09.07

What happened?

There should be no compilation issue

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

Windows

@MikaelMayer MikaelMayer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Dec 2, 2024
@alex-chew alex-chew added lang: c# Dafny's C# transpiler and its runtime invalid translated code The compiler generates invalid code, making the the target language infrastructure crash labels Dec 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
invalid translated code The compiler generates invalid code, making the the target language infrastructure crash kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: c# Dafny's C# transpiler and its runtime
Projects
None yet
Development

No branches or pull requests

3 participants