Pmodule: better error reporting on type mismatch during cloning

src/core/theory.ml

@@ -678,7 +678,7 @@ type bad_instance =
   | BadI_ls_arity of lsymbol (* lsymbol arity mismatch *)
   | BadI_ls_rs of lsymbol (* "val function" -> "function" *)
   | BadI_rs_arity of ident (* incompatible rsymbol arity *)
-  | BadI_rs_type of ident (* rsymbol type mismatch *)
+  | BadI_rs_type of ident * exn (* rsymbol type mismatch *)
   | BadI_rs_kind of ident (* incompatible rsymbol kind *)
   | BadI_rs_ghost of ident (* incompatible ghost status *)
   | BadI_rs_mask of ident (* incompatible result mask *)
@@ -1101,10 +1101,10 @@ let () = Exn_printer.register
       "Illegal instantiation for program function %a:@\n\
         arity mismatch"
         print_id id
-  | BadInstance (BadI_rs_type id) -> Format.fprintf fmt
+  | BadInstance (BadI_rs_type (id,exn)) -> Format.fprintf fmt
       "Illegal instantiation for program function %a:@\n\
-        type mismatch"
-        print_id id
+        %a"
+        print_id id Exn_printer.exn_printer exn
   | BadInstance (BadI_rs_kind id) -> Format.fprintf fmt
       "Illegal instantiation for program function %a:@\n\
         incompatible kind"

src/core/theory.mli

@@ -256,7 +256,7 @@ type bad_instance =
   | BadI_ls_arity of lsymbol (* lsymbol arity mismatch *)
   | BadI_ls_rs of lsymbol (* "val function" -> "function" *)
   | BadI_rs_arity of ident (* incompatible rsymbol arity *)
-  | BadI_rs_type of ident (* rsymbol type mismatch *)
+  | BadI_rs_type of ident * exn (* rsymbol type mismatch *)
   | BadI_rs_kind of ident (* incompatible rsymbol kind *)
   | BadI_rs_ghost of ident (* incompatible ghost status *)
   | BadI_rs_mask of ident (* incompatible result mask *)

src/mlw/pmodule.ml

@@ -1152,7 +1152,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with
       if List.length cty.cty_args <> List.length rs'.rs_cty.cty_args then
         raise (BadInstance (BadI_rs_arity rs.rs_name));
       let e = try e_exec (c_app rs' cty.cty_args [] cty.cty_result) with
-        | TypeMismatch _ -> raise (BadInstance (BadI_rs_type rs.rs_name)) in
+        | exn -> raise (BadInstance (BadI_rs_type (rs.rs_name, exn))) in
       let cexp = c_fun ~mask:cty.cty_mask cty.cty_args cty.cty_pre
         cty.cty_post cty.cty_xpost cty.cty_oldies e in
       let id = id_derive (rs.rs_name.id_string ^ "'refn") rs.rs_name in