diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 6191c7300..4110f090e 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -500,12 +500,22 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr =
       let defl = EcEnv.Fun.by_xpath fl env in
       let defr = EcEnv.Fun.by_xpath fr env in
       let sigl, sigr = defl.f_sig, defr.f_sig in
-      let testty =
-           EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg
-        && EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret
-      in
+      let ppe = EcPrinting.PPEnv.ofenv env in
+
+      if not (EcReduction.EqTest.for_type env sigl.fs_arg sigr.fs_arg)
+      then tc_error _pf "@[<v 2>the procedures do not have the same argument types:@,\
+          Left side:  @[<h>%a@]@,\
+          Right side: @[<h>%a@]@]"
+        (EcPrinting.pp_type ppe) sigl.fs_arg
+        (EcPrinting.pp_type ppe) sigr.fs_arg;
+
+      if not (EcReduction.EqTest.for_type env sigl.fs_ret sigr.fs_ret)
+      then tc_error _pf "@[<v 2>the procedures do not have the same return types:@,\
+          Left side:  @[<h>%a@]@,\
+          Right side: @[<h>%a@]@]"
+        (EcPrinting.pp_type ppe) sigl.fs_ret
+        (EcPrinting.pp_type ppe) sigr.fs_ret;
 
-      if not testty then raise EqObsInError;
       let eq_params =
         ts_inv_eqparams
           sigl.fs_arg sigl.fs_anames ml