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