feat(check): reject borrow-returns at the signature (#55, 0121 task 1)
`(ret (borrow T))` is now a check error (CheckError::BorrowReturnNotPermitted, code `borrow-return-not-permitted`), fired on the fn signature before body dataflow. Borrow-returns are refcount-invisible and can outlive their source; re-enabling them needs the escape/liveness axis, which is out of scope (spec 0062). The diagnostic names that gap as an honest "not yet". The check_fn signature destructure now also binds `ret_mode` (param_modes stays under `..`; the borrow-over-value reject that reads it is folded into the cutover, task 4). RED-first: examples/borrow_return_reject.ail checked clean (exit 0) before the reject landed, exits 1 after. New CLI-boundary E2E pin crates/ail/tests/mode_signature_rejects.rs, modelled on raw_buf_new_type_arg_pin.rs. Additive — ParamMode::Implicit still present; full workspace suite green, bench/check.py 0 regressed. refs #55
This commit is contained in:
@@ -0,0 +1,27 @@
|
||||
//! Signature-level mode rejects added by spec 0062: borrow-return
|
||||
//! (`(ret (borrow T))`) and borrow-over-value (`(borrow value-type)`).
|
||||
//! CLI-boundary E2E (the project's reject-pin pattern): the diagnostic
|
||||
//! is the observable exit behaviour of `ail check`.
|
||||
use std::path::{Path, PathBuf};
|
||||
use std::process::Command;
|
||||
|
||||
fn repo_root() -> PathBuf {
|
||||
Path::new(env!("CARGO_MANIFEST_DIR")).parent().unwrap().parent().unwrap().to_path_buf()
|
||||
}
|
||||
|
||||
fn check_rejects_with(fixture: &str, code: &str) {
|
||||
let path = repo_root().join("examples").join(fixture);
|
||||
let out = Command::new(env!("CARGO_BIN_EXE_ail"))
|
||||
.arg("check").arg(&path).output().expect("ail check spawn");
|
||||
assert!(!out.status.success(),
|
||||
"expected `ail check {fixture}` to REJECT, but it passed: stdout={}",
|
||||
String::from_utf8_lossy(&out.stdout));
|
||||
let stderr = String::from_utf8_lossy(&out.stderr);
|
||||
assert!(stderr.contains(code), "expected code `{code}`, got: {stderr}");
|
||||
}
|
||||
|
||||
/// `(ret (borrow T))` is rejected with code `borrow-return-not-permitted`.
|
||||
#[test]
|
||||
fn borrow_return_is_rejected() {
|
||||
check_rejects_with("borrow_return_reject.ail", "borrow-return-not-permitted");
|
||||
}
|
||||
@@ -774,6 +774,13 @@ pub enum CheckError {
|
||||
#[error("def `{def}` in module `{module}` uses an `(intrinsic)` body, which is allowed only in a kernel-tier module or the prelude")]
|
||||
IntrinsicOutsideKernelTier { def: String, module: String },
|
||||
|
||||
/// A fn-type return slot is `(borrow T)`. Borrow-returns are
|
||||
/// refcount-invisible and can outlive their source; re-enabling
|
||||
/// them needs the escape/liveness axis (out of scope, spec 0062
|
||||
/// §"Out of scope"). Code: `borrow-return-not-permitted`.
|
||||
#[error("borrow-return not permitted for `{0}`: a (borrow …) return is refcount-invisible and can outlive its source; this language version forbids it (the escape/liveness axis that would make it sound is not yet built)")]
|
||||
BorrowReturnNotPermitted(String),
|
||||
|
||||
/// an internal invariant in the typechecker / mono pass
|
||||
/// was violated — surfaced as an error so callers can propagate
|
||||
/// rather than abort, but in well-formed inputs (typecheck has
|
||||
@@ -835,6 +842,7 @@ impl CheckError {
|
||||
CheckError::NewArgKindMismatch { .. } => "new-arg-kind-mismatch",
|
||||
CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
|
||||
CheckError::IntrinsicOutsideKernelTier { .. } => "intrinsic-outside-kernel-tier",
|
||||
CheckError::BorrowReturnNotPermitted(_) => "borrow-return-not-permitted",
|
||||
CheckError::Internal(_) => "internal",
|
||||
}
|
||||
}
|
||||
@@ -2237,9 +2245,9 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
|
||||
other => (vec![], other.clone()),
|
||||
};
|
||||
|
||||
let (param_tys, ret_ty, declared_effs) = match &inner_ty {
|
||||
Type::Fn { params, ret, effects, .. } => {
|
||||
(params.clone(), (**ret).clone(), effects.clone())
|
||||
let (param_tys, ret_ty, ret_mode, declared_effs) = match &inner_ty {
|
||||
Type::Fn { params, ret, ret_mode, effects, .. } => {
|
||||
(params.clone(), (**ret).clone(), *ret_mode, effects.clone())
|
||||
}
|
||||
other => {
|
||||
return Err(CheckError::FnTypeRequired(
|
||||
@@ -2273,6 +2281,12 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
|
||||
}
|
||||
check_type_well_formed(&ret_ty, &env)?;
|
||||
|
||||
// spec 0062: borrow-returns are refcount-invisible — forbidden in
|
||||
// this language version (the escape/liveness axis is unbuilt).
|
||||
if matches!(ret_mode, ParamMode::Borrow) {
|
||||
return Err(CheckError::BorrowReturnNotPermitted(f.name.clone()));
|
||||
}
|
||||
|
||||
// An `(intrinsic)` body is signature-only: the signature is already
|
||||
// validated above; codegen supplies the implementation via the
|
||||
// intercept registry. The body is `Term::Intrinsic` directly (a
|
||||
|
||||
Reference in New Issue
Block a user