From 73f58826cc9468b748ee73bbb7ff5693fbb73c69 Mon Sep 17 00:00:00 2001
From: Xingyu Xie <namasikanam@gmail.com>
Date: Fri, 21 Aug 2026 13:55:13 +0200
Subject: [PATCH] fix(conv): check operator type-arguments in applied-op
 convertibility
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The `Fapp(Fop(p1,_), _), Fapp(Fop(p2,_), _)` shortcut in `conv`
(ecReduction.ml) treated two applications of the same operator path as
convertible without comparing their type-argument lists. When the type
parameter is "phantom" (present in the operator's definition but reducing
out of its head arrow type), distinct instantiations were wrongly declared
equal.

This is unsound: `reflexivity` proves
  wrap<:bool> 0 = wrap<:unit> 0
for `op wrap ['a] (x:int):int = size (to_seq<:'a> predT)`, while the
stdlib pins those to |bool|=2 and |unit|=1 — yielding a proof of `false`
with no axioms.

The fix mirrors the unapplied `Fop, Fop` case (a few lines above) and
`is_alpha_eq`, both of which already check `List.all2 for_type`. The
change only makes conversion stricter (on a type-arg mismatch it falls
through to the general head-conversion / unfolding path), so it cannot
introduce new conversions; genuinely-true phantom equations still convert
via unfolding.

Adds tests/conv-typeargs.ec, a regression test using `fail reflexivity`:
it compiles once the bug is fixed and fails to compile if it regresses.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
---
 src/ecReduction.ml     |  3 ++-
 tests/conv-typeargs.ec | 16 ++++++++++++++++
 2 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/conv-typeargs.ec

diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index 16d28b43e..036648e58 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -1519,7 +1519,8 @@ let rec conv ri env f1 f2 stk =
         && List.length args1 = List.length args2 -> begin
     (* So that we do not unfold operators *)
     match f1'.f_node, f2'.f_node with
-    | Fop(p1, _), Fop(p2, _) when EcPath.p_equal p1 p2 ->
+    | Fop(p1, tys1), Fop(p2, tys2)
+        when EcPath.p_equal p1 p2 && List.all2 (EqTest_i.for_type env) tys1 tys2 ->
       conv_next ri env f1' (zapp args1 args2 f1.f_ty stk)
     | _, _ ->
       conv ri env f1' f2' (zapp args1 args2 f1.f_ty stk)
diff --git a/tests/conv-typeargs.ec b/tests/conv-typeargs.ec
new file mode 100644
index 000000000..f5e7d9c21
--- /dev/null
+++ b/tests/conv-typeargs.ec
@@ -0,0 +1,16 @@
+(* -------------------------------------------------------------------- *)
+(* Regression test: conversion must compare operator type-arguments.
+
+   `wrap`'s type parameter ['a] is "phantom": it occurs only in the body,
+   so `wrap`'s head type is `int -> int` for every instantiation.  A bug in
+   the applied-operator convertibility shortcut (ecReduction.ml) dropped the
+   type-argument lists, so `reflexivity` wrongly closed
+     wrap<:bool> 0 = wrap<:unit> 0
+   even though those are |bool| = 2 and |unit| = 1 — a proof of `false`.
+   `reflexivity` must now be rejected here.                              *)
+require import AllCore List Finite.
+
+op wrap ['a] (x : int) : int = size (to_seq<:'a> predT).
+
+lemma conv_typeargs_phantom : wrap<:bool> 0 = wrap<:unit> 0.
+proof. fail reflexivity. abort.