From af8c3dbe2d0a14b5b0c3a5c653d6ccbafe4f7d34 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 12:54:05 +0100
Subject: [PATCH 01/15] Add test

---
 test/test__magic3.ml  | 15 +++++++++++++++
 test/test__magic3.mli |  0
 2 files changed, 15 insertions(+)
 create mode 100644 test/test__magic3.ml
 create mode 100644 test/test__magic3.mli

diff --git a/test/test__magic3.ml b/test/test__magic3.ml
new file mode 100644
index 0000000..0bb8195
--- /dev/null
+++ b/test/test__magic3.ml
@@ -0,0 +1,15 @@
+(* This test monitors an example that causes the current version of the library
+   to segfault. We keep it as regression test. *)
+
+type ('a, 'impl, 'tag) Provider.Trait.t += Trait : (unit, 'a, [ `A ]) Provider.Trait.t
+
+let a = (Trait : (unit, string, [ `A ]) Provider.Trait.t)
+let h = Provider.Handler.make [ Provider.Trait.implement a ~impl:"hello" ]
+let b = (Trait : (unit, int, [ `A ]) Provider.Trait.t)
+
+let%expect_test "crash" =
+  let (i : int) = Provider.Handler.lookup h ~trait:b in
+  print_s [%sexp { is_int = (Stdlib.Obj.is_int (Stdlib.Obj.repr i) : bool) }];
+  [%expect {| ((is_int false)) |}];
+  ()
+;;
diff --git a/test/test__magic3.mli b/test/test__magic3.mli
new file mode 100644
index 0000000..e69de29

From bba33d6869674226a2cbad753a86c72cbb4a500a Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 12:17:56 +0100
Subject: [PATCH 02/15] Monitor magic tests as mdx

In particular this allows to show that with the changes to make the
library Type-Safe, the definition of such trait is no longer possible
by design.

This is possible to show using mdx files since we can capture type
errors in expect traces, whereas in the test/ we simply have to delete
these tests.
---
 test/mdx/dune            |  6 ++++
 test/mdx/prelude.txt     |  2 ++
 test/mdx/test__magic.md  | 76 +++++++++++++++++++++++++++++++++++++++
 test/mdx/test__magic2.md | 78 ++++++++++++++++++++++++++++++++++++++++
 test/mdx/test__magic3.md | 25 +++++++++++++
 5 files changed, 187 insertions(+)
 create mode 100644 test/mdx/dune
 create mode 100644 test/mdx/prelude.txt
 create mode 100644 test/mdx/test__magic.md
 create mode 100644 test/mdx/test__magic2.md
 create mode 100644 test/mdx/test__magic3.md

diff --git a/test/mdx/dune b/test/mdx/dune
new file mode 100644
index 0000000..f8ff2f5
--- /dev/null
+++ b/test/mdx/dune
@@ -0,0 +1,6 @@
+(mdx
+ (package provider-dev)
+ (deps
+  (package provider)
+  (package provider-tests))
+ (preludes prelude.txt))
diff --git a/test/mdx/prelude.txt b/test/mdx/prelude.txt
new file mode 100644
index 0000000..a2d68af
--- /dev/null
+++ b/test/mdx/prelude.txt
@@ -0,0 +1,2 @@
+#require "base";;
+#require "provider";;
diff --git a/test/mdx/test__magic.md b/test/mdx/test__magic.md
new file mode 100644
index 0000000..8e360f0
--- /dev/null
+++ b/test/mdx/test__magic.md
@@ -0,0 +1,76 @@
+# Test magic
+
+This test monitors an example that caused an earlier version of the library to segfault. We keep it as regression test.
+
+This test was originally contributed by @v-gb.
+
+At its heart, it was based on the fact that you could add arguments to the trait constructors. Now, it is no longer possible by design, so the issues associated with this test are no longer applicable.
+
+```ocaml
+module type S = sig
+  type t
+
+  val t : t
+end
+
+type (_, _, _) Provider.Trait.t +=
+  | A :
+      'something Base.Type_equal.Id.t
+      -> (_, (module S with type t = 'something), [> `A ]) Provider.Trait.t
+```
+
+## For reference
+
+We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
+
+<!-- $MDX skip -->
+```ocaml
+
+let id_int = Type_equal.Id.create ~name:"int" [%sexp_of: int]
+let id_string = Type_equal.Id.create ~name:"string" [%sexp_of: string]
+let () = Provider.Trait.Info.register_name (A id_int) ~name:"A"
+
+let impl (type a) id value ~check_trait =
+  Provider.Private.Trait.implement_unsafe
+    (A id)
+    ~impl:
+      (module struct
+        type t = a
+
+        let t = value
+      end)
+    ~check_trait
+;;
+
+let%expect_test "magic" =
+  let make_handler ~check_trait =
+    Provider.Handler.make
+      [ (if true
+         then impl id_int 1 ~check_trait
+         else impl id_string "" ~check_trait [@coverage off])
+      ]
+  in
+  require_does_raise [%here] (fun () -> make_handler ~check_trait:true);
+  [%expect
+    {|
+    ("Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for this library"
+     ((
+       trait (
+         (id   #id)
+         (name A)))))
+    |}];
+  let handler = make_handler ~check_trait:false in
+  require_does_raise [%here] (fun () ->
+    (let module M = (val Provider.Handler.lookup handler ~trait:(A id_string)) in
+    print_string M.t) [@coverage off]);
+  [%expect
+    {|
+    ("Invalid usage of [Provider.Trait]: Extensible variants with the same id are expected to be physically equal through the use of this library"
+     ((
+       trait (
+         (id   #id)
+         (name A)))))
+    |}];
+  ()
+;;
+```
diff --git a/test/mdx/test__magic2.md b/test/mdx/test__magic2.md
new file mode 100644
index 0000000..891c2a0
--- /dev/null
+++ b/test/mdx/test__magic2.md
@@ -0,0 +1,78 @@
+# Test magic 2
+
+This is a variation of `./test__magic.md` without type ids.
+
+At its heart, it was based on the fact that you could add arguments to the trait constructors. Now, it is no longer possible by design, so the issues associated with this test are no longer applicable.
+
+```ocaml
+module type S = sig
+  type t
+
+  val t : t
+end
+
+type (_, _, _) Provider.Trait.t +=
+  | A :
+      'something Base.Type_equal.Id.t
+      -> (_, (module S with type t = 'something), [> `A ]) Provider.Trait.t
+```
+
+## For reference
+
+We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
+
+<!-- $MDX skip -->
+```ocaml
+
+module type S = sig
+  type t
+
+  val t : t
+end
+
+type (_, _, _) Provider.Trait.t +=
+  | A : 'a -> (_, (module S with type t = 'a), [> `A ]) Provider.Trait.t
+
+let () = Provider.Trait.Info.register_name (A ()) ~name:"A"
+
+let impl (type a) arg ~check_trait =
+  Provider.Private.Trait.implement_unsafe
+    (A arg)
+    ~impl:
+      (module struct
+        type t = a
+
+        let t = arg
+      end)
+    ~check_trait
+;;
+
+let%expect_test "magic" =
+  let make_handler ~check_trait =
+    Provider.Handler.make
+      [ (if true then impl 1 ~check_trait else impl "" ~check_trait [@coverage off]) ]
+  in
+  require_does_raise [%here] (fun () -> make_handler ~check_trait:true);
+  [%expect
+    {|
+    ("Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for this library"
+     ((
+       trait (
+         (id   #id)
+         (name A)))))
+    |}];
+  let handler = make_handler ~check_trait:false in
+  require_does_raise [%here] (fun () ->
+    (let module M = (val Provider.Handler.lookup handler ~trait:(A "0")) in
+    print_string M.t) [@coverage off]);
+  [%expect
+    {|
+    ("Invalid usage of [Provider.Trait]: Extensible variants with the same id are expected to be physically equal through the use of this library"
+     ((
+       trait (
+         (id   #id)
+         (name A)))))
+    |}];
+  ()
+;;
+```
diff --git a/test/mdx/test__magic3.md b/test/mdx/test__magic3.md
new file mode 100644
index 0000000..2a1510e
--- /dev/null
+++ b/test/mdx/test__magic3.md
@@ -0,0 +1,25 @@
+# Test magic
+
+This test monitors an example that caused an earlier version of the library to segfault. We keep it as regression test.
+
+```ocaml
+type ('a, 'impl, 'tag) Provider.Trait.t += Trait : (unit, 'a, [ `A ]) Provider.Trait.t
+```
+
+## For reference
+
+We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
+
+<!-- $MDX skip -->
+```ocaml
+let a = (Trait : (unit, string, [ `A ]) Provider.Trait.t)
+let h = Provider.Handler.make [ Provider.Trait.implement a ~impl:"hello" ]
+let b = (Trait : (unit, int, [ `A ]) Provider.Trait.t)
+
+let%expect_test "crash" =
+  let (i : int) = Provider.Handler.lookup h ~trait:b in
+  print_s [%sexp { is_int = (Stdlib.Obj.is_int (Stdlib.Obj.repr i) : bool) }];
+  [%expect {| ((is_int false)) |}];
+  ()
+;;
+```

From 94d576beb0f008d00bb1cb9aabd0210ff11521ff Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 11:58:34 +0100
Subject: [PATCH 03/15] Delete magic tests

---
 test/test__magic.ml   | 63 -------------------------------------------
 test/test__magic.mli  |  0
 test/test__magic2.ml  | 53 ------------------------------------
 test/test__magic2.mli |  0
 test/test__magic3.ml  | 15 -----------
 test/test__magic3.mli |  0
 6 files changed, 131 deletions(-)
 delete mode 100644 test/test__magic.ml
 delete mode 100644 test/test__magic.mli
 delete mode 100644 test/test__magic2.ml
 delete mode 100644 test/test__magic2.mli
 delete mode 100644 test/test__magic3.ml
 delete mode 100644 test/test__magic3.mli

diff --git a/test/test__magic.ml b/test/test__magic.ml
deleted file mode 100644
index 28c0f1a..0000000
--- a/test/test__magic.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(* This test monitors an example that caused an earlier version of the library
-   to segfault. We keep it as regression test.
-
-   This test was contributed by @v-gb. *)
-
-module type S = sig
-  type t
-
-  val t : t
-end
-
-type (_, _, _) Provider.Trait.t +=
-  | A :
-      'something Base.Type_equal.Id.t
-      -> (_, (module S with type t = 'something), [> `A ]) Provider.Trait.t
-
-let id_int = Type_equal.Id.create ~name:"int" [%sexp_of: int]
-let id_string = Type_equal.Id.create ~name:"string" [%sexp_of: string]
-let () = Provider.Trait.Info.register_name (A id_int) ~name:"A"
-
-let impl (type a) id value ~check_trait =
-  Provider.Private.Trait.implement_unsafe
-    (A id)
-    ~impl:
-      (module struct
-        type t = a
-
-        let t = value
-      end)
-    ~check_trait
-;;
-
-let%expect_test "magic" =
-  let make_handler ~check_trait =
-    Provider.Handler.make
-      [ (if true
-         then impl id_int 1 ~check_trait
-         else impl id_string "" ~check_trait [@coverage off])
-      ]
-  in
-  require_does_raise [%here] (fun () -> make_handler ~check_trait:true);
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for this library"
-     ((
-       trait (
-         (id   #id)
-         (name A)))))
-    |}];
-  let handler = make_handler ~check_trait:false in
-  require_does_raise [%here] (fun () ->
-    (let module M = (val Provider.Handler.lookup handler ~trait:(A id_string)) in
-    print_string M.t) [@coverage off]);
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: Extensible variants with the same id are expected to be physically equal through the use of this library"
-     ((
-       trait (
-         (id   #id)
-         (name A)))))
-    |}];
-  ()
-;;
diff --git a/test/test__magic.mli b/test/test__magic.mli
deleted file mode 100644
index e69de29..0000000
diff --git a/test/test__magic2.ml b/test/test__magic2.ml
deleted file mode 100644
index 1973bce..0000000
--- a/test/test__magic2.ml
+++ /dev/null
@@ -1,53 +0,0 @@
-(* This is a variation of [test__magic.ml] without type ids. *)
-
-module type S = sig
-  type t
-
-  val t : t
-end
-
-type (_, _, _) Provider.Trait.t +=
-  | A : 'a -> (_, (module S with type t = 'a), [> `A ]) Provider.Trait.t
-
-let () = Provider.Trait.Info.register_name (A ()) ~name:"A"
-
-let impl (type a) arg ~check_trait =
-  Provider.Private.Trait.implement_unsafe
-    (A arg)
-    ~impl:
-      (module struct
-        type t = a
-
-        let t = arg
-      end)
-    ~check_trait
-;;
-
-let%expect_test "magic" =
-  let make_handler ~check_trait =
-    Provider.Handler.make
-      [ (if true then impl 1 ~check_trait else impl "" ~check_trait [@coverage off]) ]
-  in
-  require_does_raise [%here] (fun () -> make_handler ~check_trait:true);
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for this library"
-     ((
-       trait (
-         (id   #id)
-         (name A)))))
-    |}];
-  let handler = make_handler ~check_trait:false in
-  require_does_raise [%here] (fun () ->
-    (let module M = (val Provider.Handler.lookup handler ~trait:(A "0")) in
-    print_string M.t) [@coverage off]);
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: Extensible variants with the same id are expected to be physically equal through the use of this library"
-     ((
-       trait (
-         (id   #id)
-         (name A)))))
-    |}];
-  ()
-;;
diff --git a/test/test__magic2.mli b/test/test__magic2.mli
deleted file mode 100644
index e69de29..0000000
diff --git a/test/test__magic3.ml b/test/test__magic3.ml
deleted file mode 100644
index 0bb8195..0000000
--- a/test/test__magic3.ml
+++ /dev/null
@@ -1,15 +0,0 @@
-(* This test monitors an example that causes the current version of the library
-   to segfault. We keep it as regression test. *)
-
-type ('a, 'impl, 'tag) Provider.Trait.t += Trait : (unit, 'a, [ `A ]) Provider.Trait.t
-
-let a = (Trait : (unit, string, [ `A ]) Provider.Trait.t)
-let h = Provider.Handler.make [ Provider.Trait.implement a ~impl:"hello" ]
-let b = (Trait : (unit, int, [ `A ]) Provider.Trait.t)
-
-let%expect_test "crash" =
-  let (i : int) = Provider.Handler.lookup h ~trait:b in
-  print_s [%sexp { is_int = (Stdlib.Obj.is_int (Stdlib.Obj.repr i) : bool) }];
-  [%expect {| ((is_int false)) |}];
-  ()
-;;
diff --git a/test/test__magic3.mli b/test/test__magic3.mli
deleted file mode 100644
index e69de29..0000000

From 37dce6011d9d8220ea1ceb8c0a31ac4a5913d210 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 16:07:52 +0100
Subject: [PATCH 04/15] Add custom Type equal type

---
 src/type_eq_opt.ml  |  3 +++
 src/type_eq_opt.mli | 14 ++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 src/type_eq_opt.ml
 create mode 100644 src/type_eq_opt.mli

diff --git a/src/type_eq_opt.ml b/src/type_eq_opt.ml
new file mode 100644
index 0000000..335400b
--- /dev/null
+++ b/src/type_eq_opt.ml
@@ -0,0 +1,3 @@
+type (_, _) t =
+  | Equal : ('a, 'a) t
+  | Not_equal : ('a, 'b) t
diff --git a/src/type_eq_opt.mli b/src/type_eq_opt.mli
new file mode 100644
index 0000000..6e79889
--- /dev/null
+++ b/src/type_eq_opt.mli
@@ -0,0 +1,14 @@
+(** A simplified type for [_ Type.eq option].
+
+    Using the option variation can sometimes result in the option being
+    optimized by the compiler (such as being pre-allocated, or code being
+    inlined), which is desirable. However, we prefer this type because it
+    eliminates the need to consider the conditions under which such
+    optimizations are guaranteed.
+
+    This module is intended for internal use within the library and is not
+    designed to be a general-purpose module. *)
+
+type (_, _) t =
+  | Equal : ('a, 'a) t
+  | Not_equal : ('a, 'b) t

From 21ef87253918ce80b0c78f3f93d19be84009f5c1 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 16:08:10 +0100
Subject: [PATCH 05/15] Redesign the library to make it Type-Safe

- This is joint work with @v-gb
---
 doc/docs/reference/hello_world.md             |   9 +-
 doc/docs/tutorials/getting-started/README.md  |   9 +-
 doc/docs/tutorials/handler-explicit/README.md |  59 ++---
 src/provider.ml                               |  55 +----
 src/provider.mli                              |  48 ++--
 src/trait0.ml                                 |  70 +++++-
 src/trait0.mli                                |  34 ++-
 test/mdx/test__magic.md                       |   4 +
 test/mdx/test__magic2.md                      |   4 +
 test/mdx/test__magic3.md                      |   4 +
 test/test__extensible_variant.ml              | 213 +-----------------
 test/test__higher_kinded.ml                   |  16 +-
 test/test__info.ml                            |   9 +-
 test/test__lookup.ml                          |  51 +----
 test/test_interfaces/directory_reader.ml      |   9 +-
 test/test_interfaces/file_reader.ml           |   9 +-
 test/test_interfaces/float_printer.ml         |   9 +-
 test/test_interfaces/int_printer.ml           |   9 +-
 18 files changed, 211 insertions(+), 410 deletions(-)

diff --git a/doc/docs/reference/hello_world.md b/doc/docs/reference/hello_world.md
index 2fbd403..f3e31d3 100644
--- a/doc/docs/reference/hello_world.md
+++ b/doc/docs/reference/hello_world.md
@@ -13,12 +13,9 @@ type show = [ `Show ]
 
 module Show : sig
   val t : ('t, (module S with type t = 't), [> show ]) Provider.Trait.t
-end  = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Show : ('t, (module S with type t = 't), [> show ]) Provider.Trait.t
-
-  let t = Show
-end
+end = Provider.Trait.Create (struct
+  type 'a module_type = (module S with type t = 'a)
+end)
 
 let print (Provider.T { t; handler }) =
   let module M = (val Provider.Handler.lookup handler ~trait:Show.t) in
diff --git a/doc/docs/tutorials/getting-started/README.md b/doc/docs/tutorials/getting-started/README.md
index 757362b..3a3457c 100644
--- a/doc/docs/tutorials/getting-started/README.md
+++ b/doc/docs/tutorials/getting-started/README.md
@@ -128,12 +128,9 @@ type reader = [ `Reader ]
 
 module Reader : sig
   val t : ('t, (module READER with type t = 't), [> reader ]) Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    Reader : ('t, (module READER with type t = 't), [> reader ]) Provider.Trait.t
-
-  let t = Reader
-end
+end = Provider.Trait.Create (struct
+  type 't module_type =  (module READER with type t = 't)
+end)
 ```
 
 ### Parametrized Library
diff --git a/doc/docs/tutorials/handler-explicit/README.md b/doc/docs/tutorials/handler-explicit/README.md
index 4328923..cae5e02 100644
--- a/doc/docs/tutorials/handler-explicit/README.md
+++ b/doc/docs/tutorials/handler-explicit/README.md
@@ -24,12 +24,9 @@ type id = [ `Id ]
 
 module Id : sig
   val t : ('a, (module Id with type t = 'a), [> id]) Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Id : ('a, (module Id with type t = 'a), [> id]) Provider.Trait.t
-
-  let t = Id
-end
+end = Provider.Trait.Create (struct
+  type 'a module_type = (module Id with type t = 'a)
+end)
 
 let id : type a. (a, [> id]) Provider.Handler.t -> a -> a =
   fun handler x ->
@@ -67,13 +64,9 @@ type doublable = [ `Doublable ]
 
 module Doublable : sig
   val t : ('a, (module Doublable with type t = 'a), [> doublable ]) Provider.Trait.t
-end = struct
-
-  type (_, _, _) Provider.Trait.t +=
-    | Doublable : ('a, (module Doublable with type t = 'a), [> doublable ]) Provider.Trait.t
-
-  let t = Doublable
-end
+end = Provider.Trait.Create (struct
+  type 'a module_type = (module Doublable with type t = 'a)
+end)
 ```
 
 ### Writing Parametrized Code
@@ -152,12 +145,9 @@ type repeatable = [ `Repeatable ]
 
 module Repeatable : sig
   val t : ('a, (module Repeatable with type t = 'a), [> repeatable ]) Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Repeatable : ('a, (module Repeatable with type t = 'a), [> repeatable ]) Provider.Trait.t
-
-  let t = Repeatable
-end
+end = Provider.Trait.Create (struct
+  type 'a module_type = (module Repeatable with type t = 'a)
+end)
 ```
 
 ### Writing Parametrized Code
@@ -268,12 +258,9 @@ Note, you cannot write this (the `'a 't` syntax doesn't mean anything):
 ```ocaml
 module Mappable : sig
   val t : ('a 't, (module Mappable with type 'a t = 'a 't), [> mappable ]) Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Mappable : ('a 't, (module Mappable with type 'a t = 'a 't), [> mappable ]) Provider.Trait.t
-
-  let t = Mappable
-end
+end = Provider.Trait.Create (struct
+  type 'a 't module_type =  (module Mappable with type 'a t = 'a 't)
+end)
 ```
 ```mdx-error
 Line 2, characters 17-18:
@@ -285,20 +272,14 @@ This is where `Higher_kinded` comes to the rescue:
 ```ocaml
 module Mappable : sig
   val t :
-       ( ('a -> 'higher_kinded) Higher_kinded.t
-          , (module Mappable with type higher_kinded = 'higher_kinded)
-          , [> mappable ] )
-          Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Mappable :
-        ( ('a -> 'higher_kinded) Higher_kinded.t
-          , (module Mappable with type higher_kinded = 'higher_kinded)
-          , [> mappable ] )
-          Provider.Trait.t
-
-  let t = Mappable
-end
+      ( ('a -> 'higher_kinded) Higher_kinded.t
+        , (module Mappable with type higher_kinded = 'higher_kinded)
+        , [> mappable ] )
+        Provider.Trait.t
+end = Provider.Trait.Create2 (struct
+  type (!'a, !'higher_kinded) t = ('a -> 'higher_kinded) Higher_kinded.t
+  type ('a, 'higher_kinded) module_type = (module Mappable with type higher_kinded = 'higher_kinded)
+end)
 ```
 
 ### Writing Parametrized Code
diff --git a/src/provider.ml b/src/provider.ml
index dec4058..b59a045 100644
--- a/src/provider.ml
+++ b/src/provider.ml
@@ -12,7 +12,12 @@ let raise_s msg sexp = raise (E (Sexp.List [ Atom msg; sexp ]))
 let phys_same t1 t2 = phys_equal (Obj.repr t1) (Obj.repr t2)
 
 module Trait = struct
-  type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t = ..
+  type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t
+
+  module Create = Trait0.Create
+  module Create0 = Trait0.Create0
+  module Create1 = Trait0.Create1
+  module Create2 = Trait0.Create2
 
   let runtime_trait_info = Runtime_trait_info.default
 
@@ -55,41 +60,7 @@ module Trait = struct
   let uid (t : _ t) = Trait0.uid t
   let compare_by_uid id1 id2 = Uid.compare (uid id1) (uid id2)
   let same (id1 : _ t) (id2 : _ t) = phys_same id1 id2
-
-  let check_trait_exn (t : _ t) =
-    if not (Trait0.is_valid t)
-    then
-      raise_s
-        "Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for \
-         this library"
-        (Sexp.List [ List [ Atom "trait"; info t |> Info.sexp_of_t ] ])
-  ;;
-
-  let implement trait ~impl =
-    check_trait_exn trait;
-    Binding0.implement trait ~impl
-  ;;
-
-  module Unsafe_cast : sig
-    type (_, _) eq_opt =
-      | Equal : ('a, 'a) eq_opt
-      | Not_equal : ('a, 'b) eq_opt
-
-    (* We limit unsafe casting to cases where the first parameter is already
-       determined to be the same. *)
-    val same_witness : ('a, 'i1, _) t -> ('a, 'i2, _) t -> ('i1, 'i2) eq_opt
-  end = struct
-    type (_, _) eq_opt =
-      | Equal : ('a, 'a) eq_opt
-      | Not_equal : ('a, 'b) eq_opt
-
-    let same_witness : type a i1 i2. (a, i1, _) t -> (a, i2, _) t -> (i1, i2) eq_opt =
-      fun t1 t2 ->
-      if same t1 t2
-      then (Obj.magic (Obj.repr (Equal : _ eq_opt)) : (i1, i2) eq_opt)
-      else Not_equal
-    ;;
-  end
+  let implement = Binding0.implement
 end
 
 module Binding = struct
@@ -178,7 +149,7 @@ module Handler = struct
       | Greater ->
         binary_search t ~trait ~update_cache ~if_not_found ~if_found ~from ~to_:(mid - 1)
       | Equal ->
-        (match Trait.Unsafe_cast.same_witness elt trait with
+        (match Trait0.same_witness elt trait with
          | Equal ->
            if update_cache then t.(0) <- binding;
            if_found implementation
@@ -207,7 +178,7 @@ module Handler = struct
     then if_not_found ~trait_info:(Trait.info trait)
     else (
       let (Binding.T { trait = cached_id; implementation }) = t.(0) in
-      match Trait.Unsafe_cast.same_witness trait cached_id with
+      match Trait0.same_witness trait cached_id with
       | Equal -> if_found implementation
       | Not_equal ->
         binary_search
@@ -270,13 +241,5 @@ type -'tags t =
 
 module Private = struct
   module Import = Import
-
-  module Trait = struct
-    let implement_unsafe trait ~impl ~check_trait =
-      if check_trait then Trait.check_trait_exn trait;
-      Binding0.implement trait ~impl
-    ;;
-  end
-
   module Handler = Handler
 end
diff --git a/src/provider.mli b/src/provider.mli
index d9f7e73..ce5e65a 100644
--- a/src/provider.mli
+++ b/src/provider.mli
@@ -27,12 +27,37 @@ module Trait : sig
         phantom type designed to make {!val:Handler.lookup} more type-safe.
 
       ['module_type] is expected to be a module type (Eio supports single
-      functions but this is discouraged through the use of this library).
+      functions but this is discouraged through the use of this library). *)
+  type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t
 
-      Beware, traits constructors must be such that they are physically equal
-      when they have the same extension id. In particular they should have zero
-      arguments. *)
-  type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t = ..
+  (** {1 Creating traits} *)
+
+  module Create0 (X : sig
+      type t
+      type module_type
+    end) : sig
+    val t : (X.t, X.module_type, _) t
+  end
+
+  module Create (X : sig
+      type 'a module_type
+    end) : sig
+    val t : ('a, 'a X.module_type, _) t
+  end
+
+  module Create1 (X : sig
+      type !'a t
+      type 'a module_type
+    end) : sig
+    val t : ('a X.t, 'a X.module_type, _) t
+  end
+
+  module Create2 (X : sig
+      type (!'a, !'b) t
+      type ('a, 'b) module_type
+    end) : sig
+    val t : (('a, 'b) X.t, ('a, 'b) X.module_type, _) t
+  end
 
   (** {1 Dump & debug} *)
 
@@ -246,19 +271,6 @@ module Private : sig
     val dedup_sorted_keep_last : 'a list -> compare:('a -> 'a -> int) -> 'a list
   end
 
-  module Trait : sig
-    (** Some error cases of the implementation have been made non-reachable
-        thanks to additional checks run early. However, we'd like to cover
-        these cases in tests, thus this constructor is exposed to optionally
-        bypass the trait validation happening during [implement]. To be used
-        by tests only, do not use in user code. *)
-    val implement_unsafe
-      :  ('t, 'module_type, _) Trait.t
-      -> impl:'module_type
-      -> check_trait:bool
-      -> 't Binding.t
-  end
-
   module Import : sig
     (** Exported things from the import module we'd like to test separately. *)
 
diff --git a/src/trait0.ml b/src/trait0.ml
index affed6d..b37b83f 100644
--- a/src/trait0.ml
+++ b/src/trait0.ml
@@ -1,8 +1,68 @@
-type ('t, 'module_type, 'tag) t = ..
+type ('t, 'module_type) ext = ..
 
-let is_valid (t : _ t) =
-  let extension_constructor = Obj.Extension_constructor.of_val t in
-  Obj.repr t == Obj.repr extension_constructor
+type ('t, 'module_type, 'tag) t =
+  { ext : ('t, 'module_type) ext
+  ; same_witness : 'm2. ('t, 'm2) ext -> ('module_type, 'm2) Type_eq_opt.t
+  }
+
+let uid (t : _ t) = Obj.Extension_constructor.id (Obj.Extension_constructor.of_val t.ext)
+
+let same_witness : ('t, 'mt1, _) t -> ('t, 'mt2, _) t -> ('mt1, 'mt2) Type_eq_opt.t =
+  fun t1 t2 -> t1.same_witness t2.ext
 ;;
 
-let uid (t : _ t) = Obj.Extension_constructor.id (Obj.Extension_constructor.of_val t)
+module Create0 (X : sig
+    type t
+    type module_type
+  end) =
+struct
+  type (_, _) ext += T : (X.t, X.module_type) ext
+
+  let same_witness (type m2) t2 : (X.module_type, m2) Type_eq_opt.t =
+    match (t2 : (X.t, m2) ext) with
+    | T -> Type_eq_opt.Equal
+    | _ -> Not_equal
+  ;;
+
+  let t = { ext = T; same_witness }
+end
+
+module Create1 (X : sig
+    type !'a t
+    type 'a module_type
+  end) =
+struct
+  type (_, _) ext += T : ('a X.t, 'a X.module_type) ext
+
+  let same_witness (type a m2) t2 : (a X.module_type, m2) Type_eq_opt.t =
+    match (t2 : (a X.t, m2) ext) with
+    | T -> Type_eq_opt.Equal
+    | _ -> Not_equal
+  ;;
+
+  let t = { ext = T; same_witness }
+end
+
+module Create2 (X : sig
+    type (!'a, !'b) t
+    type ('a, 'b) module_type
+  end) =
+struct
+  type (_, _) ext += T : (('a, 'b) X.t, ('a, 'b) X.module_type) ext
+
+  let same_witness (type a b m2) t2 : ((a, b) X.module_type, m2) Type_eq_opt.t =
+    match (t2 : ((a, b) X.t, m2) ext) with
+    | T -> Type_eq_opt.Equal
+    | _ -> Not_equal
+  ;;
+
+  let t = { ext = T; same_witness }
+end
+
+module Create (X : sig
+    type 'a module_type
+  end) =
+Create1 (struct
+    type !'a t = 'a
+    type 'a module_type = 'a X.module_type
+  end)
diff --git a/src/trait0.mli b/src/trait0.mli
index 4468f0d..8683389 100644
--- a/src/trait0.mli
+++ b/src/trait0.mli
@@ -1,9 +1,33 @@
-type ('t, 'module_type, 'tag) t = ..
+type ('t, 'module_type, 'tag) t
 
-(** Through the use of this library, a tag is only valid if it has no arguments.
-    This function is used to check that, and used to validate traits built by
-    the user to detect invalid usage of the library. *)
-val is_valid : _ t -> bool
+module Create (X : sig
+    type 'a module_type
+  end) : sig
+  val t : ('a, 'a X.module_type, _) t
+end
+
+module Create0 (X : sig
+    type t
+    type module_type
+  end) : sig
+  val t : (X.t, X.module_type, _) t
+end
+
+module Create1 (X : sig
+    type !'a t
+    type 'a module_type
+  end) : sig
+  val t : ('a X.t, 'a X.module_type, _) t
+end
+
+module Create2 (X : sig
+    type (!'a, !'b) t
+    type ('a, 'b) module_type
+  end) : sig
+  val t : (('a, 'b) X.t, ('a, 'b) X.module_type, _) t
+end
 
 (** Return a id that is unique to this trait for the lifetime of the program. *)
 val uid : _ t -> int
+
+val same_witness : ('t, 'mt1, _) t -> ('t, 'mt2, _) t -> ('mt1, 'mt2) Type_eq_opt.t
diff --git a/test/mdx/test__magic.md b/test/mdx/test__magic.md
index 8e360f0..21e0488 100644
--- a/test/mdx/test__magic.md
+++ b/test/mdx/test__magic.md
@@ -18,6 +18,10 @@ type (_, _, _) Provider.Trait.t +=
       'something Base.Type_equal.Id.t
       -> (_, (module S with type t = 'something), [> `A ]) Provider.Trait.t
 ```
+```mdx-error
+Lines 7-10, characters 3-78:
+Error: Type definition Provider.Trait.t is not extensible
+```
 
 ## For reference
 
diff --git a/test/mdx/test__magic2.md b/test/mdx/test__magic2.md
index 891c2a0..638f775 100644
--- a/test/mdx/test__magic2.md
+++ b/test/mdx/test__magic2.md
@@ -16,6 +16,10 @@ type (_, _, _) Provider.Trait.t +=
       'something Base.Type_equal.Id.t
       -> (_, (module S with type t = 'something), [> `A ]) Provider.Trait.t
 ```
+```mdx-error
+Lines 7-10, characters 3-78:
+Error: Type definition Provider.Trait.t is not extensible
+```
 
 ## For reference
 
diff --git a/test/mdx/test__magic3.md b/test/mdx/test__magic3.md
index 2a1510e..964504f 100644
--- a/test/mdx/test__magic3.md
+++ b/test/mdx/test__magic3.md
@@ -5,6 +5,10 @@ This test monitors an example that caused an earlier version of the library to s
 ```ocaml
 type ('a, 'impl, 'tag) Provider.Trait.t += Trait : (unit, 'a, [ `A ]) Provider.Trait.t
 ```
+```mdx-error
+Line 1, characters 1-87:
+Error: Type definition Provider.Trait.t is not extensible
+```
 
 ## For reference
 
diff --git a/test/test__extensible_variant.ml b/test/test__extensible_variant.ml
index 36bf4dd..63dc839 100644
--- a/test/test__extensible_variant.ml
+++ b/test/test__extensible_variant.ml
@@ -39,21 +39,15 @@ let%expect_test "Eq_opt at runtime" =
 
 module No_arg_A : sig
   val t : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-end = struct
-  type ('t, 'module_type, 'tag) Provider.Trait.t +=
-    | No_arg_A : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-
-  let t = No_arg_A
-end
+end = Provider.Trait.Create (struct
+    type 'a module_type = (module T with type t = 'a)
+  end)
 
 module No_arg_B : sig
   val t : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-end = struct
-  type ('t, 'module_type, 'tag) Provider.Trait.t +=
-    | No_arg_B : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-
-  let t = No_arg_B
-end
+end = Provider.Trait.Create (struct
+    type 'a module_type = (module T with type t = 'a)
+  end)
 
 let () =
   Provider.Trait.Info.register_name No_arg_A.t ~name:"No_arg_A";
@@ -74,10 +68,10 @@ let%expect_test "extension_constructor" =
     |}];
   let extension_constructor_A = Obj.Extension_constructor.of_val No_arg_A.t in
   print_s [%sexp (Obj.Extension_constructor.name extension_constructor_A : string)];
-  [%expect {| Provider_test.Test__extensible_variant.No_arg_A.No_arg_A |}];
+  [%expect {| "Provider__Trait0.Create1(X).T" |}];
   let extension_constructor_B = Obj.Extension_constructor.of_val No_arg_B.t in
   print_s [%sexp (Obj.Extension_constructor.name extension_constructor_B : string)];
-  [%expect {| Provider_test.Test__extensible_variant.No_arg_B.No_arg_B |}];
+  [%expect {| "Provider__Trait0.Create1(X).T" |}];
   (* We do not print the actual runtime ids because it is too brittle. We simply
      characterize that they are different. *)
   let idA = Obj.Extension_constructor.id extension_constructor_A in
@@ -91,13 +85,12 @@ let%expect_test "implement" =
   (* This test covers a case where [implement_unsafe ~check_trait] succeeds. *)
   let handler =
     Provider.Handler.make
-      [ Provider.Private.Trait.implement_unsafe
+      [ Provider.Trait.implement
           No_arg_A.t
           ~impl:
             (module struct
               type t = int
             end)
-          ~check_trait:true
       ]
   in
   let module M = (val Provider.Handler.lookup handler ~trait:No_arg_A.t) in
@@ -121,191 +114,3 @@ let%expect_test "no_arg physical equality" =
   [%expect {||}];
   ()
 ;;
-
-module Name_override : sig
-  val t : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-end = struct
-  type ('t, 'module_type, 'tag) Provider.Trait.t +=
-    | No_arg_A : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-
-  let t = No_arg_A
-end
-
-let () = Provider.Trait.Info.register_name Name_override.t ~name:"No_arg_A"
-
-let%expect_test "name override" =
-  require [%here] (not (phys_equal No_arg_A.t Name_override.t));
-  [%expect {||}];
-  let extension_constructor_A = Obj.Extension_constructor.of_val No_arg_A.t in
-  let extension_constructor_A' = Obj.Extension_constructor.of_val Name_override.t in
-  require_not_equal
-    [%here]
-    (module Int)
-    (Obj.Extension_constructor.id extension_constructor_A)
-    (Obj.Extension_constructor.id extension_constructor_A');
-  [%expect {||}];
-  ()
-;;
-
-module With_arg = struct
-  type (_, _, _) extensible = ..
-
-  type ('t, 'module_type, 'tag) extensible +=
-    | A : { value : 'a } -> ('t, 't * 'a, [> `T ]) extensible
-    | B : { value : 'a } -> ('t, 'a * 't, [> `T ]) extensible
-end
-
-let%expect_test "extension_constructor" =
-  let extension_constructor_A =
-    Obj.Extension_constructor.of_val (With_arg.A { value = 0 })
-  in
-  print_s [%sexp (Obj.Extension_constructor.name extension_constructor_A : string)];
-  [%expect {| Provider_test.Test__extensible_variant.With_arg.A |}];
-  let extension_constructor_A' =
-    Obj.Extension_constructor.of_val (With_arg.A { value = "0" })
-  in
-  print_s [%sexp (Obj.Extension_constructor.name extension_constructor_A' : string)];
-  [%expect {| Provider_test.Test__extensible_variant.With_arg.A |}];
-  let extension_constructor_B =
-    Obj.Extension_constructor.of_val (With_arg.B { value = "0" })
-  in
-  print_s [%sexp (Obj.Extension_constructor.name extension_constructor_B : string)];
-  [%expect {| Provider_test.Test__extensible_variant.With_arg.B |}];
-  let idA = Obj.Extension_constructor.id extension_constructor_A in
-  let idA' = Obj.Extension_constructor.id extension_constructor_A' in
-  let idB = Obj.Extension_constructor.id extension_constructor_B in
-  require_equal [%here] (module Int) idA idA';
-  [%expect {||}];
-  require_not_equal [%here] (module Int) idA idB;
-  [%expect {||}];
-  ()
-;;
-
-let%expect_test "with_arg physical equality" =
-  require [%here] (not (phys_equal (With_arg.A { value = 0 }) (With_arg.A { value = 0 })));
-  [%expect {||}];
-  ()
-;;
-
-(* Because we currently allow Traits with arguments, we have effectively the
-   possibility for different traits to have the same id even though they are
-   physically different. *)
-
-module type S = sig
-  type t
-
-  val show : t -> string
-end
-
-type show = [ `Show ]
-
-type (_, _, _) Provider.Trait.t +=
-  | Show : { arg : int } -> ('t, (module S with type t = 't), [> show ]) Provider.Trait.t
-
-let () = Provider.Trait.Info.register_name (Show { arg = 0 }) ~name:"Show"
-
-let%expect_test "ids" =
-  let trait1 = Show { arg = 0 } in
-  let trait2 = Show { arg = 1 } in
-  require [%here] (not (phys_equal trait1 trait2));
-  [%expect {||}];
-  let idA = Provider.Trait.uid (Show { arg = 0 }) in
-  let idB = Provider.Trait.uid (Show { arg = 1 }) in
-  require_equal [%here] (module Provider.Trait.Uid) idA idB;
-  [%expect {||}];
-  ()
-;;
-
-let print (Provider.T { t; handler }) =
-  (let module M = (val Provider.Handler.lookup handler ~trait:(Show { arg = 0 })) in
-  print_endline (M.show t)) [@coverage off]
-;;
-
-let string_provider t ~check_trait =
-  let handler =
-    Provider.Handler.make
-      [ Provider.Private.Trait.implement_unsafe
-          (Show { arg = 0 })
-          ~impl:
-            (module struct
-              type t = string
-
-              let show = Fn.id
-            end)
-          ~check_trait
-      ]
-  in
-  Provider.T { t; handler }
-;;
-
-let%expect_test "invalid_trait" =
-  require_does_raise [%here] (fun () -> string_provider "Hello World" ~check_trait:true);
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: trait is not a valid extensible variant for this library"
-     ((
-       trait (
-         (id   #id)
-         (name Show)))))
-    |}];
-  require_does_raise [%here] (fun () ->
-    print (string_provider "Hello World" ~check_trait:false));
-  [%expect
-    {|
-    ("Invalid usage of [Provider.Trait]: Extensible variants with the same id are expected to be physically equal through the use of this library"
-     ((
-       trait (
-         (id   #id)
-         (name Show)))))
-    |}];
-  ()
-;;
-
-(* Note that the API may be changed in the future to avoid it by design. This is
-   left as future work. *)
-
-type ('t, 'module_type, 'tag) With_arg.extensible +=
-  | With_arg_C :
-      { a : 'a
-      ; b : 'b
-      }
-      -> ('t, 'a * 'b, [> `T ]) With_arg.extensible
-
-let%expect_test "with-arg detection" =
-  (* To detect the presence of argument, we can check whether the object is the
-     same as its extension constructor. *)
-  let test (repr : Obj.t) =
-    let is_block = Obj.is_block repr in
-    require [%here] is_block;
-    let size = Obj.size repr in
-    let extension_constructor = Obj.Extension_constructor.of_val repr in
-    let name = Obj.Extension_constructor.name extension_constructor in
-    let has_args = not (phys_equal repr (Obj.repr extension_constructor)) in
-    print_s [%sexp { name : string; is_block : bool; size : int; has_args : bool }]
-  in
-  test (Obj.repr No_arg_A.t);
-  [%expect
-    {|
-    ((name Provider_test.Test__extensible_variant.No_arg_A.No_arg_A)
-     (is_block true)
-     (size     2)
-     (has_args false))
-    |}];
-  test (Obj.repr (With_arg.A { value = 42 }));
-  [%expect
-    {|
-    ((name Provider_test.Test__extensible_variant.With_arg.A)
-     (is_block true)
-     (size     2)
-     (has_args true))
-    |}];
-  test (Obj.repr (With_arg_C { a = 0; b = "1" }));
-  [%expect
-    {|
-    ((name Provider_test.Test__extensible_variant.With_arg_C)
-     (is_block true)
-     (size     3)
-     (has_args true))
-    |}];
-  ()
-;;
diff --git a/test/test__higher_kinded.ml b/test/test__higher_kinded.ml
index 175d7c0..0f87a1f 100644
--- a/test/test__higher_kinded.ml
+++ b/test/test__higher_kinded.ml
@@ -28,16 +28,12 @@ module Mappable : sig
         , (module Mappable with type higher_kinded = 'higher_kinded)
         , [> mappable ] )
         Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | Mappable :
-        ( ('a -> 'higher_kinded) Higher_kinded.t
-          , (module Mappable with type higher_kinded = 'higher_kinded)
-          , [> mappable ] )
-          Provider.Trait.t
-
-  let t = Mappable
-end
+end = Provider.Trait.Create2 (struct
+    type (!'a, !'higher_kinded) t = ('a -> 'higher_kinded) Higher_kinded.t
+
+    type ('a, 'higher_kinded) module_type =
+      (module Mappable with type higher_kinded = 'higher_kinded)
+  end)
 
 let map_n_times
   : type a t.
diff --git a/test/test__info.ml b/test/test__info.ml
index 0c98e22..bda1712 100644
--- a/test/test__info.ml
+++ b/test/test__info.ml
@@ -1,11 +1,8 @@
 module T : sig
   val t : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-end = struct
-  type (_, _, _) Provider.Trait.t +=
-    | T : ('t, (module T with type t = 't), [> `T ]) Provider.Trait.t
-
-  let t = T
-end
+end = Provider.Trait.Create (struct
+    type 't module_type = (module T with type t = 't)
+  end)
 
 let%expect_test "info" =
   (* By default, id are not shown, and trait do not have names. *)
diff --git a/test/test__lookup.ml b/test/test__lookup.ml
index 3565a15..1c56ac6 100644
--- a/test/test__lookup.ml
+++ b/test/test__lookup.ml
@@ -34,47 +34,16 @@ end
 
 type 'a t = ([> Tag.t ] as 'a) Provider.t
 
-module A = struct
-  type (_, _, _) Provider.Trait.t +=
-    | A : ('a, (module S with type t = 'a), [> `A ]) Provider.Trait.t
-
-  let t = A
-end
-
-module B = struct
-  type (_, _, _) Provider.Trait.t +=
-    | B : ('a, (module S with type t = 'a), [> `B ]) Provider.Trait.t
-
-  let t = B
-end
-
-module C = struct
-  type (_, _, _) Provider.Trait.t +=
-    | C : ('a, (module S with type t = 'a), [> `C ]) Provider.Trait.t
-
-  let t = C
-end
-
-module D = struct
-  type (_, _, _) Provider.Trait.t +=
-    | D : ('a, (module S with type t = 'a), [> `D ]) Provider.Trait.t
-
-  let t = D
-end
-
-module E = struct
-  type (_, _, _) Provider.Trait.t +=
-    | E : ('a, (module S with type t = 'a), [> `E ]) Provider.Trait.t
-
-  let t = E
-end
-
-module F = struct
-  type (_, _, _) Provider.Trait.t +=
-    | F : ('a, (module S with type t = 'a), [> `F ]) Provider.Trait.t
-
-  let t = F
-end
+module C_all () = Provider.Trait.Create (struct
+    type 't module_type = (module S with type t = 't)
+  end)
+
+module A = C_all ()
+module B = C_all ()
+module C = C_all ()
+module D = C_all ()
+module E = C_all ()
+module F = C_all ()
 
 let a : (_, _, [> `A ]) Provider.Trait.t = A.t
 let b : (_, _, [> `B ]) Provider.Trait.t = B.t
diff --git a/test/test_interfaces/directory_reader.ml b/test/test_interfaces/directory_reader.ml
index abe0c92..356f8cc 100644
--- a/test/test_interfaces/directory_reader.ml
+++ b/test/test_interfaces/directory_reader.ml
@@ -8,12 +8,9 @@ module Provider_interface = struct
     val readdir : t -> path:string -> string list
   end
 
-  module Trait = struct
-    type (_, _, _) Provider.Trait.t +=
-      | Directory_reader : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t
-
-    let t = Directory_reader
-  end
+  module Trait = Provider.Trait.Create (struct
+      type 'a module_type = (module S with type t = 'a)
+    end)
 
   let directory_reader =
     (Trait.t : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t)
diff --git a/test/test_interfaces/file_reader.ml b/test/test_interfaces/file_reader.ml
index 73fed75..cd48c7b 100644
--- a/test/test_interfaces/file_reader.ml
+++ b/test/test_interfaces/file_reader.ml
@@ -8,12 +8,9 @@ module Provider_interface = struct
     val load : t -> path:string -> string
   end
 
-  module Trait = struct
-    type (_, _, _) Provider.Trait.t +=
-      | File_reader : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t
-
-    let t = File_reader
-  end
+  module Trait = Provider.Trait.Create (struct
+      type 'a module_type = (module S with type t = 'a)
+    end)
 
   let file_reader =
     (Trait.t : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t)
diff --git a/test/test_interfaces/float_printer.ml b/test/test_interfaces/float_printer.ml
index 97fc830..4e10960 100644
--- a/test/test_interfaces/float_printer.ml
+++ b/test/test_interfaces/float_printer.ml
@@ -8,12 +8,9 @@ module Provider_interface = struct
     val string_of_float : t -> float -> string
   end
 
-  module Trait = struct
-    type (_, _, _) Provider.Trait.t +=
-      | Float_printer : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t
-
-    let t = Float_printer
-  end
+  module Trait = Provider.Trait.Create (struct
+      type 'a module_type = (module S with type t = 'a)
+    end)
 
   let float_printer =
     (Trait.t : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t)
diff --git a/test/test_interfaces/int_printer.ml b/test/test_interfaces/int_printer.ml
index 7cf3ada..71b5b22 100644
--- a/test/test_interfaces/int_printer.ml
+++ b/test/test_interfaces/int_printer.ml
@@ -8,12 +8,9 @@ module Provider_interface = struct
     val string_of_int : t -> int -> string
   end
 
-  module Trait = struct
-    type (_, _, _) Provider.Trait.t +=
-      | Int_printer : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t
-
-    let t = Int_printer
-  end
+  module Trait = Provider.Trait.Create (struct
+      type 'a module_type = (module S with type t = 'a)
+    end)
 
   let int_printer =
     (Trait.t : ('t, (module S with type t = 't), [> tag ]) Provider.Trait.t)

From 6d9598acfa9912c76ce447f452e870010242442e Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 13:21:22 +0100
Subject: [PATCH 06/15] Say more about how the counter-examples are fixed

---
 test/mdx/test__magic.md  |   2 +
 test/mdx/test__magic2.md |   2 +
 test/mdx/test__magic3.md | 130 ++++++++++++++++++++++++++++++++++++++-
 3 files changed, 133 insertions(+), 1 deletion(-)

diff --git a/test/mdx/test__magic.md b/test/mdx/test__magic.md
index 21e0488..e50134c 100644
--- a/test/mdx/test__magic.md
+++ b/test/mdx/test__magic.md
@@ -23,6 +23,8 @@ Lines 7-10, characters 3-78:
 Error: Type definition Provider.Trait.t is not extensible
 ```
 
+Now that we have to go through the `Trait.Create` functors, there just isn't any way to build a trait with this extra argument.
+
 ## For reference
 
 We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
diff --git a/test/mdx/test__magic2.md b/test/mdx/test__magic2.md
index 638f775..680fe87 100644
--- a/test/mdx/test__magic2.md
+++ b/test/mdx/test__magic2.md
@@ -21,6 +21,8 @@ Lines 7-10, characters 3-78:
 Error: Type definition Provider.Trait.t is not extensible
 ```
 
+Now that we have to go through the `Trait.Create` functors, there just isn't any way to build a trait with this extra argument.
+
 ## For reference
 
 We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
diff --git a/test/mdx/test__magic3.md b/test/mdx/test__magic3.md
index 964504f..d696bf3 100644
--- a/test/mdx/test__magic3.md
+++ b/test/mdx/test__magic3.md
@@ -10,9 +10,137 @@ Line 1, characters 1-87:
 Error: Type definition Provider.Trait.t is not extensible
 ```
 
+## Trying through the Create functors
+
+The error above indicates that it is no longer possible to define the trait that way, because we no longer expose any extensible variant to extend. However, can a similar example be built through one of the functors? The short answer is No. Below are a few attempts.
+
+### Direct translation of the previous example
+
+This is rejected through injectivity check.
+
+```ocaml
+module Trait = Provider.Trait.Create1 (struct
+  type 'a t = unit
+  type 'a module_type = 'a
+end)
+```
+```mdx-error
+Lines 1-4, characters 16-7:
+Error: Modules do not match:
+       sig type 'a t = unit type 'a module_type = 'a end
+     is not included in sig type !'a t type 'a module_type end
+     Type declarations do not match:
+       type 'a t = unit
+     is not included in
+       type !'a t
+     Their variances do not agree.
+     File "src/provider.mli", line 49, characters 6-16: Expected declaration
+```
+
+Trying to force the injectivity won't do either.
+
+```ocaml
+module Trait = Provider.Trait.Create1 (struct
+  type !'a t = unit
+  type 'a module_type = 'a
+end)
+```
+```mdx-error
+Line 2, characters 5-22:
+Error: In this definition, expected parameter variances are not satisfied.
+       The 1st type parameter was expected to be injective invariant,
+       but it is unrestricted.
+```
+
+### Tweaking the original example somehow
+
+Replacing `unit` by a record or a variant doesn't make the injectivity annotation valid.
+
+```ocaml
+type record = { a : string }
+
+module Trait = Provider.Trait.Create1 (struct
+  type !'a t = record
+  type 'a module_type = 'a
+end)
+```
+```mdx-error
+Line 4, characters 5-24:
+Error: In this definition, expected parameter variances are not satisfied.
+       The 1st type parameter was expected to be injective invariant,
+       but it is unrestricted.
+```
+
+```ocaml
+type variant = A
+
+module Trait = Provider.Trait.Create1 (struct
+  type !'a t = variant
+  type 'a module_type = 'a
+end)
+```
+```mdx-error
+Line 4, characters 5-25:
+Error: In this definition, expected parameter variances are not satisfied.
+       The 1st type parameter was expected to be injective invariant,
+       but it is unrestricted.
+```
+
+If you bind the `'a` parameter so the annotation pass, the definition of the trait is valid.
+
+```ocaml
+module Trait = Provider.Trait.Create1 (struct
+  type !'a t = 'a
+  type 'a module_type = 'a
+end)
+```
+
+Granted, you can coerce it with different types:
+
+```ocaml
+let a = (Trait.t : ('a, 'a, [ `A]) Provider.Trait.t) ;;
+let b = (Trait.t : (string, string, [ `A]) Provider.Trait.t) ;;
+let c = (Trait.t : (int, int, [ `A]) Provider.Trait.t) ;;
+```
+
+But the point is that now the parameters of the first and second arguments are bound:
+
+```ocaml
+let _ = (Trait.t : (unit, string, [ `A]) Provider.Trait.t) ;;
+```
+```mdx-error
+Line 1, characters 10-17:
+Error: This expression has type (unit, unit, 'a) Provider.Trait.t
+       but an expression was expected of type
+         (unit, string, [ `A ]) Provider.Trait.t
+       Type unit is not compatible with type string
+```
+
+So, the rest of the test does not apply.
+
+```ocaml
+let a = (Trait.t : (string, string, [ `A ]) Provider.Trait.t)
+let h = Provider.Handler.make [ Provider.Trait.implement a ~impl:"hello" ]
+let b = (Trait.t : (int, int, [ `A ]) Provider.Trait.t)
+```
+
+```ocaml
+let crash () =
+  let (i : int) = Provider.Handler.lookup h ~trait:b in
+  assert (Stdlib.Obj.is_int (Stdlib.Obj.repr i))
+;;
+```
+```mdx-error
+Line 2, characters 54-55:
+Error: This expression has type (int, int, [ `A ]) Provider.Trait.t
+       but an expression was expected of type
+         (string, 'a, 'b) Provider.Trait.t
+       Type int is not compatible with type string
+```
+
 ## For reference
 
-We're keeping the rest of the test for reference only, it cannot be written with recent versions of the library anymore.
+We're keeping the rest of the original test for reference only, it cannot be written with recent versions of the library anymore.
 
 <!-- $MDX skip -->
 ```ocaml

From a5e6593b456277b3ab59b6f843d0d502555bc50c Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 14:41:57 +0100
Subject: [PATCH 07/15] Add test with coverage for trait0

---
 src/provider.ml       |  1 +
 src/provider.mli      |  2 ++
 test/test__trait0.ml  | 78 +++++++++++++++++++++++++++++++++++++++++++
 test/test__trait0.mli |  0
 4 files changed, 81 insertions(+)
 create mode 100644 test/test__trait0.ml
 create mode 100644 test/test__trait0.mli

diff --git a/src/provider.ml b/src/provider.ml
index b59a045..e37762a 100644
--- a/src/provider.ml
+++ b/src/provider.ml
@@ -242,4 +242,5 @@ type -'tags t =
 module Private = struct
   module Import = Import
   module Handler = Handler
+  module Trait0 = Trait0
 end
diff --git a/src/provider.mli b/src/provider.mli
index ce5e65a..564ce89 100644
--- a/src/provider.mli
+++ b/src/provider.mli
@@ -287,4 +287,6 @@ module Private : sig
       val of_int : int -> t
     end
   end
+
+  module Trait0 = Trait0
 end
diff --git a/test/test__trait0.ml b/test/test__trait0.ml
new file mode 100644
index 0000000..ed68d3a
--- /dev/null
+++ b/test/test__trait0.ml
@@ -0,0 +1,78 @@
+(* In this section we make sure to exercise all available [Create] functors and
+   monitor the 2 branches of the [same_witness] functions. *)
+
+let same_trait t1 t2 =
+  match Provider.Private.Trait0.same_witness t1 t2 with
+  | Equal -> true
+  | Not_equal -> false
+;;
+
+let%expect_test "Create" =
+  let module T1 =
+    Provider.Trait.Create (struct
+      type 'a module_type = (module T with type t = 'a)
+    end)
+  in
+  let module T2 =
+    Provider.Trait.Create (struct
+      type 'a module_type = (module T with type t = 'a)
+    end)
+  in
+  require [%here] (same_trait T1.t T1.t : bool);
+  require [%here] (not (same_trait T1.t T2.t : bool));
+  ()
+;;
+
+let%expect_test "Create0" =
+  let module T1 =
+    Provider.Trait.Create0 (struct
+      type t = unit
+      type module_type = unit
+    end)
+  in
+  let module T2 =
+    Provider.Trait.Create0 (struct
+      type t = unit
+      type module_type = unit
+    end)
+  in
+  require [%here] (same_trait T1.t T1.t : bool);
+  require [%here] (not (same_trait T1.t T2.t : bool));
+  ()
+;;
+
+let%expect_test "Create1" =
+  let module T1 =
+    Provider.Trait.Create1 (struct
+      type 'a t = 'a
+      type 'a module_type = unit
+    end)
+  in
+  let module T2 =
+    Provider.Trait.Create1 (struct
+      type 'a t = 'a
+      type 'a module_type = unit
+    end)
+  in
+  require [%here] (same_trait T1.t T1.t : bool);
+  require [%here] (not (same_trait T1.t T2.t : bool));
+  ()
+;;
+
+let%expect_test "Create2" =
+  let module T1 =
+    Provider.Trait.Create2 (struct
+      type ('a, 'b) t = 'a * 'b
+      type ('a, 'b) module_type = unit
+    end)
+  in
+  let module T2 =
+    Provider.Trait.Create2 (struct
+      type ('a, 'b) t = 'a * 'b
+      type ('a, 'b) module_type = unit
+    end)
+  in
+  require [%here] (same_trait T1.t T1.t : bool);
+  require [%here] (not (same_trait T1.t T2.t : bool));
+  ()
+;;
diff --git a/test/test__trait0.mli b/test/test__trait0.mli
new file mode 100644
index 0000000..e69de29

From 496a204b6a2b722dac2127b570bcdd69ccd75fb1 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:03:06 +0100
Subject: [PATCH 08/15] Add context related to marshal

---
 test/test__trait0.ml | 52 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/test/test__trait0.ml b/test/test__trait0.ml
index ed68d3a..de402b6 100644
--- a/test/test__trait0.ml
+++ b/test/test__trait0.ml
@@ -76,3 +76,55 @@ let%expect_test "Create2" =
   require [%here] (not (same_trait T1.t T2.t : bool));
   ()
 ;;
+
+(* Below we add extra tests regarding Marshal, just for added context. They are
+   not directly related to the project but are interesting context to have in
+   mind while working on the representation of traits. *)
+
+let%expect_test "Marshal extensible variant" =
+  (* Marshalling breaks extensible variant matching, as explained in the OCaml
+     documentation. *)
+  let module E = struct
+    type t = ..
+    type t += A | B of int
+  end
+  in
+  let open E in
+  require [%here] (phys_equal A A);
+  require [%here] (not (phys_equal A (B 0)));
+  require [%here] (not (phys_equal (B 0) (B 0)));
+  let id (t : t) =
+    Stdlib.Obj.Extension_constructor.id (Stdlib.Obj.Extension_constructor.of_val t)
+  in
+  require [%here] (id (B 0) = id (B 0));
+  require [%here] (id (B 0) = id (B 2));
+  (* Marshalling does not preserve physical equality of extensible variant with
+     no arguments. *)
+  let marshal = Stdlib.Marshal.to_string A [] in
+  let a2 = Stdlib.Marshal.from_string marshal 0 in
+  require [%here] (not (phys_equal A a2));
+  (* Marshalling does not preserve extension constructor ids. *)
+  let marshal = Stdlib.Marshal.to_string (B 0) [] in
+  let b2 = Stdlib.Marshal.from_string marshal 0 in
+  require [%here] (id (B 0) <> id b2);
+  ()
+;;
+
+let%expect_test "Marshal" =
+  (* Because trait contain extensible variant, they inherit some behavior from
+     they as it relates to marshalling traits.
+
+     In short: do not marshall traits. *)
+  let module T =
+    Provider.Trait.Create (struct
+      type 'a module_type = (module T with type t = 'a)
+    end)
+  in
+  let t1 = T.t in
+  require [%here] (same_trait t1 t1 : bool);
+  let marshal = Stdlib.Marshal.to_string T.t [ Closures ] in
+  let t2 = Stdlib.Marshal.from_string marshal 0 in
+  require [%here] (same_trait t2 t2 : bool);
+  require [%here] (not (same_trait t1 t2 : bool));
+  ()
+;;

From 03ee54edd07c5f47344ca4b7c3aced2bfaa01e48 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:09:11 +0100
Subject: [PATCH 09/15] Move same to trait0

---
 src/provider.ml | 7 +++----
 src/trait0.ml   | 4 ++++
 src/trait0.mli  | 1 +
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/provider.ml b/src/provider.ml
index e37762a..c27bc88 100644
--- a/src/provider.ml
+++ b/src/provider.ml
@@ -9,7 +9,6 @@ let () =
 ;;
 
 let raise_s msg sexp = raise (E (Sexp.List [ Atom msg; sexp ]))
-let phys_same t1 t2 = phys_equal (Obj.repr t1) (Obj.repr t2)
 
 module Trait = struct
   type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t
@@ -57,9 +56,9 @@ module Trait = struct
     let seeded_hash = Int.seeded_hash
   end
 
-  let uid (t : _ t) = Trait0.uid t
-  let compare_by_uid id1 id2 = Uid.compare (uid id1) (uid id2)
-  let same (id1 : _ t) (id2 : _ t) = phys_same id1 id2
+  let uid = Trait0.uid
+  let compare_by_uid t1 t2 = Uid.compare (uid t1) (uid t2)
+  let same = Trait0.same
   let implement = Binding0.implement
 end
 
diff --git a/src/trait0.ml b/src/trait0.ml
index b37b83f..9eb9b76 100644
--- a/src/trait0.ml
+++ b/src/trait0.ml
@@ -1,3 +1,5 @@
+open! Import
+
 type ('t, 'module_type) ext = ..
 
 type ('t, 'module_type, 'tag) t =
@@ -11,6 +13,8 @@ let same_witness : ('t, 'mt1, _) t -> ('t, 'mt2, _) t -> ('mt1, 'mt2) Type_eq_op
   fun t1 t2 -> t1.same_witness t2.ext
 ;;
 
+let same (t1 : _ t) (t2 : _ t) = phys_equal (Obj.repr t1) (Obj.repr t2)
+
 module Create0 (X : sig
     type t
     type module_type
diff --git a/src/trait0.mli b/src/trait0.mli
index 8683389..88c195f 100644
--- a/src/trait0.mli
+++ b/src/trait0.mli
@@ -31,3 +31,4 @@ end
 val uid : _ t -> int
 
 val same_witness : ('t, 'mt1, _) t -> ('t, 'mt2, _) t -> ('mt1, 'mt2) Type_eq_opt.t
+val same : _ t -> _ t -> bool

From 34a6e9ec29f3f795618d8987357f01050974e6d7 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:18:31 +0100
Subject: [PATCH 10/15] Assert unreachable point and document

---
 src/provider.ml | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/provider.ml b/src/provider.ml
index c27bc88..1e439e9 100644
--- a/src/provider.ml
+++ b/src/provider.ml
@@ -153,14 +153,11 @@ module Handler = struct
            if update_cache then t.(0) <- binding;
            if_found implementation
          | Not_equal ->
-           (* [same_witness a b => (uid a = uid b)] but the converse might not
-              hold. We treat as invalid usages cases where traits (t1, t2) would
-              have the same uids without being physically equal. *)
-           raise_s
-             "Invalid usage of [Provider.Trait]: Extensible variants with the same id \
-              are expected to be physically equal through the use of this library"
-             (Sexp.List
-                [ List [ Atom "trait"; Trait.info trait |> Trait.Info.sexp_of_t ] ])))
+           (* Because [Trait0.t] is abstract, traits are necessarily created
+              through the [Trait0.Create*] functors, which only create 0-arg [T]
+              extensible variants. As a result, for all traits (a, b) the
+              following holds: [(uid a = uid b) => phys_equal a b]. *)
+           assert false))
   ;;
 
   let make_lookup

From 4cd22d80bba58eca162ac674042d86896615e489 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:26:19 +0100
Subject: [PATCH 11/15] Update tutorial

---
 doc/docs/tutorials/getting-started/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/docs/tutorials/getting-started/README.md b/doc/docs/tutorials/getting-started/README.md
index 3a3457c..22eca89 100644
--- a/doc/docs/tutorials/getting-started/README.md
+++ b/doc/docs/tutorials/getting-started/README.md
@@ -121,7 +121,7 @@ If you are not using opam or dune, we'll assume you're an expert and know what t
 To use Provider, first we have to create a new tag and a new type constructor that will be attached to our `READER` Trait. To do this, we:
 
 - Create a tag type with a polymorphic variant that will be dedicated to our Trait.
-- Add dynamically a new constructor to the `Provider.Trait.t` extensible variant. This uses an OCaml Language Extension named [Extensible variant types](https://ocaml.org/manual/5.2/extensiblevariants.html). This one has the particularity that it is also a [GADT](https://ocaml.org/manual/5.2/gadts.html#start-section)!
+- Create a new trait with one of the `Provider.Trait.Create*` functors.
 
 ```ocaml
 type reader = [ `Reader ]

From 47433232967c047e3ffc9b8267f0ff441dae0bc0 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:26:33 +0100
Subject: [PATCH 12/15] Relax the module_type guidance

---
 src/provider.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/provider.mli b/src/provider.mli
index 564ce89..76c3647 100644
--- a/src/provider.mli
+++ b/src/provider.mli
@@ -26,8 +26,8 @@ module Trait : sig
       - ['tag] is the tag (or tags) indicating the supported Trait. It's a
         phantom type designed to make {!val:Handler.lookup} more type-safe.
 
-      ['module_type] is expected to be a module type (Eio supports single
-      functions but this is discouraged through the use of this library). *)
+      ['module_type] is typically expected to be a module type, but it doesn't
+      have too (functions, constants are fine too, etc.). *)
   type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t
 
   (** {1 Creating traits} *)

From d221e6fb7f82e1a13870b87e185481011667dbdc Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 15:26:41 +0100
Subject: [PATCH 13/15] Update changelog

---
 CHANGES.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGES.md b/CHANGES.md
index cfef096..f3d6ee5 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -4,6 +4,7 @@
 
 ### Changed
 
+- Change the API to make the library Type-Safe (breaking change). (#PR, @mbarbin, @v-gb).
 - Register custom trait names instead of extensible variant names (#31, @mbarbin).
 
 ### Deprecated

From f79e5271bd81eb85e359304bc3604f49f129b63a Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 16:20:48 +0100
Subject: [PATCH 14/15] Support more parametrizing cases

---
 doc/docs/tutorials/handler-explicit/README.md |  6 ++---
 src/provider.mli                              | 12 ++++-----
 src/trait0.ml                                 | 20 +++++++-------
 src/trait0.mli                                | 12 ++++-----
 test/mdx/test__magic3.md                      | 26 +++++++++----------
 test/test__higher_kinded.ml                   |  6 ++---
 test/test__trait0.ml                          | 12 ++++-----
 7 files changed, 47 insertions(+), 47 deletions(-)

diff --git a/doc/docs/tutorials/handler-explicit/README.md b/doc/docs/tutorials/handler-explicit/README.md
index cae5e02..1d0be7f 100644
--- a/doc/docs/tutorials/handler-explicit/README.md
+++ b/doc/docs/tutorials/handler-explicit/README.md
@@ -276,9 +276,9 @@ module Mappable : sig
         , (module Mappable with type higher_kinded = 'higher_kinded)
         , [> mappable ] )
         Provider.Trait.t
-end = Provider.Trait.Create2 (struct
-  type (!'a, !'higher_kinded) t = ('a -> 'higher_kinded) Higher_kinded.t
-  type ('a, 'higher_kinded) module_type = (module Mappable with type higher_kinded = 'higher_kinded)
+end = Provider.Trait.Create1 (struct
+  type (!'higher_kinded, 'a) t = ('a -> 'higher_kinded) Higher_kinded.t
+  type 'higher_kinded module_type = (module Mappable with type higher_kinded = 'higher_kinded)
 end)
 ```
 
diff --git a/src/provider.mli b/src/provider.mli
index 76c3647..65e9843 100644
--- a/src/provider.mli
+++ b/src/provider.mli
@@ -33,10 +33,10 @@ module Trait : sig
   (** {1 Creating traits} *)
 
   module Create0 (X : sig
-      type t
+      type 'a t
       type module_type
     end) : sig
-    val t : (X.t, X.module_type, _) t
+    val t : ('a X.t, X.module_type, _) t
   end
 
   module Create (X : sig
@@ -46,17 +46,17 @@ module Trait : sig
   end
 
   module Create1 (X : sig
-      type !'a t
+      type (!'a, 'b) t
       type 'a module_type
     end) : sig
-    val t : ('a X.t, 'a X.module_type, _) t
+    val t : (('a, 'b) X.t, 'a X.module_type, _) t
   end
 
   module Create2 (X : sig
-      type (!'a, !'b) t
+      type (!'a, !'b, 'c) t
       type ('a, 'b) module_type
     end) : sig
-    val t : (('a, 'b) X.t, ('a, 'b) X.module_type, _) t
+    val t : (('a, 'b, 'c) X.t, ('a, 'b) X.module_type, _) t
   end
 
   (** {1 Dump & debug} *)
diff --git a/src/trait0.ml b/src/trait0.ml
index 9eb9b76..67a7a73 100644
--- a/src/trait0.ml
+++ b/src/trait0.ml
@@ -16,14 +16,14 @@ let same_witness : ('t, 'mt1, _) t -> ('t, 'mt2, _) t -> ('mt1, 'mt2) Type_eq_op
 let same (t1 : _ t) (t2 : _ t) = phys_equal (Obj.repr t1) (Obj.repr t2)
 
 module Create0 (X : sig
-    type t
+    type 'a t
     type module_type
   end) =
 struct
-  type (_, _) ext += T : (X.t, X.module_type) ext
+  type (_, _) ext += T : ('a X.t, X.module_type) ext
 
   let same_witness (type m2) t2 : (X.module_type, m2) Type_eq_opt.t =
-    match (t2 : (X.t, m2) ext) with
+    match (t2 : (_ X.t, m2) ext) with
     | T -> Type_eq_opt.Equal
     | _ -> Not_equal
   ;;
@@ -32,14 +32,14 @@ struct
 end
 
 module Create1 (X : sig
-    type !'a t
+    type (!'a, 'b) t
     type 'a module_type
   end) =
 struct
-  type (_, _) ext += T : ('a X.t, 'a X.module_type) ext
+  type (_, _) ext += T : (('a, 'b) X.t, 'a X.module_type) ext
 
   let same_witness (type a m2) t2 : (a X.module_type, m2) Type_eq_opt.t =
-    match (t2 : (a X.t, m2) ext) with
+    match (t2 : ((a, _) X.t, m2) ext) with
     | T -> Type_eq_opt.Equal
     | _ -> Not_equal
   ;;
@@ -48,14 +48,14 @@ struct
 end
 
 module Create2 (X : sig
-    type (!'a, !'b) t
+    type (!'a, !'b, 'c) t
     type ('a, 'b) module_type
   end) =
 struct
-  type (_, _) ext += T : (('a, 'b) X.t, ('a, 'b) X.module_type) ext
+  type (_, _) ext += T : (('a, 'b, 'c) X.t, ('a, 'b) X.module_type) ext
 
   let same_witness (type a b m2) t2 : ((a, b) X.module_type, m2) Type_eq_opt.t =
-    match (t2 : ((a, b) X.t, m2) ext) with
+    match (t2 : ((a, b, _) X.t, m2) ext) with
     | T -> Type_eq_opt.Equal
     | _ -> Not_equal
   ;;
@@ -67,6 +67,6 @@ module Create (X : sig
     type 'a module_type
   end) =
 Create1 (struct
-    type !'a t = 'a
+    type (!'a, _) t = 'a
     type 'a module_type = 'a X.module_type
   end)
diff --git a/src/trait0.mli b/src/trait0.mli
index 88c195f..54dbad7 100644
--- a/src/trait0.mli
+++ b/src/trait0.mli
@@ -7,24 +7,24 @@ module Create (X : sig
 end
 
 module Create0 (X : sig
-    type t
+    type 'a t
     type module_type
   end) : sig
-  val t : (X.t, X.module_type, _) t
+  val t : ('a X.t, X.module_type, _) t
 end
 
 module Create1 (X : sig
-    type !'a t
+    type (!'a, 'b) t
     type 'a module_type
   end) : sig
-  val t : ('a X.t, 'a X.module_type, _) t
+  val t : (('a, 'b) X.t, 'a X.module_type, _) t
 end
 
 module Create2 (X : sig
-    type (!'a, !'b) t
+    type (!'a, !'b, 'c) t
     type ('a, 'b) module_type
   end) : sig
-  val t : (('a, 'b) X.t, ('a, 'b) X.module_type, _) t
+  val t : (('a, 'b, 'c) X.t, ('a, 'b) X.module_type, _) t
 end
 
 (** Return a id that is unique to this trait for the lifetime of the program. *)
diff --git a/test/mdx/test__magic3.md b/test/mdx/test__magic3.md
index d696bf3..23b8328 100644
--- a/test/mdx/test__magic3.md
+++ b/test/mdx/test__magic3.md
@@ -20,33 +20,33 @@ This is rejected through injectivity check.
 
 ```ocaml
 module Trait = Provider.Trait.Create1 (struct
-  type 'a t = unit
+  type (_, _) t = unit
   type 'a module_type = 'a
 end)
 ```
 ```mdx-error
 Lines 1-4, characters 16-7:
 Error: Modules do not match:
-       sig type 'a t = unit type 'a module_type = 'a end
-     is not included in sig type !'a t type 'a module_type end
+       sig type (_, _) t = unit type 'a module_type = 'a end
+     is not included in sig type (!'a, 'b) t type 'a module_type end
      Type declarations do not match:
-       type 'a t = unit
+       type (_, _) t = unit
      is not included in
-       type !'a t
+       type (!'a, 'b) t
      Their variances do not agree.
-     File "src/provider.mli", line 49, characters 6-16: Expected declaration
+     File "src/provider.mli", line 73, characters 6-22: Expected declaration
 ```
 
 Trying to force the injectivity won't do either.
 
 ```ocaml
 module Trait = Provider.Trait.Create1 (struct
-  type !'a t = unit
+  type (!'a, _) t = unit
   type 'a module_type = 'a
 end)
 ```
 ```mdx-error
-Line 2, characters 5-22:
+Line 2, characters 5-27:
 Error: In this definition, expected parameter variances are not satisfied.
        The 1st type parameter was expected to be injective invariant,
        but it is unrestricted.
@@ -60,12 +60,12 @@ Replacing `unit` by a record or a variant doesn't make the injectivity annotatio
 type record = { a : string }
 
 module Trait = Provider.Trait.Create1 (struct
-  type !'a t = record
+  type (!'a, _) t = record
   type 'a module_type = 'a
 end)
 ```
 ```mdx-error
-Line 4, characters 5-24:
+Line 4, characters 5-29:
 Error: In this definition, expected parameter variances are not satisfied.
        The 1st type parameter was expected to be injective invariant,
        but it is unrestricted.
@@ -75,12 +75,12 @@ Error: In this definition, expected parameter variances are not satisfied.
 type variant = A
 
 module Trait = Provider.Trait.Create1 (struct
-  type !'a t = variant
+  type (!'a, _) t = variant
   type 'a module_type = 'a
 end)
 ```
 ```mdx-error
-Line 4, characters 5-25:
+Line 4, characters 5-30:
 Error: In this definition, expected parameter variances are not satisfied.
        The 1st type parameter was expected to be injective invariant,
        but it is unrestricted.
@@ -90,7 +90,7 @@ If you bind the `'a` parameter so the annotation pass, the definition of the tra
 
 ```ocaml
 module Trait = Provider.Trait.Create1 (struct
-  type !'a t = 'a
+  type (!'a, _) t = 'a
   type 'a module_type = 'a
 end)
 ```
diff --git a/test/test__higher_kinded.ml b/test/test__higher_kinded.ml
index 0f87a1f..cb9d7d7 100644
--- a/test/test__higher_kinded.ml
+++ b/test/test__higher_kinded.ml
@@ -28,10 +28,10 @@ module Mappable : sig
         , (module Mappable with type higher_kinded = 'higher_kinded)
         , [> mappable ] )
         Provider.Trait.t
-end = Provider.Trait.Create2 (struct
-    type (!'a, !'higher_kinded) t = ('a -> 'higher_kinded) Higher_kinded.t
+end = Provider.Trait.Create1 (struct
+    type (!'higher_kinded, 'a) t = ('a -> 'higher_kinded) Higher_kinded.t
 
-    type ('a, 'higher_kinded) module_type =
+    type 'higher_kinded module_type =
       (module Mappable with type higher_kinded = 'higher_kinded)
   end)
 
diff --git a/test/test__trait0.ml b/test/test__trait0.ml
index de402b6..3cabab7 100644
--- a/test/test__trait0.ml
+++ b/test/test__trait0.ml
@@ -26,13 +26,13 @@ let%expect_test "Create" =
 let%expect_test "Create0" =
   let module T1 =
     Provider.Trait.Create0 (struct
-      type t = unit
+      type _ t = unit
       type module_type = unit
     end)
   in
   let module T2 =
     Provider.Trait.Create0 (struct
-      type t = unit
+      type _ t = unit
       type module_type = unit
     end)
   in
@@ -44,13 +44,13 @@ let%expect_test "Create0" =
 let%expect_test "Create1" =
   let module T1 =
     Provider.Trait.Create1 (struct
-      type 'a t = 'a
+      type ('a, _) t = 'a
       type 'a module_type = unit
     end)
   in
   let module T2 =
     Provider.Trait.Create1 (struct
-      type 'a t = 'a
+      type ('a, _) t = 'a
       type 'a module_type = unit
     end)
   in
@@ -62,13 +62,13 @@ let%expect_test "Create1" =
 let%expect_test "Create2" =
   let module T1 =
     Provider.Trait.Create2 (struct
-      type ('a, 'b) t = 'a * 'b
+      type ('a, 'b, _) t = 'a * 'b
       type ('a, 'b) module_type = unit
     end)
   in
   let module T2 =
     Provider.Trait.Create2 (struct
-      type ('a, 'b) t = 'a * 'b
+      type ('a, 'b, _) t = 'a * 'b
       type ('a, 'b) module_type = unit
     end)
   in

From 6d6ee17fe862faf2e1e51d18f762a40129dec374 Mon Sep 17 00:00:00 2001
From: Mathieu Barbin <mathieu.barbin@gmail.com>
Date: Thu, 31 Oct 2024 16:31:32 +0100
Subject: [PATCH 15/15] Add documentation for Create functors

---
 src/provider.mli | 42 +++++++++++++++++++++++++++++++++---------
 1 file changed, 33 insertions(+), 9 deletions(-)

diff --git a/src/provider.mli b/src/provider.mli
index 65e9843..cd6d6c2 100644
--- a/src/provider.mli
+++ b/src/provider.mli
@@ -23,21 +23,38 @@ module Trait : sig
 
       - ['t] is the internal state of the provider itself.
       - ['module_type] is the signature of a module implementing the Trait.
-      - ['tag] is the tag (or tags) indicating the supported Trait. It's a
-        phantom type designed to make {!val:Handler.lookup} more type-safe.
+      - ['tag] is the tag (or tags) indicating the supported Trait(s). It's a
+        phantom type designed to help using {!val:Handler.lookup} correctly.
 
       ['module_type] is typically expected to be a module type, but it doesn't
       have too (functions, constants are fine too, etc.). *)
   type ('t, 'module_type, 'tag) t = ('t, 'module_type, 'tag) Trait0.t
 
-  (** {1 Creating traits} *)
+  (** {1 Creating traits}
 
-  module Create0 (X : sig
-      type 'a t
-      type module_type
-    end) : sig
-    val t : ('a X.t, X.module_type, _) t
-  end
+      Traits are abstract and must be created using the following functors. The
+      most common one is {!module:Create}. It is to be used when the trait is
+      defined by a module type with a single type t. For example:
+
+      {[
+        module type Show = sig
+          type t
+
+          val show : t -> string
+        end
+
+        module Show : sig
+          val t : ('a, (module Show with type t = 'a), [> `Show ]) Provider.Trait.t
+        end = Provider.Trait.Create (struct
+            type 'a module_type = (module Show with type t = 'a)
+          end)
+      ]}
+
+      The other functors are reserved for less common cases. The number suffix
+      indicates the number of parameters of the [module_type] type, each of
+      which must be present and injective in [X.t]. We added one extra parameter
+      to [X.t] to allow for more flexibility in what can be expressed, but not
+      all parameters have to be used. *)
 
   module Create (X : sig
       type 'a module_type
@@ -45,6 +62,13 @@ module Trait : sig
     val t : ('a, 'a X.module_type, _) t
   end
 
+  module Create0 (X : sig
+      type 'a t
+      type module_type
+    end) : sig
+    val t : ('a X.t, X.module_type, _) t
+  end
+
   module Create1 (X : sig
       type (!'a, 'b) t
       type 'a module_type