fix(conv): check operator type-arguments in applied op-convertibility

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)

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.