where { const_expr } predicates in where clauses#1446
Draft
micahscopes wants to merge 14 commits into
Draft
Conversation
Add support for where { const_expr } syntax in Fe where clauses.
Const predicates are boolean expressions evaluated via CTFE at
monomorphization time. If the expression evaluates to false,
compilation fails with a diagnostic.
Implementation spans 5 compiler layers:
- Parser: WhereConstPredicate AST node, LBrace-triggered parsing
- HIR: const_predicates field on WhereClauseId
- Lowering: Body lowering for const predicate expressions
- Diagnostics: ConstPredicateFailed error variant
- Call-site evaluation: CTFE eval in callable.rs at instantiation
This enables replacing #[arithmetic(unchecked)] with machine-checked
compile-time proofs. For example, a tuple encode_to_ptr can express
{ T0::HEAD_SIZE + T1::HEAD_SIZE >= T0::HEAD_SIZE } as a where clause
predicate instead of trusting the annotation.
Prototype status: compiles (parser + HIR), needs end-to-end testing
with actual Fe code using the new syntax.
When checking const predicates at a call site, also evaluate predicates
from the parent item's where clause (impl, impl-trait, trait). This is
needed for cases like const predicates on impl blocks:
impl<T0, T1> Encode<Sol> for (T0, T1)
where { T0::HEAD_SIZE + T1::HEAD_SIZE >= T0::HEAD_SIZE }
Previously only predicates on the function's own where clause were
evaluated. Now predicates propagate from the enclosing impl/trait.
Test that CTFE can evaluate a mandelbrot iteration loop inside a where clause predicate. Uses fixed-point arithmetic (scale 1000) on the real axis to check convergence: - c=0.25 (in the set): predicate passes - c=0.5 with 3 iterations (not yet escaped): predicate passes - c=0.5 with 10 iterations (escapes at iter 5): predicate fails Exercises loops, local mutation, and conditional returns in CTFE predicate evaluation.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 969e1f5afb
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
The disambiguation heuristic incorrectly rejected const predicates in trait methods and extern fns where nothing follows the predicate block. Since is_where_const_predicate is only called when after_comma is true, the block cannot be an item body — simplify to just validating the block parses as an expression. Add regression test for trait method context.
Previously, if eval_body_owner_const returned Err (e.g. div-by-zero, overflow), the predicate was silently treated as passing. Now emits error[8-0083] so broken predicates properly block compilation.
micahscopes
force-pushed
the
const-predicates
branch
from
b753050 to
f68f12c
Compare
Const predicates can now be written as bare expressions:
where T: Sized, T::SIZE >= 50
in addition to the block form:
where T: Sized, { T::SIZE >= 50 }
Disambiguation uses existing parser infrastructure:
- Type predicates: dry-run parse_type + check for ':'
- Bare expressions: delegates to parse_expr which already
handles <>/generics disambiguation via PathSegmentScope
- Block predicates: '{' after comma is still a const predicate
(after_comma invariant), not the item body
Trivia state is explicitly restored before the comma check to
prevent parse_expr sub-scopes from leaking newline_as_trivia.
micahscopes
force-pushed
the
const-predicates
branch
from
f68f12c to
0f6a3d7
Compare
Collaborator
Author
|
before merging I'd like to take a look at rust's unstable feature(generic_const_exprs) and discussions around it |
Collaborator
|
Does this work on trait impls? eg |
When a generic function calls another with const predicates in its where clause, the early detection pipeline tries to prove the predicates from the caller's assumptions using structural expression comparison. If the caller's where clause contains the same predicate (accounting for generic param name mapping), the call is accepted at definition time. Otherwise, silently defers to CTFE at monomorphization. No new errors, no false negatives — purely earlier feedback. Also fixes a latent bug where CTFE was attempted on generic args containing type params (HAS_PARAM), which would always fail.
When the trait solver selects an impl candidate and the generic args
are fully resolved (concrete types), CTFE-evaluate the impl's where
clause const predicates. Reject the candidate if any predicate is false.
This means `impl<T> Foo for T where { T::SIZE <= 32 }` now only applies
to types whose SIZE is actually <= 32. Previously, the const predicate
was ignored during trait selection.
When types are still unresolved (inference vars or params), the check
is skipped and deferred to the call-site check in callable.rs.
Collaborator
Author
|
@sbillig it should work now |
When an impl's const predicate crashes during trait selection (e.g.
division by zero), the "doesn't implement Trait" error now includes a
note explaining that a predicate panicked and why.
Before: `Zero` doesn't implement `SafeDiv`
After: `Zero` doesn't implement `SafeDiv`
= a const predicate on an impl of `SafeDiv` panicked: division by zero
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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 PR makes
ConstraintListIdthe canonical internal representation for where-clause assumptions and type-checking obligations, with const predicates treated as ordinary internal constraints.Const predicates now participate in the same obligation flow as trait constraints:
ConstraintListIdConstraintIdobligationsParamEnvassumptionsPredicateListIdremains only as a compatibility projection for the current trait solver and resolver seams. PublicConstraintkind syntax,Evidence<C>, typed reflection, generated overlays, and metaprogramming providers are intentionally out of scope for this PR.Validation:
CARGO_TARGET_DIR=/tmp/fe-constraints-target cargo test -p fe-hir --test constraintsCARGO_TARGET_DIR=/tmp/fe-constraints-target cargo check -p fe-hir