Distinguish SUT-type unification errors

Unification of the SUT type is used in two different contexts:
- when handling a value, to know if its SUT-type argument has a
  compatible type with the one currently configured;
- when handling the declaration of the SUT type itself.
In the first case, we just want to skip the value with a warning; in the
second case, we need to error out

Consequently:
- Add a new kind of error
- Feed `unify` with the information to know in which case we are

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -35,15 +35,20 @@ let is_a_function ty =
   let open Ppxlib in
   match ty.ptyp_desc with Ptyp_arrow (_, _, _) -> true | _ -> false
 
-let unify value_name sut_ty ty =
+let unify case sut_ty ty =
   let open Ppxlib in
   let open Reserr in
-  let show_type = Fmt.to_to_string Pprintast.core_type in
+  let fail () =
+    let sut_ty = Fmt.to_to_string Pprintast.core_type sut_ty in
+    match case with
+    | `Value name -> error (Incompatible_type (name, sut_ty), ty.ptyp_loc)
+    | `Type ty -> error (Incompatible_sut sut_ty, ty.td_loc)
+  in
   let add_if_needed a x i =
     match List.assoc_opt a i with
     | None -> ok ((a, x) :: i)
     | Some y when x.ptyp_desc = y.ptyp_desc -> ok i
-    | _ -> error (Incompatible_type (value_name, show_type sut_ty), ty.ptyp_loc)
+    | _ -> fail ()
   in
   let rec aux i = function
     | [], [] -> ok i
@@ -55,13 +60,10 @@ let unify value_name sut_ty ty =
           | Ptyp_tuple xs, Ptyp_tuple ys -> aux i (xs, ys)
           | Ptyp_constr (c, xs), Ptyp_constr (d, ys) when c.txt = d.txt ->
               aux i (xs, ys)
-          | _ ->
-              error
-                (Incompatible_type (value_name, show_type sut_ty), ty.ptyp_loc)
+          | _ -> fail ()
         in
         aux i (xs, ys)
-    | _, _ ->
-        error (Incompatible_type (value_name, show_type sut_ty), ty.ptyp_loc)
+    | _, _ -> fail ()
   in
   match (sut_ty.ptyp_desc, ty.ptyp_desc) with
   | Ptyp_constr (t, args_sut), Ptyp_constr (t', args_ty) when t.txt = t'.txt ->
@@ -84,7 +86,7 @@ let ty_var_substitution config (vd : val_description) =
           match seen with
           | None ->
               let open Reserr in
-              let* x = unify value_name config.sut_core_type l in
+              let* x = unify (`Value value_name) config.sut_core_type l in
               aux (Some x) r
           | Some _ ->
               Reserr.(
@@ -238,8 +240,9 @@ let state config sigs =
   let* subst =
     Fun.flip List.assoc_opt
     <$> (Ocaml_of_gospel.core_type_of_tysymbol ty.td_ts
-        |> unify sut_name config.sut_core_type)
-  and* spec =
+        |> unify (`Type ty) config.sut_core_type)
+  in
+  let* spec =
     match ty.td_spec with
     | None -> error (Sut_type_not_specified sut_name, ty.td_loc)
     | Some spec -> ok spec

plugins/qcheck-stm/src/reserr.ml

@@ -32,6 +32,7 @@ type W.kind +=
   | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
   | Ghost_values of (string * [ `Arg | `Ret ])
+  | Incompatible_sut of string
 
 let level kind =
   match kind with
@@ -45,7 +46,7 @@ let level kind =
   | Sut_type_not_supported _ | Type_not_supported_for_sut_parameter _
   | Syntax_error_in_init_sut _ | Type_parameter_not_instantiated _
   | Sut_type_not_specified _ | No_models _ | Impossible_init_state_generation _
-    ->
+  | Incompatible_sut _ ->
       W.Error
   | _ -> W.level kind
 
@@ -195,6 +196,11 @@ let pp_kind ppf kind =
       pf ppf "Error in INIT expression %s:@ %a" fct text
         "mismatch in the number of arguments between the INIT expression and \
          the function specification"
+  | Incompatible_sut t ->
+      pf ppf "Incompatible declaration of SUT type:@ %a%s" text
+        "the declaration of the SUT type is incompatible with the configured \
+         one: "
+        t
   | _ -> W.pp_kind ppf kind
 
 let pp_errors = W.pp_param pp_kind level |> Fmt.list

plugins/qcheck-stm/src/reserr.mli

@@ -32,6 +32,7 @@ type W.kind +=
   | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
   | Ghost_values of (string * [ `Arg | `Ret ])
+  | Incompatible_sut of string
 
 type 'a reserr
 

plugins/qcheck-stm/test/test_errors.t

@@ -35,6 +35,15 @@ We can give a type that does not exist in the module as the system under test:
   $ ortac qcheck-stm foo.mli "()" "ty"
   Error: Type ty not declared in the module.
 
+Or forget its argument:
+
+  $ ortac qcheck-stm foo.mli "()" "t"
+  File "foo.mli", line 1, characters 0-9:
+  1 | type 'a t
+      ^^^^^^^^^
+  Error: Incompatible declaration of SUT type: the declaration of the SUT type
+         is incompatible with the configured one: t.
+
 We can forget to instantiate the type parameter of the system under test:
 
   $ cat > foo.mli << EOF