Support more parametrizing cases

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)
 ```
 

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} *)

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)

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. *)

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)
 ```

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)
 

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