Merge PR #17841: Fixes #15221: a case of invalid eta-expansion in not…

…ation printing

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

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).

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 ->

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

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

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.