diff --git a/doc/changelog/03-notations/17841-master+fixes15221-invalid-eta-expansion-notation.rst b/doc/changelog/03-notations/17841-master+fixes15221-invalid-eta-expansion-notation.rst
new file mode 100644
index 000000000000..6578780ba0c4
--- /dev/null
+++ b/doc/changelog/03-notations/17841-master+fixes15221-invalid-eta-expansion-notation.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  An invalid case of eta-expansion in notation pretty-printer
+  (`#17841 <https://github.com/coq/coq/pull/17841>`_,
+  fixes `#15221 <https://github.com/coq/coq/issues/15221>`_,
+  by Hugo Herbelin).
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index cf0d8bda59af..b23596448099 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1403,6 +1403,11 @@ let does_not_come_from_already_eta_expanded_var glob =
   (* checked). *)
   match DAst.get glob with GVar _ -> false | _ -> true
 
+let eta_well_typed pat =
+  (* A criterion for well-typedness of the eta-expansion
+     is that the head of the pattern is rigid (see #15221) *)
+  match pat with NVar _ -> false | _ -> true
+
 let is_var_term = function
   (* The kind of expressions allowed to be both a term and a binding variable *)
   | GVar _ -> true
@@ -1446,7 +1451,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
         else if n1 > n2 then
           let l11,l12 = List.chop (n1-n2) l1 in DAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
         else f1,l1, f2, l2 in
-      let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
+      let may_use_eta = does_not_come_from_already_eta_expanded_var f1 && eta_well_typed f2 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_hd u alp metas sigma f1 f2) l1 l2
   | GProj ((cst1,u1),l1,a1), NProj ((cst2,u2),l2,a2) when GlobRef.CanOrd.equal (GlobRef.ConstRef cst1) (GlobRef.ConstRef cst2) && compare_glob_universe_instances_le u1 u2 ->
diff --git a/interp/notationextern.ml b/interp/notationextern.ml
index 35227e098458..a75b53107bd3 100644
--- a/interp/notationextern.ml
+++ b/interp/notationextern.ml
@@ -176,6 +176,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
       RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
   | NApp (NList (_,_,NApp (_,args),_,_), args') ->
       Oth, AppBoundedNotation (List.length args + List.length args')
+  | NApp (NVar _,_) -> Oth, AppUnboundedNotation
   | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
   | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
   | _ -> Oth, NotAppNotation
diff --git a/test-suite/output/bug_15221.out b/test-suite/output/bug_15221.out
new file mode 100644
index 000000000000..3d1fd6ba0e66
--- /dev/null
+++ b/test-suite/output/bug_15221.out
@@ -0,0 +1,7 @@
+chain =
+fun x y : nat => let/c f := foo x y in
+                 let/c b := bar x y in
+                 f = b
+     : nat -> nat -> Prop
+
+Arguments chain (x y)%nat_scope
diff --git a/test-suite/output/bug_15221.v b/test-suite/output/bug_15221.v
new file mode 100644
index 000000000000..3e8cc1cf8252
--- /dev/null
+++ b/test-suite/output/bug_15221.v
@@ -0,0 +1,16 @@
+Definition foo{A}(a b: nat)(k: nat -> A): A :=
+  k (a + b).
+
+Definition bar{A}(a b: nat)(k: nat -> A): A :=
+  k (a - b).
+
+Notation "'let/c' x := r 'in' b" := (r (fun x => b))
+  (x binder, at level 200, right associativity,
+   format "'[hv' 'let/c'  x  :=  r  'in'  '//' b ']'").
+
+Definition chain(x y: nat): Prop :=
+  let/c f := foo x y in
+  let/c b := bar x y in
+  f = b.
+
+Print chain.