where { const_expr } predicates in where clauses#1446
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".
| match p.current_kind() { | ||
| Some(SyntaxKind::Comma) => true, | ||
| Some(kind) if is_type_start(kind) => true, | ||
| Some(SyntaxKind::LBrace) => true, | ||
| _ => false, |
There was a problem hiding this comment.
{...} in where clauses as const predicates
The new disambiguation returns false whenever the block is followed by a non-where token, which misclassifies valid trailing const predicates (for example in trait/extern method signatures like fn f<T>() where { true } before a newline/}) as function bodies. In those contexts, the parser consumes the predicate block as the method body and drops the predicate semantics entirely, so constraints are not enforced.
Useful? React with 👍 / 👎.
| Err(_) => { | ||
| // CTFE evaluation failed -- silently skip for the prototype. | ||
| // In a production implementation, we'd emit a more specific | ||
| // diagnostic here. | ||
| } |
There was a problem hiding this comment.
Err(_) from eval_body_owner_const is currently ignored, so predicates that cannot be evaluated (e.g. due to CTFE errors such as overflow/div-by-zero or unsupported operations) are treated as if they succeeded. This lets calls compile even though their where { ... } constraint was not proven, which breaks the feature’s contract and can hide real compile-time failures.
Useful? React with 👍 / 👎.
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
|
before merging I'd like to take a look at rust's unstable feature(generic_const_exprs) and discussions around it |
1 participant
Const predicates in where clauses, evaluated via CTFE at monomorphization. If the expression is false, compilation fails.
Full CTFE works inside predicates (loops, mutation, function calls). There's a mandelbrot convergence test that runs a fixed-point iteration loop at compile time as a stress test.
Main use case: replacing
#[arithmetic(unchecked)]with compile-time overflow proofs for things like tuple ABI encoding where offset sums are all const. Predicates on parent items (impl blocks, traits) propagate to methods.