A field keeps what its type said

CHANGELOG.md

@@ -20,6 +20,34 @@ release notes.
 
 ### Diagnostics
 
+- 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:
+
+  ```deed
+  record Held { by: Positive }
+
+  fn needs(n: Positive) -> Int where n > 0, { n }
+
+  fn through(h: Held) -> Int { needs(h.by) }   // was Guarded, is Proven
+  ```
+
+  The value has no name at that call for anything to have narrowed, and no
+  contract answered for it, so the only thing that knew anything was the type
+  the record was declared with — and nothing asked it. The comment in
+  `facts.rs` said so: "every other field read is a value nothing here knows".
+
+  It knows now, and only that. A field declared plainly is still a value
+  nothing knows, and a refinement the interval machinery cannot hold still
+  carries nothing either way: `value != 0` admits everything but one number,
+  which is two intervals and not one. That is a limit of what `Facts` keeps
+  rather than of fields, and it is the half that still stops `std/ratio` from
+  proving `simplified`'s `bottom != 0` at its call sites — along with the
+  product of two numbers, which no interval bounds.
+
+  No obligation in the corpus moves: the records there are declared with plain
+  `Int`. What moved is that the compiler stopped losing something it had.
+
 - `deed explain` showed programs that do not produce the code being explained.
   Forty-three of the eighty-nine pages carrying an example, measured by
   checking each one and running its tests. The example was "the first

crates/deed-driver/tests/proving.rs

@@ -1480,3 +1480,53 @@ fn a_value_nothing_is_known_about_gets_no_invented_number() {
     );
     assert!(!text.contains("when this is"), "{text}");
 }
+/// A refinement written on a record's field survives reading the field back.
+///
+/// A parameter of type `Positive` is already known to be positive; a field
+/// declared `Positive` was not, and the two say the same thing. The value has
+/// no name here for anything to have narrowed, so the only thing that knows
+/// is the type the record was declared with, and until this the only place
+/// that survived was the literal that built it.
+#[test]
+fn a_field_declared_with_a_refinement_carries_it_when_it_is_read() {
+    expect_each(
+        &[("needs requires", Tier::Proven)],
+        "\
+         record Held { by: Positive }\n\n\
+         fn needs(n: Positive) -> Int\n  where\n    n > 0,\n{\n    n\n}\n\n\
+         fn through(h: Held) -> Int { needs(h.by) }\n",
+    );
+}
+
+/// And a plain field still knows nothing, so this is the type talking rather
+/// than field reads having quietly become trustworthy.
+#[test]
+fn a_field_declared_without_one_is_still_a_value_nothing_knows() {
+    expect_each(
+        &[
+            ("needs requires", Tier::Guarded),
+            ("Positive", Tier::Guarded),
+        ],
+        "\
+         record Held { by: Int }\n\n\
+         fn needs(n: Positive) -> Int\n  where\n    n > 0,\n{\n    n\n}\n\n\
+         fn through(h: Held) -> Int { needs(h.by) }\n",
+    );
+}
+
+/// A refinement the interval machinery cannot hold is still not held.
+///
+/// `value != 0` admits everything but one number, which is two intervals and
+/// not one, so a field declared with it carries nothing. The type is not the
+/// limit here and neither is the field: it is that `Facts` keeps ranges.
+#[test]
+fn a_refinement_that_is_not_an_interval_carries_nothing_either_way() {
+    expect_each(
+        &[("needs requires", Tier::Guarded)],
+        "\
+         type NonZero = Int where value != 0\n\n\
+         record Held { by: NonZero }\n\n\
+         fn needs(n: NonZero) -> Int\n  where\n    n != 0,\n{\n    n\n}\n\n\
+         fn through(h: Held) -> Int { needs(h.by) }\n",
+    );
+}

crates/deed-typeck/src/check.rs

@@ -1254,10 +1254,12 @@ impl<'a> Checker<'a> {
         match &requires.origin {
             Origin::Here { .. } => {
                 let (def_of, call) = self.env();
+                let refined = self.refinements();
                 let env = facts::Env {
                     def_of: &def_of,
                     length: self.resolutions.builtin("length"),
                     call: &call,
+                    refined: &refined,
                 };
                 facts::holds(clause, facts, &env)
             }
@@ -1270,6 +1272,9 @@ impl<'a> Checker<'a> {
                     def_of: &def_of,
                     length: Some(imported_name(ClauseName::Length)),
                     call: &|_| Promise::any(),
+                    // No type table on this side of the boundary, and the
+                    // clause arrived without one.
+                    refined: &|_| Range::ANY,
                 };
                 let outcome = facts::holds(clause, facts, &env);
                 facts::thinned_by_boundary(clause, &env, outcome)
@@ -1305,10 +1310,12 @@ impl<'a> Checker<'a> {
             // brings its own size.
             let length = {
                 let (def_of, call) = self.env();
+                let refined = self.refinements();
                 let env = facts::Env {
                     def_of: &def_of,
                     length: self.resolutions.builtin("length"),
                     call: &call,
+                    refined: &refined,
                 };
                 facts::length_of(arg, &self.facts, &env)
             };
@@ -1336,10 +1343,12 @@ impl<'a> Checker<'a> {
     /// What a fact could be attached to, for an expression in this body.
     fn term_of(&self, expr: &Expr) -> Option<facts::Term> {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::term_of(expr, &env)
     }
@@ -2046,10 +2055,14 @@ impl<'a> Checker<'a> {
         match &alias.refinement {
             Some(predicate) => {
                 let (def_of, call) = self.env();
+                // Blind about fields on purpose: a predicate is read against
+                // `value`, and asking what a field read in it admits would
+                // come straight back here for the type being read.
                 let env = facts::Env {
                     def_of: &def_of,
                     length: self.resolutions.builtin("length"),
                     call: &call,
+                    refined: &|_| Range::ANY,
                 };
                 facts::admitted_by(predicate, &env)
             }
@@ -2130,59 +2143,87 @@ impl<'a> Checker<'a> {
         (self.resolver(), |callee: &Expr| self.call_promise(callee))
     }
 
+    /// What a declared type admits, as the fact machinery asks it.
+    fn refinements(&self) -> impl Fn(&Expr) -> Range + '_ {
+        |expr: &Expr| self.refined_range(expr)
+    }
+
+    /// What this expression's declared type admits, when that type is refined.
+    ///
+    /// The type table rather than the facts, because the value has no name
+    /// here for anything to have narrowed. A record declaring `bottom:
+    /// Positive` has said its field is positive, and until this existed the
+    /// only place that survived was the literal that built it.
+    fn refined_range(&self, expr: &Expr) -> Range {
+        match self.types.type_of(expr.span()) {
+            Some(Ty::Named { def, .. }) => self.refinement_range(*def),
+            _ => Range::ANY,
+        }
+    }
+
     fn narrowed_by(&self, condition: &Expr, when_true: bool) -> Facts {
         self.narrowed_from(&self.facts, condition, when_true)
     }
 
     fn narrowed_from(&self, base: &Facts, condition: &Expr, when_true: bool) -> Facts {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::narrowed(condition, base, &env, when_true)
     }
 
     fn range_of(&self, expr: &Expr) -> Range {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::range_of(expr, &self.facts, &env)
     }
 
     /// The range the value inside the `ok` of `expr` lands in.
     fn ok_range_of(&self, expr: &Expr) -> Range {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::ok_range_of(expr, &self.facts, &env)
     }
 
     /// What is known about how long an expression is.
     fn length_of(&self, expr: &Expr) -> Range {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::length_of(expr, &self.facts, &env)
     }
 
     /// Where the arithmetic in `expr` can have no answer, if anywhere.
     fn overflowing(&self, expr: &Expr) -> Option<Span> {
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::overflowing(expr, &self.facts, &env)
     }
@@ -2198,10 +2239,12 @@ impl<'a> Checker<'a> {
         };
         let with_subject = self.facts.with_subject(subject);
         let (def_of, call) = self.env();
+        let refined = self.refinements();
         let env = facts::Env {
             def_of: &def_of,
             length: self.resolutions.builtin("length"),
             call: &call,
+            refined: &refined,
         };
         facts::holds(predicate, &with_subject, &env)
     }

crates/deed-typeck/src/facts.rs

@@ -816,6 +816,7 @@ pub fn promised_by(condition: &Expr, subject: &str, names: &[&str]) -> Guarantee
         def_of: &def_of,
         length: None,
         call: &|_| Promise::any(),
+        refined: &|_| Range::ANY,
     };
 
     let mut facts = Facts::new();
@@ -953,6 +954,15 @@ pub struct Env<'a> {
     /// answering for contracts that are themselves checked, since a promise
     /// nobody keeps is not a fact.
     pub call: &'a dyn Fn(&Expr) -> Promise,
+    /// What this expression's declared type admits, when that type is refined.
+    ///
+    /// A name carries what the body worked out about it, and a call carries
+    /// what its contract promises. A field read has neither: nothing narrowed
+    /// it here and no contract answered for it, and the only thing that knows
+    /// anything is the type the record declared the field with. Answered by
+    /// whoever has the type table, since this module has none, and answered
+    /// with [`Range::ANY`] when the type says nothing.
+    pub refined: &'a dyn Fn(&Expr) -> Range,
 }
 
 impl Env<'_> {
@@ -962,6 +972,7 @@ impl Env<'_> {
             def_of: &|_| None,
             length: None,
             call: &|_| Promise::any(),
+            refined: &|_| Range::ANY,
         }
     }
 }
@@ -1391,11 +1402,13 @@ fn interval_of(expr: &Expr, facts: &Facts, env: &Env<'_>) -> Range {
     match expr {
         Expr::Int { value, .. } => Range::exactly(*value),
         // `Int.max` is the number, so a clause naming it is one the checker
-        // can settle rather than guard. Every other field read is a value
-        // nothing here knows.
+        // can settle rather than guard. Otherwise the only thing that knows
+        // anything about a field is the type it was declared with: a record
+        // saying `bottom: Positive` has said it, and reading the field back
+        // used to lose it.
         Expr::Field { .. } => match expr.int_limit() {
             Some(value) => Range::exactly(value),
-            None => Range::ANY,
+            None => (env.refined)(expr),
         },
         Expr::Ident(_) => match term_of(expr, env) {
             Some(term) => facts.get(term),
@@ -2235,6 +2248,7 @@ mod tests {
             },
             length: Some(DefId::from_raw(1)),
             call: &|_| Promise::any(),
+            refined: &|_| Range::ANY,
         }
     }