fix(fixpoint): matchfix termination check must descend into all call arguments

src/ecHiInductive.ml

@@ -466,7 +466,12 @@ let trans_matchfix
         match destr_app e with
         | ({ e_node = Elocal x }, args) when x = opname -> begin
           match List.nth_opt args pos with
-          | Some { e_node = Elocal a } when Sid.mem a pvars -> ()
+          | Some { e_node = Elocal a } when Sid.mem a pvars ->
+            (* The decreasing argument is a valid structural subterm, but the
+               OTHER arguments may themselves hide a non-decreasing recursive
+               call (e.g. `f k (! (f n b))` with n the whole input). Descend
+               into every argument so such calls are also checked. *)
+            List.iter check_body args
           | _ -> fxerror loc env TT.FXE_SynCheckFailure
           end
         | _ -> EcTypes.e_iter check_body e

tests/matchfix-termination.ec

@@ -0,0 +1,15 @@
+(* Regression for the matchfix termination-check hole.
+
+   `check_body` (ecHiInductive.ml) accepts a recursive call whose decreasing
+   argument is a valid structural subterm, but used to return without checking
+   the call's OTHER arguments -- so a non-decreasing recursive call hidden in a
+   sibling argument escaped. The op below defines `f (S Z) b = ! (f (S Z) b)`
+   (i.e. `f x = not (f x)`), which has no total-function solution and makes the
+   logic inconsistent. It MUST be rejected by the termination check. *)
+require import AllCore.
+
+type t = [ Z | S of t ].
+
+fail op f (n : t) (b : bool) : bool =
+  with n = Z   => b
+  with n = S k => f k (! (f n b)).