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

Confusing error message when existential parameter used in the body #336

Open
rachitnigam opened this issue Sep 26, 2023 · 0 comments
Open
Labels
bug Something isn't working C: well-formedness Component: A check that is not the interval check S: available This is available to be worked on

Comments

@rachitnigam
Copy link
Member

When trying to compile the following program:

comp Foo<'G:1>() -> () with {
    exists N;
} {
    // Bundle uses N which will not be bound in time during monomorphization.
    bundle a[N]: ['G, 'G+1] 32;
    exists N = 10;
}

comp main<'G:1>() -> () {
    F := new Foo;
}

The compiler says:

rachitnigam ~/git/filament (aetherling-existential !?$)
% cargo run -q -- exist-bad-err.fil
thread 'main' panicked at 'internal error: entered unreachable code: existential parameter `N' occurred in a use location', src/ir_passes/mono/monosig.rs:235:21
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

The actual problem in the program is use of N in bundle a[N]. The problem is that when running the program, N is not yet bound to a value because we have not evaluated the exists binding. In general, existential parameters cannot be used in the body because of this problem. Instead, the correct program should just say bundle a[N].

Our well-formedness pass should emit an error to this effect.

@rachitnigam rachitnigam added bug Something isn't working C: well-formedness Component: A check that is not the interval check S: available This is available to be worked on labels Sep 26, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working C: well-formedness Component: A check that is not the interval check S: available This is available to be worked on
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant