@@ -1617,6 +1617,133 @@ impl Infer {
16171617 }
16181618 }
16191619
1620+ /// Compile-time check: a compile-time-constant `body` flowing where the
1621+ /// *nominal refined* type `expected` is required (e.g. a function whose
1622+ /// declared return type is `Nat` returning a literal) is run through the
1623+ /// predicate now. A passing constant is right-by-construction; a failing
1624+ /// one is a compile error. Anything not statically evaluable is left to the
1625+ /// normal path (which requires `refine`). Reports the error but does not
1626+ /// alter the subsequent unification — the caller still runs its usual
1627+ /// check, so type errors surface normally on top of this refinement error.
1628+ fn check_const_refined_intro(&mut self, body: &ast::Expr, expected: &Ty) {
1629+ let applied = self.apply(expected);
1630+ let refined_name = match applied.peel_alias() {
1631+ Ty::Con(name, args) if args.is_empty() && self.refined_types.contains_key(name) => {
1632+ name.clone()
1633+ }
1634+ _ => return,
1635+ };
1636+ let Some(lit) = crate::codegen::extract_literal_with_consts(body, &self.const_literals)
1637+ else {
1638+ return;
1639+ };
1640+ let pred = self.refined_types.get(&refined_name).unwrap().1.clone();
1641+ if let Some(false) = crate::codegen::eval_refine_predicate_pub(&pred, &lit) {
1642+ self.error(
1643+ format!(
1644+ "constant {} does not satisfy the predicate for refined type `{}`",
1645+ lit.display(),
1646+ refined_name
1647+ ),
1648+ body.span,
1649+ );
1650+ }
1651+ }
1652+
1653+ /// For a relation element type that names (or structurally is) a record
1654+ /// alias carrying refined fields, synthesize its whole-record predicate.
1655+ /// Returns `(type_name, predicate)` where `predicate` is
1656+ /// `\row -> pred(row.f1) && pred(row.f2) && …`.
1657+ fn record_refined_pred_for(&self, elem: Ty) -> Option<(String, ast::Expr)> {
1658+ let applied = self.apply(&elem);
1659+ // The alias name survives as `Ty::Alias(name, _)`; look up its
1660+ // per-field refined predicates directly.
1661+ if let Ty::Alias(name, _) = &applied
1662+ && let Some(fps) = self.refined_field_preds.get(name)
1663+ && !fps.is_empty()
1664+ {
1665+ let pred = self.synthesize_record_pred(fps)?;
1666+ return Some((name.clone(), pred));
1667+ }
1668+ None
1669+ }
1670+
1671+ /// Build the whole-record predicate for a record alias from its per-field
1672+ /// predicates. Each `refined_field_preds` entry is already a row-level
1673+ /// lambda `\row -> <field-pred> row.fi`, so the whole-record predicate is
1674+ /// `\row -> p1(row) && … && pn(row)`.
1675+ fn synthesize_record_pred(&self, fps: &[(String, ast::Expr)]) -> Option<ast::Expr> {
1676+ let dummy = knot::ast::Span { start: 0, end: 0 };
1677+ let mut conj: Option<ast::Expr> = None;
1678+ for (_field, field_pred) in fps {
1679+ // `(field_pred) __row` — apply the row-level field predicate to the
1680+ // row being checked.
1681+ let applied = ast::Expr {
1682+ node: ast::ExprKind::App {
1683+ func: Box::new(field_pred.clone()),
1684+ arg: Box::new(ast::Expr {
1685+ node: ast::ExprKind::Var(ast::Binding::User("__row".to_string())),
1686+ span: dummy,
1687+ }),
1688+ },
1689+ span: dummy,
1690+ };
1691+ conj = Some(match conj {
1692+ None => applied,
1693+ Some(acc) => ast::Expr {
1694+ node: ast::ExprKind::BinOp {
1695+ op: ast::BinOp::And,
1696+ lhs: Box::new(acc),
1697+ rhs: Box::new(applied),
1698+ },
1699+ span: dummy,
1700+ },
1701+ });
1702+ }
1703+ let conj = conj?;
1704+ Some(ast::Expr {
1705+ node: ast::ExprKind::Lambda {
1706+ params: vec![ast::Pat {
1707+ node: ast::PatKind::Var("__row".into()),
1708+ span: dummy,
1709+ }],
1710+ ty_params: Vec::new(),
1711+ body: Box::new(conj),
1712+ },
1713+ span: dummy,
1714+ })
1715+ }
1716+
1717+ /// Compile-time check for a whole-record refined element type written to a
1718+ /// source: evaluate the record-level predicate against each constant row
1719+ /// literal in the written value. A passing row is right-by-construction; a
1720+ /// failing one is a compile error rather than a runtime write-abort. Rows
1721+ /// that aren't statically evaluable are skipped (the runtime write-check
1722+ /// still validates them).
1723+ fn check_const_rows_against_pred(
1724+ &mut self,
1725+ value: &ast::Expr,
1726+ type_name: &str,
1727+ pred: &ast::Expr,
1728+ ) {
1729+ let rows: Vec<&ast::Expr> = match &value.node {
1730+ ast::ExprKind::List(elems) => elems.iter().collect(),
1731+ // A single record literal written directly (no list wrapper).
1732+ ast::ExprKind::Record(fields) if !fields.is_empty() => vec![value],
1733+ _ => return,
1734+ };
1735+ for row in rows {
1736+ if let Some(false) = crate::codegen::eval_refine_predicate_on_const(pred, row) {
1737+ self.error(
1738+ format!(
1739+ "constant row does not satisfy the predicate for refined type `{type_name}`",
1740+ ),
1741+ row.span,
1742+ );
1743+ }
1744+ }
1745+ }
1746+
16201747 fn resolve_refined_base(&mut self, name: &str, span: Span) -> Option<Ty> {
16211748 let mut visited: Vec<String> = vec![name.to_string()];
16221749 let mut current = self.refined_types.get(name)?.0.clone();
@@ -7391,6 +7518,13 @@ impl Infer {
73917518 // The first value arg (if present in this same app)
73927519 // is CHECKED against the ascribed type.
73937520 if let Some(first) = value_args.next() {
7521+ // A constant ascribed to a refined type
7522+ // (`base.the (Nat) (0-5)`): evaluate the
7523+ // predicate now so a violating constant is a
7524+ // compile error, not a silent launder (the
7525+ // type-witness path bypasses the introduction
7526+ // guard and never touches a source write).
7527+ self.check_const_refined_intro(first, &ascribed);
73947528 self.check_expr(first, &ascribed);
73957529 result = ascribed.clone();
73967530 }
@@ -7573,6 +7707,18 @@ impl Infer {
75737707 // refined function parameters encountered inside the value.
75747708 let source_refined = self.refined_names_in(&target_inner);
75757709 let prev_suppress = self.suppress_refine_intro.replace(source_refined);
7710+ // Whole-record refined element type (`Rel VP` where `VP` is a
7711+ // record-level refined alias): the per-field check doesn't see
7712+ // the record-level predicate, so const-evaluate it here against
7713+ // each constant row literal. A passing constant is
7714+ // right-by-construction; a failing one is a compile error
7715+ // rather than a runtime write-abort. Non-constant rows defer to
7716+ // the runtime write-check as before.
7717+ if let Ty::Relation(elem) = self.apply(&target_inner).peel_alias() {
7718+ if let Some((ename, pred)) = self.record_refined_pred_for((**elem).clone()) {
7719+ self.check_const_rows_against_pred(value, &ename, &pred);
7720+ }
7721+ }
75767722 self.check_expr(value, &target_inner);
75777723 self.suppress_refine_intro = prev_suppress;
75787724 Ty::IO(Box::new(Ty::unit()))
@@ -7987,6 +8133,12 @@ ast::ExprKind::Atomic(inner) => {
79878133 for (param, p_ty) in params.iter().zip(peeled.iter()) {
79888134 self.check_pattern(param, p_ty);
79898135 }
8136+ // A constant returned where the declared return type is a
8137+ // refined type: evaluate the predicate at compile time so a
8138+ // violating constant is a build error (by-construction),
8139+ // rather than silently laundering it into the refined type
8140+ // with no check anywhere (it never touches a source write).
8141+ self.check_const_refined_intro(body, ¤t);
79908142 self.check_expr(body, ¤t);
79918143 self.pop_scope();
79928144 } else {
@@ -8058,7 +8210,45 @@ ast::ExprKind::Atomic(inner) => {
80588210 self.check_expr(&f.value, &sig_ty);
80598211 field_tys.insert(fname.clone(), sig_ty);
80608212 } else if let Some(exp_ty) = expected_fields.get(&fname) {
8061− self.check_expr(&f.value, exp_ty);
8213+ // Refined field with a statically-known value
8214+ // being introduced (the write path suppresses the
8215+ // introduction guard): verify the predicate at
8216+ // compile time instead of deferring to the runtime
8217+ // write-check. A constant that satisfies it is
8218+ // right-by-construction; one that violates it is a
8219+ // compile error, not a runtime abort. Non-constant
8220+ // values (None) fall through to the guarded check,
8221+ // which under suppression defers to the runtime.
8222+ let applied = self.apply(exp_ty);
8223+ if let Ty::Con(rname, rargs) = applied.peel_alias()
8224+ && rargs.is_empty()
8225+ && self.refined_types.contains_key(rname)
8226+ && self.refine_intro_suppressed(rname)
8227+ && let Some(lit) = crate::codegen::extract_literal_with_consts(
8228+ &f.value,
8229+ &self.const_literals,
8230+ )
8231+ {
8232+ let pred = self.refined_types.get(rname).unwrap().1.clone();
8233+ match crate::codegen::eval_refine_predicate_pub(&pred, &lit) {
8234+ Some(true) => {
8235+ let base =
8236+ self.resolve_refined_base(rname, f.value.span).unwrap_or_else(|| applied.clone());
8237+ self.check_expr(&f.value, &base);
8238+ }
8239+ Some(false) => {
8240+ self.error(
8241+ format!(
8242+ "field '{fname}' does not satisfy '{rname}' predicate",
8243+ ),
8244+ f.value.span,
8245+ );
8246+ }
8247+ None => self.check_expr(&f.value, exp_ty),
8248+ }
8249+ } else {
8250+ self.check_expr(&f.value, exp_ty);
8251+ }
80628252 field_tys.insert(fname.clone(), exp_ty.clone());
80638253 } else {
80648254 let val_ty = self.infer_expr(&f.value);
@@ -13823,9 +14013,13 @@ fn split_host_data_decls(src: &str) -> (CtorSets, String) {
1382314013 let mut rest = src;
1382414014 loop {
1382514015 let trimmed = rest.trim_start();
13826− // Host ADTs are declared `Name Ctor {} Ctor {f T}` — a leading
13827− // uppercase name, a gap, then whitespace-separated constructors.
13828− if !trimmed.starts_with(|c: char| c.is_uppercase()) {
14016+ // Host ADTs arrive as `data Name = Ctor {} Ctor {f T}` lines (rendered
14017+ // by the host) or, in the older in-tree form, `Name Ctor {} …`. A
14018+ // leading `data` keyword or uppercase name marks a decl; anything else
14019+ // (a bare type like `Int 1` or `Priority`) is the type to check.
14020+ let is_decl = trimmed.starts_with("data ")
14021+ || trimmed.starts_with(|c: char| c.is_uppercase());
14022+ if !is_decl {
1382914023 return (sets, trimmed.to_string());
1383014024 }
1383114025 let (line, next) = match trimmed.find('\n') {
@@ -13851,13 +14045,20 @@ fn split_host_data_decls(src: &str) -> (CtorSets, String) {
1385114045/// can re-parse them into real `Ty`s and unify against the snippet's payload
1385214046/// types. Returns `None` if the line isn't a well-formed variant decl.
1385314047fn parse_data_decl_ctors(line: &str) -> Option<(String, CtorList)> {
13854− // `Name` then a gap, then the constructor arms.
13855− let mut it = line.trim().splitn(2, char::is_whitespace);
14048+ // Wire form is `data Name = Ctor {} Ctor {f T}` (rendered by the host);
14049+ // the older in-tree form is `Name Ctor {} …`. Normalise both to
14050+ // `Name <ctor-arms>` before splitting.
14051+ let line = line.trim();
14052+ let line = line.strip_prefix("data ").unwrap_or(line).trim_start();
14053+ // `Name` then a gap (or ` = `), then the constructor arms.
14054+ let mut it = line.splitn(2, char::is_whitespace);
1385614055 let name = it.next()?.trim().to_string();
1385714056 let rhs = it.next()?;
1385814057 if name.is_empty() {
1385914058 return None;
1386014059 }
14060+ // Drop a leading `=` separating the name from the arms.
14061+ let rhs = rhs.trim_start().strip_prefix('=').map(str::trim_start).unwrap_or(rhs);
1386114062 // A decl body must contain a `{` (a constructor with a payload record);
1386214063 // a bare `Int 1` / `Priority` (the type to check) has none — not a decl.
1386314064 if !rhs.contains('{') {
@@ -14118,8 +14319,8 @@ fn check_adt_ctors(
1411814319 }
1411914320 };
1412014321 if !sets_ok {
14121− return false;
14122− }
14322+ return false;
14323+ }
1412314324 // Payload field types, at matching variance. The CONSUMED side destructures
1412414325 // the value, so every field it binds must be PRESENT in the produced side
1412514326 // with a subsumable type; extra fields on the produced side are ignored.