From b47c34912c4fb8494d91245bbf7983b87884efb7 Mon Sep 17 00:00:00 2001 From: Jacques Garrigue Date: Fri, 20 Nov 2020 16:29:23 +0900 Subject: [PATCH] Mark datatypes as injective in recursive module approximations (#10029) --- testsuite/tests/typing-misc/injectivity.ml | 12 ++++++++++++ typing/datarepr.ml | 2 +- typing/typeclass.ml | 8 ++++---- typing/typedecl.ml | 11 ++++++----- typing/typedecl.mli | 2 +- typing/types.ml | 5 +++-- typing/types.mli | 2 +- 7 files changed, 28 insertions(+), 14 deletions(-) diff --git a/testsuite/tests/typing-misc/injectivity.ml b/testsuite/tests/typing-misc/injectivity.ml index bed73a1ca..afe16e4b5 100644 --- a/testsuite/tests/typing-misc/injectivity.ml +++ b/testsuite/tests/typing-misc/injectivity.ml @@ -423,3 +423,15 @@ Line 1, characters 18-21: ^^^ Error: Unbound module R |}] + +(* #10028 by Stephen Dolan *) + +module rec A : sig + type _ t = Foo : 'a -> 'a A.s t + type 'a s = T of 'a +end = + A +;; +[%%expect{| +module rec A : sig type _ t = Foo : 'a -> 'a A.s t type 'a s = T of 'a end +|}] diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 97bbf87f6..989395c0f 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -85,7 +85,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep = type_kind = Type_record (lbls, rep); type_private = priv; type_manifest = None; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:true ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; diff --git a/typing/typeclass.ml b/typing/typeclass.ml index 04400c53e..12dec437a 100644 --- a/typing/typeclass.ml +++ b/typing/typeclass.ml @@ -1311,7 +1311,7 @@ let temp_abbrev loc env id arity uid = type_kind = Type_abstract; type_private = Public; type_manifest = Some ty; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:false ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; @@ -1490,7 +1490,7 @@ let class_infos define_class kind (* Class and class type temporary definitions *) let cty_variance = - Variance.unknown_signature ~arity:(List.length params) in + Variance.unknown_signature ~injective:false ~arity:(List.length params) in let cltydef = {clty_params = params; clty_type = class_body typ; clty_variance = cty_variance; @@ -1572,7 +1572,7 @@ let class_infos define_class kind type_kind = Type_abstract; type_private = Public; type_manifest = Some obj_ty; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:false ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; @@ -1596,7 +1596,7 @@ let class_infos define_class kind type_kind = Type_abstract; type_private = Public; type_manifest = Some cl_ty; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:false ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; diff --git a/typing/typedecl.ml b/typing/typedecl.ml index ae25fc6b6..7c700b1ab 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -114,7 +114,7 @@ let enter_type rec_flag env sdecl (id, uid) = type_manifest = begin match sdecl.ptype_manifest with None -> None | Some _ -> Some(Ctype.newvar ()) end; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:false ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; @@ -403,7 +403,7 @@ let transl_declaration env sdecl (id, uid) = type_kind = kind; type_private = sdecl.ptype_private; type_manifest = man; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective:false ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; @@ -1531,7 +1531,7 @@ let transl_with_constraint id row_path ~sig_env ~sig_decl ~outer_env sdecl = (* Approximate a type declaration: just make all types abstract *) -let abstract_type_decl arity = +let abstract_type_decl ~injective arity = let rec make_params n = if n <= 0 then [] else Ctype.newvar() :: make_params (n-1) in Ctype.begin_def(); @@ -1541,7 +1541,7 @@ let abstract_type_decl arity = type_kind = Type_abstract; type_private = Public; type_manifest = None; - type_variance = Variance.unknown_signature ~arity; + type_variance = Variance.unknown_signature ~injective ~arity; type_separability = Types.Separability.default_signature ~arity; type_is_newtype = false; type_expansion_scope = Btype.lowest_level; @@ -1559,8 +1559,9 @@ let approx_type_decl sdecl_list = let scope = Ctype.create_scope () in List.map (fun sdecl -> + let injective = sdecl.ptype_kind <> Ptype_abstract in (Ident.create_scoped ~scope sdecl.ptype_name.txt, - abstract_type_decl (List.length sdecl.ptype_params))) + abstract_type_decl ~injective (List.length sdecl.ptype_params))) sdecl_list (* Variant of check_abbrev_recursion to check the well-formedness diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 88f5b2f14..fec0bd65b 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -44,7 +44,7 @@ val transl_with_constraint: outer_env:Env.t -> Parsetree.type_declaration -> Typedtree.type_declaration -val abstract_type_decl: int -> type_declaration +val abstract_type_decl: injective:bool -> int -> type_declaration val approx_type_decl: Parsetree.type_declaration list -> (Ident.t * type_declaration) list diff --git a/typing/types.ml b/typing/types.ml index 9d0817c09..d723a3042 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -187,8 +187,9 @@ module Variance = struct let conjugate v = swap May_pos May_neg (swap Pos Neg v) let get_upper v = (mem May_pos v, mem May_neg v) let get_lower v = (mem Pos v, mem Neg v, mem Inv v, mem Inj v) - let unknown_signature ~arity = - Misc.replicate_list unknown arity + let unknown_signature ~injective ~arity = + let v = if injective then set Inj true unknown else unknown in + Misc.replicate_list v arity end module Separability = struct diff --git a/typing/types.mli b/typing/types.mli index d36f26c2d..98bd408f7 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -308,7 +308,7 @@ module Variance : sig val conjugate : t -> t (* exchange positive and negative *) val get_upper : t -> bool * bool (* may_pos, may_neg *) val get_lower : t -> bool * bool * bool * bool (* pos, neg, inv, inj *) - val unknown_signature : arity:int -> t list + val unknown_signature : injective:bool -> arity:int -> t list (** The most pessimistic variance for a completely unknown type. *) end