Repository navigation
Conversation
A string literal passed to `String<N>` or `[u8; N]` with a generic `N` left
`N` unresolved ("type annotation is needed"):
- `String<N>`: unifying the literal's string variable with `String<?N>`
accepted the type without binding anything, so the literal later fell back
to `String<len>` while `?N` stayed open. Now the length variable gets the
new `TyVarSort::StringLen { min_len }` sort and the literal is bound to
`String<?N>`. The sort only unifies with constants of at least `min_len`
(several literals keep the largest minimum) and defaults to `min_len` when
types are finalized.
- `[u8; N]`: by-value parameters are typed as `view [u8; N]`, so the check
that types a literal as a byte array for a `[u8; _]` expectation never saw
the array. Peel the view capability first.
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b5ec879270
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| TyVarSort::StringLen { min_len } => { | ||
| if let TyData::ConstTy(const_ty) = value.data(self.db) | ||
| && let Some(n_value) = const_ty.integer_value(self.db) | ||
| && n_value < BigInt::from(min_len) | ||
| { | ||
| return Err(UnificationError::TypeMismatch); | ||
| } | ||
| self.table | ||
| .unify_var_value(root_var.key, InferenceValue::Bound(value)) |
There was a problem hiding this comment.
Preserve the minimum when binding symbolic lengths
When another argument equates this inferred length to a caller's symbolic const parameter, integer_value returns None, so this arm binds the variable while discarding min_len. For example, f("abc", a) for parameters String<N> and [u8; N] inside a generic caller taking a: [u8; M] binds N to unconstrained M; instantiating that caller with M = 2 then treats the three-byte literal as String<2>. Reject symbolic values unless the lower bound is proven, or propagate the minimum constraint instead of unconditionally binding them.
Useful? React with 👍 / 👎.
A string literal passed to
String<N>or[u8; N]with a genericNleftNunresolved ("type annotation is needed"):String<N>: unifying the literal's string variable withString<?N>accepted the type without binding anything, so the literal later fell back toString<len>while?Nstayed open. Now the length variable gets the newTyVarSort::StringLen { min_len }sort and the literal is bound toString<?N>. The sort only unifies with constants of at leastmin_len(several literals keep the largest minimum) and defaults tomin_lenwhen types are finalized.[u8; N]: by-value parameters are typed asview [u8; N], so the check that types a literal as a byte array for a[u8; _]expectation never saw the array. Peel the view capability first.