Name collisions between STM and user-provided code

[shym]

Currently there is no protection against collisions between the namespaces of STM and of the user-provided code.

Here is a simple example, renaming the base type in ref.ml from t to ty, to match the base type in STM.

diff --git i/plugins/qcheck-stm/test/ref.ml w/plugins/qcheck-stm/test/ref.ml
index a105d98..c67cd35 100644
--- i/plugins/qcheck-stm/test/ref.ml
+++ w/plugins/qcheck-stm/test/ref.ml
@@ -1,4 +1,4 @@
-type t = int ref
+type ty = int ref

 let make = ref
 let get r = !r
diff --git i/plugins/qcheck-stm/test/ref.mli w/plugins/qcheck-stm/test/ref.mli
index 2cd26e7..9f37a5f 100644
--- i/plugins/qcheck-stm/test/ref.mli
+++ w/plugins/qcheck-stm/test/ref.mli
@@ -1,11 +1,11 @@
-type t = private int ref
+type ty = private int ref
 (*@ mutable model value : integer *)

-val make : int -> t
+val make : int -> ty
 (*@ r = make i
     ensures r.value = i *)

-val get : t -> int
+val get : ty -> int
 (*@ i = get r
     pure
     ensures i = r.value

The generated code fails to compile with the following error:

File "plugins/qcheck-stm/test/ref_stm_tests.ml", line 9, characters 15-17:
9 |     type sut = ty
                   ^^
Error: The type constructor ty expects 1 argument(s),
       but is here applied to 0 argument(s)