Closed compiler-errors closed 9 months ago
This issue is not meant to be used for technical discussion. There is a Zulip stream for that. Use this issue to leave procedural comments, such as volunteering to review, indicating that you second the proposal (or third, etc), or raising a concern that you would like to be addressed.
cc @rust-lang/types
@rustbot second
As stated on zulip, I don't think this really needs an MCP, since it aligns with our "vision" of the future type system in a-mir-formality.
But, for process, seconding.
Closing as accepted.
Proposal
Implement implication predicates
[A1, A2, ..] => B
that have the the following behavior:[A1, A2, ..] => B
, addA1, A2, ..
to the existing param-env and evaluateB
under that new param-env.B
holds, and we have an implication predicate[A1, A2, ..] => B
in the param-env, then that predicate may satisfyB
if the nested obligationsA1, A2, ..
hold.This proposal does not suggest adding surface syntax for these predicates yet, just adding them to the "middle" type layer.
Side-note: If anyone thinks this should be a compiler MCP, I'd be happy to move this over there. If this is better suited for a T-lang initiative, or needs a pre-RFC, then let me know.
Mentors or Reviewers
I've got a branch that mostly implements support for this. I'd probably start over from scratch since I'd want to audit all the places I added
todo!()
s for these predicates though. I don't want to put up a PR for it unless the team is interested in supporting this in the trait system, though.Process
The main points of the Major Change Process are as follows:
@rustbot second
.-C flag
, then full team check-off is required.@rfcbot fcp merge
on either the MCP or the PR.You can read more about Major Change Proposals on forge.
Comments
This issue is not meant to be used for technical discussion. There is a Zulip stream for that. Use this issue to leave procedural comments, such as volunteering to review, indicating that you second the proposal (or third, etc), or raising a concern that you would like to be addressed.