diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs
index dee8038..44d82ca 100644
--- a/crates/ailang-check/src/linearity.rs
+++ b/crates/ailang-check/src/linearity.rs
@@ -213,6 +213,12 @@ struct BinderState {
     /// for it. Invariant per binder; set at the introduction site
     /// (param / pattern / lam) where the type is locally available.
     is_value: bool,
+    /// For a function-typed binder (a HOF predicate param, or a
+    /// `let`/`lam`-bound function value), its declared parameter modes
+    /// — so `callee_arg_modes` can resolve `(app p h)` where `p` is a
+    /// local `(borrow …)` predicate and walk `h` as a borrow, not a
+    /// consume. `None` for a non-function binder.
+    fn_param_modes: Option<Vec<ParamMode>>,
 }
 
 /// top-level entry. Walks every fn in `m` and emits
@@ -346,6 +352,18 @@ fn strip_forall(t: &Type) -> &Type {
     }
 }
 
+/// Pull a function-typed value's declared parameter modes out of its
+/// type, unwrapping a leading `forall`. Returns `None` for any
+/// non-function type and for a fn-type with no explicit modes (legacy
+/// all-implicit), so a caller that gets `None` falls back to the
+/// global symbol table exactly as before.
+fn fn_modes_of(t: &Type) -> Option<Vec<ParamMode>> {
+    match strip_forall(t) {
+        Type::Fn { param_modes, .. } if !param_modes.is_empty() => Some(param_modes.clone()),
+        _ => None,
+    }
+}
+
 /// Per-fn check. Skips fns whose signature has any `Implicit` param —
 /// see module-level scope rules.
 fn check_fn(
@@ -398,6 +416,7 @@ fn check_fn(
                 ParamMode::Own | ParamMode::Implicit => 0,
             },
             is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
+            fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
         };
         checker.binders.insert(name.clone(), initial);
     }
@@ -521,14 +540,14 @@ impl<'a> Checker<'a> {
             }
             Term::Let { name, value, body } => {
                 self.walk(value, Position::Consume);
-                let is_value = self
+                let teed = self
                     .let_binder_types
-                    .get(&(self.def_name.to_string(), name.clone()))
-                    .map(type_is_value)
-                    .unwrap_or(false);
+                    .get(&(self.def_name.to_string(), name.clone()));
+                let is_value = teed.map(type_is_value).unwrap_or(false);
+                let fn_param_modes = teed.and_then(|t| fn_modes_of(t));
                 self.with_binder(
                     name,
-                    BinderState { is_value, ..BinderState::default() },
+                    BinderState { is_value, fn_param_modes, ..BinderState::default() },
                     |this| {
                         this.walk(body, pos);
                     },
@@ -609,6 +628,7 @@ impl<'a> Checker<'a> {
                     saved_for_params.insert(p.clone(), self.binders.remove(p));
                     let st = BinderState {
                         is_value: param_tys.get(i).map(type_is_value).unwrap_or(false),
+                        fn_param_modes: param_tys.get(i).and_then(|t| fn_modes_of(t)),
                         ..BinderState::default()
                     };
                     self.binders.insert(p.clone(), st);
@@ -767,19 +787,30 @@ impl<'a> Checker<'a> {
 
     /// Resolve the param-mode vector of a fn-call's callee.
     ///
-    /// Currently only handles `callee = Term::Var { name }` resolving
-    /// to a global fn type (with explicit `param_modes`). All other
-    /// callee shapes return an empty vec → all args default to
-    /// Consume. This is the conservative, "no false negatives on the
-    /// borrow-arg case" behaviour: if we can't see the modes, we
-    /// assume Consume and may miss a borrow.
+    /// For `callee = Term::Var { name }`, a local function-typed binder
+    /// (a HOF predicate param, or a `let`/`lam`-bound function value)
+    /// carrying `fn_param_modes` is resolved first, then a global fn
+    /// type (with explicit `param_modes`). All other callee shapes
+    /// return an empty vec → all args default to Consume. This is the
+    /// conservative, "no false negatives on the borrow-arg case"
+    /// behaviour: if we can't see the modes, we assume Consume and may
+    /// miss a borrow.
     fn callee_arg_modes(&self, callee: &Term, n_args: usize) -> Vec<ParamMode> {
         let name = match callee {
             Term::Var { name } => name,
             _ => return vec![],
         };
-        // Locals never carry fn-types in 18c.2 (no first-class fn vars
-        // with mode info). Look up the global symbol table.
+        // A local function-typed binder (HOF predicate param, or a
+        // `let`/`lam`-bound function value) carries its declared arg
+        // modes on its `BinderState`. Prefer those over the global
+        // table so `(app p h)` with `p` a local `(borrow …)` predicate
+        // borrows `h` instead of consuming it. A local binder shadows a
+        // global of the same name, which is the correct lexical scope.
+        if let Some(s) = self.binders.get(name) {
+            if let Some(modes) = &s.fn_param_modes {
+                return modes.clone();
+            }
+        }
         let ty = match self.globals.get(name) {
             Some(t) => t,
             None => {
@@ -1477,6 +1508,111 @@ mod tests {
         );
     }
 
+    /// fn f(p0: (borrow (List -> Bool, inner arg Borrow)), h: (own List)).
+    /// The inner predicate's arg is `Borrow`, so applying `p0` to `h`
+    /// borrows `h` (it stays reusable). Used by the class-1 tests.
+    fn fn_with_borrow_pred_and_heap(name: &str, body: Term) -> Def {
+        let list = Type::Con { name: "List".into(), args: vec![] };
+        Def::Fn(FnDef {
+            name: name.into(),
+            ty: Type::Fn {
+                params: vec![
+                    Type::Fn {
+                        params: vec![list.clone()],
+                        param_modes: vec![ParamMode::Borrow],
+                        ret: Box::new(Type::bool_()),
+                        ret_mode: ParamMode::Own,
+                        effects: vec![],
+                    },
+                    list.clone(),
+                ],
+                param_modes: vec![ParamMode::Borrow, ParamMode::Own],
+                ret: Box::new(Type::int()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+            params: vec!["p0".into(), "h".into()],
+            body,
+            suppress: vec![],
+            doc: None,
+            export: None,
+        })
+    }
+
+    /// Class 1 (param path): a local borrow-mode predicate param `p0`
+    /// applied to a heap binder `h` (`(seq (app p0 h) h)`) does NOT
+    /// consume `h` — `p0`'s declared `(borrow …)` arg mode makes the
+    /// application a borrow, so `h` is reusable. RED until the
+    /// local-fn-param-mode resolution lands.
+    #[test]
+    fn borrow_fn_param_applied_does_not_consume_heap_arg() {
+        let body = Term::Seq {
+            lhs: Box::new(Term::App {
+                callee: Box::new(Term::Var { name: "p0".into() }),
+                args: vec![Term::Var { name: "h".into() }],
+                tail: false,
+            }),
+            rhs: Box::new(Term::Var { name: "h".into() }),
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![fn_with_borrow_pred_and_heap("f", body)],
+        };
+        let diags = check_module(&m);
+        assert!(
+            !diags.iter().any(|d| d.code == "use-after-consume"),
+            "applying a borrow-mode predicate param borrows its arg; got {diags:?}"
+        );
+    }
+
+    /// Class 1 (let path): a `let`-bound function value whose type is
+    /// teed as a `(borrow …)` predicate resolves its modes from the
+    /// LetBinderTypes table — applying it to heap binder `h` borrows
+    /// `h`. The let-value term is a trivial literal; the hand-built
+    /// table is the unit under test.
+    #[test]
+    fn borrow_fn_let_binder_applied_does_not_consume_heap_arg() {
+        let body = Term::Let {
+            name: "g".into(),
+            value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
+            body: Box::new(Term::Seq {
+                lhs: Box::new(Term::App {
+                    callee: Box::new(Term::Var { name: "g".into() }),
+                    args: vec![Term::Var { name: "p0".into() }],
+                    tail: false,
+                }),
+                rhs: Box::new(Term::Var { name: "p0".into() }),
+            }),
+        };
+        let m = Module {
+            schema: ailang_core::SCHEMA.into(),
+            name: "t".into(),
+            kernel: false,
+            imports: vec![],
+            defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
+        };
+        let list = Type::Con { name: "List".into(), args: vec![] };
+        let mut lbt = LetBinderTypes::new();
+        lbt.insert(
+            ("f".into(), "g".into()),
+            Type::Fn {
+                params: vec![list.clone()],
+                param_modes: vec![ParamMode::Borrow],
+                ret: Box::new(Type::bool_()),
+                ret_mode: ParamMode::Own,
+                effects: vec![],
+            },
+        );
+        let diags = check_module_with_visible(&m, &[], &lbt);
+        assert!(
+            !diags.iter().any(|d| d.code == "use-after-consume"),
+            "a let-bound borrow predicate borrows its arg via the teed modes; got {diags:?}"
+        );
+    }
+
     /// A fn with one `(own (con Int))` value-type param `p0`, returning
     /// Int. Used to exercise the value-type exemption.
     fn fn_with_int_own(name: &str, body: Term) -> Def {
diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs
index 98807d5..161462c 100644
--- a/crates/ailang-check/tests/workspace.rs
+++ b/crates/ailang-check/tests/workspace.rs
@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
 /// is active today) and were RED before the hardening (docs/specs/0063).
 #[test]
 fn harden_ownership_false_positives_are_clean() {
-    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let"] {
+    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof"] {
         let entry = examples_dir().join(format!("{name}.ail"));
         let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
         let diags = check_workspace(&ws);
diff --git a/examples/c1_local_hof.ail b/examples/c1_local_hof.ail
new file mode 100644
index 0000000..a8e124c
--- /dev/null
+++ b/examples/c1_local_hof.ail
@@ -0,0 +1,23 @@
+(module c1_local_hof
+  (data Box
+    (doc "heap cell")
+    (ctor Box (con Int)))
+  (data List
+    (doc "boxed list of boxes")
+    (ctor Nil)
+    (ctor Cons (con Box) (con List)))
+  (fn filter_box
+    (doc "borrow-mode predicate p applied to h; h reused in the kept Cons")
+    (type
+      (fn-type
+        (params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool)))))
+                (own (con List)))
+        (ret (own (con List)))))
+    (params p xs)
+    (body
+      (match xs
+        (case (pat-ctor Nil) (term-ctor List Nil))
+        (case (pat-ctor Cons h t)
+          (if (app p h)
+            (term-ctor List Cons h (app filter_box p t))
+            (app filter_box p t)))))))