The obligation the caller owns

CHANGELOG.md

@@ -20,6 +20,26 @@ release notes.
 
 ### Diagnostics
 
+- An obligation nobody could ever prove no longer reads like one nobody has got
+  round to. Every `ensures` clause that came back `Guarded` said "nothing tries
+  to prove this one ahead of time"; seven of the nine in `examples/` are about
+  an effect, and those are not waiting on anything:
+
+  ```deed
+  fn peek() -> Int uses Counter.value, ensures ok => unchanged(Counter), { .. }
+  ```
+
+  A function is checked once. The `with` block deciding what `Counter` means is
+  written by whoever calls it, and a different caller may install a different
+  handler, so no pass on this side settles that clause however hard it tries.
+  Those now say the caller installs the handler that answers it, which is the
+  one reason here whose answer to "what would make this Proven" is nothing.
+
+  The two left saying "nothing tries" are `transfer`'s `result.from == from`
+  and `result.amount == amount`, which really are obligations a checker could
+  one day discharge. Splitting the count is what makes the difference visible:
+  `design/02-syntax.md` now reports both rows separately.
+
 - A refinement written on a record's field survives reading the field back.
   A parameter of type `Positive` was already known to be positive; a field
   declared `Positive` was not, and the two say the same thing:

crates/deed-ast/src/lib.rs

@@ -799,6 +799,94 @@ impl Expr {
     }
 }
 
+/// Every expression one step inside `expr`.
+///
+/// Here rather than in a pass, because which expressions are inside another
+/// one is a fact about the tree and every reader of it wants the same answer.
+/// The interpreter used to keep this and had written it out twice before that;
+/// both copies stopped in the same place, a closure body, and `DEED6006`'s own
+/// note describes the hole that left.
+///
+/// Matched without a wildcard, so a new kind of expression is a build error
+/// here rather than a walk that silently stops covering it.
+pub fn children<'a>(expr: &'a Expr, out: &mut Vec<&'a Expr>) {
+    match expr {
+        Expr::Field { receiver, .. } => out.push(receiver),
+        Expr::Call { callee, args, .. } => {
+            out.push(callee);
+            out.extend(args);
+        }
+        Expr::List { elements, .. } => out.extend(elements),
+        Expr::StructLit { path, fields, .. } => {
+            out.push(path);
+            out.extend(fields.iter().filter_map(|field| field.value.as_ref()));
+        }
+        Expr::Unary { operand, .. } | Expr::Try { operand, .. } => out.push(operand),
+        Expr::Binary { lhs, rhs, .. } => {
+            out.push(lhs);
+            out.push(rhs);
+        }
+        Expr::If {
+            condition,
+            then_branch,
+            else_branch,
+            ..
+        } => {
+            out.push(condition);
+            block_children(then_branch, out);
+            out.extend(else_branch.as_deref());
+        }
+        Expr::Match {
+            scrutinee, arms, ..
+        } => {
+            out.push(scrutinee);
+            out.extend(arms.iter().map(|arm| &arm.body));
+        }
+        Expr::For {
+            iterable,
+            accumulator,
+            keep,
+            body,
+            ..
+        } => {
+            out.push(iterable);
+            out.extend(accumulator.iter().map(|acc| acc.init.as_ref()));
+            out.extend(keep.as_deref());
+            block_children(body, out);
+        }
+        Expr::Block(block) => block_children(block, out),
+        Expr::Closure { body, .. } => out.push(body),
+        Expr::Old { expr, .. } => out.push(expr),
+        Expr::With { handlers, body, .. } => {
+            out.extend(handlers);
+            block_children(body, out);
+        }
+        Expr::Int { .. }
+        | Expr::Str { .. }
+        | Expr::Bool { .. }
+        | Expr::Unit(_)
+        | Expr::Ident(_)
+        | Expr::Unchanged { .. }
+        | Expr::Error(_) => {}
+    }
+}
+
+/// Every expression one step inside a block.
+pub fn block_children<'a>(block: &'a Block, out: &mut Vec<&'a Expr>) {
+    for stmt in &block.stmts {
+        match stmt {
+            Stmt::Let { init, .. } => out.push(init),
+            Stmt::Assign { value, .. } => out.push(value),
+            Stmt::Return { value, .. } => out.extend(value),
+            Stmt::Assert { condition, .. } => out.push(condition),
+            Stmt::Refuses { subject, .. } => out.push(subject),
+            Stmt::Expr(expr) => out.push(expr),
+            Stmt::Abandon { .. } => {}
+        }
+    }
+    out.extend(block.tail.as_deref());
+}
+
 #[derive(Clone, Debug)]
 pub struct PatternField {
     pub name: Ident,

crates/deed-driver/src/lib.rs

@@ -110,13 +110,13 @@ mod clock_tests {
     }
 }
 
-use deed_ast::{Item, Module, Outcome};
+use deed_ast::{Expr, Item, Module, Outcome, children};
 use deed_diagnostics::{Diagnostic, FileId, Severity, SourceMap, Span};
 use deed_effects::Effects;
 use deed_interp::{DeclaredRows, Guard, Guards, OperatorCalls, Program, RowItem};
 use deed_lexer::tokenize;
 use deed_parser::parse;
-use deed_resolve::{Resolutions, Universe};
+use deed_resolve::{DefKind, Resolutions, Universe};
 use deed_typeck::{Reason, Tier, Types, World};
 
 /// One obligation and how it was discharged.
@@ -565,12 +565,13 @@ fn check_parsed(
     // can be generated gets exercised by a property test as well, which is the
     // `Tested` tier and the only place it comes from.
     //
-    // A guarded one carries `NothingTriesToProveThis` rather than no reason at
-    // all. The distinction matters more here than anywhere else: the other
-    // guarded obligations are the checker having looked and failed, and these
-    // are the checker never having looked, and until this said so the two were
-    // the same word with nothing to tell them apart. Thirteen of the sixteen
-    // guarded obligations in `examples/` are this case.
+    // A guarded one says why it is guarded, and there are two answers. Most of
+    // these clauses are about an effect, and the `with` block that decides
+    // what the effect means belongs to whoever calls the function: nothing
+    // here can settle those, ever. The rest are simply not attempted, which is
+    // the checker never having looked rather than having looked and failed.
+    // Until these two were told apart, an obligation nobody could ever prove
+    // read the same as one nobody had got round to.
     for item in &parsed_module.items {
         let Item::Function(function) = item else {
             continue;
@@ -592,7 +593,12 @@ fn check_parsed(
                 // answer rather than the absence of one.
                 reason: match tested {
                     true => None,
-                    false => Some(deed_typeck::facts::Reason::NothingTriesToProveThis),
+                    false => Some(
+                        match reaches_an_effect(&obligation.condition, &resolved.resolutions) {
+                            true => Reason::TheCallerInstallsTheHandler,
+                            false => Reason::NothingTriesToProveThis,
+                        },
+                    ),
                 },
             });
         }
@@ -612,6 +618,41 @@ fn check_parsed(
     }
 }
 
+/// Whether a contract clause talks about an effect.
+///
+/// Two shapes reach one: `unchanged(Ledger)`, which names an effect and
+/// nothing else, and any mention of an operation, whether it is performed
+/// directly or read through `old(...)`. Both mean the same thing for the
+/// tier, and it is a fact about the caller rather than about this function:
+/// the body is checked once, and which handler answers is decided by whoever
+/// wrote the `with` block above the call.
+///
+/// Asked of the resolver rather than of the text, so an effect called
+/// `unchanged` or a local called `Ledger` cannot fool it.
+///
+/// A bare name is not asked, because an operation is declared as a member of
+/// its effect and there is no scope a bare name could find one in: every
+/// mention of one is `Effect.operation`, whether it is being called or handed
+/// on as a value. Asking anyway was a branch no program could reach.
+fn reaches_an_effect(expr: &Expr, resolutions: &Resolutions) -> bool {
+    if let Expr::Unchanged { .. } = expr {
+        return true;
+    }
+    let operation = match expr {
+        Expr::Field { name, .. } => resolutions.resolution(name.span),
+        _ => None,
+    }
+    .is_some_and(|def| resolutions.def(def).kind == DefKind::EffectOp);
+    if operation {
+        return true;
+    }
+    let mut inside = Vec::new();
+    children(expr, &mut inside);
+    inside
+        .into_iter()
+        .any(|child| reaches_an_effect(child, resolutions))
+}
+
 /// Convenience for callers holding text rather than a populated map.
 pub fn check_text(
     sources: &mut SourceMap,