We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
formality-check isn't rejecting an is-implemented where clause with nonsense in the implementing type or in a parameter to the trait.
formality-check
For example it doesn't reject a where clause whose implementing type doesn't exist:
trait Trait1 {} struct S where Nonex: Trait1 {}
or which gives the implementing type the wrong number of parameters:
trait Trait1 {} struct S1 {} struct S2<ty T> where S1<T>: Trait1 { dummy: T }
It accepts nonsensical types in trait parameters too:
trait Trait1<ty T> {} struct S where u8: Trait1<Nonex> {}
I see:
formality-check's checks amount to proving wc.well_formed() for the single where clause
wc.well_formed()
wc.well_formed() amounts to proving WellFormedTraitRef for (say) Nonex: Trait1
WellFormedTraitRef
Nonex: Trait1
the "trait well formed" rule in prove_wc() considers only the where clauses of the TraitRef's underlying trait, ignoring the TraitRef's parameters.
prove_wc()
TraitRef
The text was updated successfully, but these errors were encountered:
No branches or pull requests
formality-check
isn't rejecting an is-implemented where clause with nonsense in the implementing type or in a parameter to the trait.For example it doesn't reject a where clause whose implementing type doesn't exist:
or which gives the implementing type the wrong number of parameters:
It accepts nonsensical types in trait parameters too:
I see:
formality-check
's checks amount to provingwc.well_formed()
for the single where clausewc.well_formed()
amounts to provingWellFormedTraitRef
for (say)Nonex: Trait1
the "trait well formed" rule in
prove_wc()
considers only the where clauses of theTraitRef
's underlying trait, ignoring theTraitRef
's parameters.The text was updated successfully, but these errors were encountered: