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

Export sets should transitively consider subset types #5417

Open
MikaelMayer opened this issue May 9, 2024 · 0 comments
Open

Export sets should transitively consider subset types #5417

MikaelMayer opened this issue May 9, 2024 · 0 comments
Assignees
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

module A {
  type uint8 = int
  type Converted = seq<uint8>
  
  function Convert(s : string) : (ret : Converted)
}

module B {
  import A
  export provides
    A,
    DEFAULT_VALUE
  const DEFAULT_VALUE := A.Convert("DEFAULT_VALUE")
}

Command to run and resulting output

Paste in VSCode in latest-nightly

What happened?

Raised while checking export set B: Type or type parameter is not declared in this scope: uint8 (did you forget to qualify a name or declare a module import 'opened'?) (note that names in outer modules are not visible in contained modules)
This export set is not consistent: B

There should be no error.

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

Windows

@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done labels May 9, 2024
@MikaelMayer MikaelMayer self-assigned this May 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done
Projects
None yet
Development

No branches or pull requests

1 participant