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

Add check to ensure generics for sorts are correct #863

Merged
merged 3 commits into from
Nov 5, 2024

Conversation

vrindisbacher
Copy link
Collaborator

Closes (#820)

@vrindisbacher
Copy link
Collaborator Author

Checking works, but I'm not sure this error is particularly helpful...

Code:

use flux_rs::*;

#[refined_by(n: int)]
struct S {
    #[field(i32[n])]
    f: i32,
}

defs! {
    fn foo(s: S<int>) -> int {
        s.n
    }
}

Output:

error[E0999]: cannot instantiate base generic with opaque type or a type parameter of kind type
 --> ../sort_gen.rs:8:1
  |
8 | struct S {
  | ^^^^^^^^
-Ztrack-diagnostics: created at crates/flux-fhir-analysis/src/wf/sortck.rs:394:18

error: aborting due to 1 previous error

It would be nice if we could point to the flux def itself and say something like:

Argument int supplied but definition for S has no generics. Either remove the generic type supplied to sort S or add missing generic type to S

crates/flux-fhir-analysis/src/conv/mod.rs Outdated Show resolved Hide resolved
crates/flux-fhir-analysis/src/conv/mod.rs Outdated Show resolved Hide resolved
@vrindisbacher
Copy link
Collaborator Author

Example input:

#![allow(unused)]

use flux_rs::*;

#[refined_by(n: int)]
struct S {
    #[field(i32[n])]
    f: i32,
}

defs! {
    fn foo(s: S<int>) -> int {
        s.n
    }
}

Output:

error[E0999]: sorts associated with this struct should have no generic arguments but 1 generic argument supplied
  --> ../sorts.rs:12:15
   |
12 |     fn foo(s: S<int>) -> int {
   |               ^ expected no generic arguments on sort
-Ztrack-diagnostics: created at crates/flux-fhir-analysis/src/conv/mod.rs:2017:40

error: aborting due to 1 previous error

Another example:

#![allow(unused)]

use flux_rs::*;

#[refined_by(n: int)]
struct S {
    #[field(i32[n])]
    f: i32,
}

defs! {
    fn foo(x: int<bool>) -> int {
        1
    }
}

And output:

error[E0999]: primitive sort int expects no generics but found 1
  --> ../sorts.rs:16:15
   |
16 |     fn foo(x: int<bool>) -> int {
   |               ^^^ Incorrect generics on primitive sort
-Ztrack-diagnostics: created at crates/flux-fhir-analysis/src/conv/mod.rs:2043:17

error: aborting due to 1 previous error

Copy link
Member

@nilehmann nilehmann left a comment

Choose a reason for hiding this comment

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

Cool, this looks good. I like having separate messages for primitive sorts and adt sorts.

There are a couple of extra places where we should report an error. I suppose we can have a different message for each of them but I'm fine with lumping them together in a generic "this sort doesn't have the right number of arguments" message.

Please also add some tests inside tests/tests/neg/error_messages/conv/

Feel free to merge after fixing the comments or ping me if something is not clear.

crates/flux-fhir-analysis/locales/en-US.ftl Outdated Show resolved Hide resolved
crates/flux-fhir-analysis/src/conv/mod.rs Outdated Show resolved Hide resolved
crates/flux-fhir-analysis/src/conv/mod.rs Show resolved Hide resolved
crates/flux-fhir-analysis/src/conv/mod.rs Outdated Show resolved Hide resolved
@vrindisbacher vrindisbacher force-pushed the vrindisbacher/sort-generics branch 9 times, most recently from 6d3921b to 55cde7a Compare November 5, 2024 22:42
@vrindisbacher
Copy link
Collaborator Author

vrindisbacher commented Nov 5, 2024

@nilehmann, I think this is almost good to go, but I'm confused by what's going on here tests/tests/neg/error_messages/conv/mismatched_generics.rs

EDIT: Seems like the same thing is happening with Self<int>...

@nilehmann
Copy link
Member

@vrindisbacher I think you put the wrong #[diagnostic] attributes. Both the error structs for self and opaque have

#[diag(fhir_analysis_generics_on_type_parameter, code = E0999)]

@vrindisbacher
Copy link
Collaborator Author

doh! thanks... can't believe i didn't catch that...

@vrindisbacher vrindisbacher merged commit 4a5b9f8 into main Nov 5, 2024
7 checks passed
@vrindisbacher vrindisbacher deleted the vrindisbacher/sort-generics branch November 5, 2024 23:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants