add some wf checks for fn types #181
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
nikomatsakis
requested changes
Jul 11, 2024
| @@ -20,13 +20,13 @@ fn decls() -> Decls { | |||
| fn direct_cycle() { | |||
| test_prove(decls(), term("exists<ty A> {} => {A = Vec<A>}")).assert_err( | |||
| expect![[r#" | |||
| judgment `prove_wc_list { goal: {?ty_0 = Vec<?ty_0>}, assumptions: {}, env: Env { variables: [?ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty> ], [impl <ty> Foo(Vec<^ty0_0>)], [], [], [], [], {}, {}) }` failed at the following rule(s): | |||
There was a problem hiding this comment.
we should probably cleanup the Env Debug impl to e.g. suppress empty lists...
There was a problem hiding this comment.
#187 smaller decls output
shua
commented
Jul 11, 2024
src/test/functions.rs
Outdated
Comment on lines
47
to
56
| fn wf() { | ||
| crate::assert_ok!( | ||
| [ | ||
| crate Foo { | ||
| fn foo<ty T>() -> T { trusted } | ||
| fn bar(fn foo<u32>, fn(u32) -> (), fn(bool)) -> () { trusted } | ||
| } | ||
| ] | ||
|
|
||
| expect_test::expect![[r#" | ||
| judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): | ||
| the rule "some" failed at step #0 (src/file.rs:LL:CC) because | ||
| judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): | ||
| the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because | ||
| judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }`"#]] | ||
| expect_test::expect!["()"] |
There was a problem hiding this comment.
@nikomatsakis this is a test for fn well-formed. I can also add some tests for catching poorly formed fns.
lcnr
reviewed
Jul 16, 2024
There was a problem hiding this comment.
mind blocking this PR on #187 (comment) reviewing it with most of the changes being an added [] to decls isn't great
|
good time for re-review @lcnr or @nikomatsakis ? |
|
Yes! I have been very absent from a-mir-formality but I'm looking to jump back in and figure out next steps soon-ish anyway, so it is a good time.
…On Thu, Oct 17, 2024, at 1:20 PM, shua wrote:
good time for re-review @lcnr <https://github.com/lcnr> or @nikomatsakis <https://github.com/nikomatsakis> ?
—
Reply to this email directly, view it on GitHub <#181 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AABF4ZQUX5NRP6N45S7MWWTZ37WXDAVCNFSM6AAAAABKH4ENP2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMRQGA4TEMRRG4>.
You are receiving this because you were mentioned.Message ID: ***@***.***>
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This change adds a syntax for specifying FnDefs and FnPtrs as type parameters,
fn name<T, U, ...>andfn(T, U,...) -> Vrespectively. Thefnprefix is used to disambiguate between adt identifiers. In addition, some relevant well-formed cases have been added.