From 4edc4b9928f6fa7c03cf990e421558918daf27b4 Mon Sep 17 00:00:00 2001 From: Thomas Refis Date: Thu, 9 Jul 2020 12:20:37 +0200 Subject: [PATCH] pattern aliases do not ignore type constraints (#1655) --- Changes | 3 + testsuite/tests/typing-gadts/or_patterns.ml | 24 +-- .../typing-gadts/principality-and-gadts.ml | 2 +- testsuite/tests/typing-misc/build_as_type.ml | 155 ++++++++++++++++++ .../typing-misc/disambiguate_principality.ml | 6 - typing/typecore.ml | 31 ++-- typing/typetexp.ml | 10 +- typing/typetexp.mli | 9 +- 8 files changed, 202 insertions(+), 38 deletions(-) create mode 100644 testsuite/tests/typing-misc/build_as_type.ml diff --git a/Changes b/Changes index 5b7ac82fd..0ff2e99be 100644 --- a/Changes +++ b/Changes @@ -3,6 +3,9 @@ Working version ### Language features: +- #1655: pattern aliases do not ignore type constraints + (Thomas Refis, review by Jacques Garrigue and Gabriel Scherer) + * #9500, #9727: Injectivity annotations One can now mark type parameters as injective, which is useful for abstract types: diff --git a/testsuite/tests/typing-gadts/or_patterns.ml b/testsuite/tests/typing-gadts/or_patterns.ml index cfe711395..eeafa2544 100644 --- a/testsuite/tests/typing-gadts/or_patterns.ml +++ b/testsuite/tests/typing-gadts/or_patterns.ml @@ -233,11 +233,7 @@ let simple_merged_annotated_return_annotated (type a) (t : a t) (a : a) = ;; [%%expect{| -Lines 3-4, characters 4-30: -3 | ....IntLit, ((3 : a) as x) -4 | | BoolLit, ((true : a) as x)............ -Error: The variable x on the left-hand side of this or-pattern has type - a but on the right-hand side it has type bool +val simple_merged_annotated_return_annotated : 'a t -> 'a -> unit = |}] (* test more scenarios: when the or-pattern itself is not at toplevel but under @@ -579,12 +575,7 @@ let lambiguity (type a) (t2 : a t2) = ;; [%%expect{| -Line 3, characters 8-22: -3 | | Int ((_ : a) as x) - ^^^^^^^^^^^^^^ -Error: This pattern matches values of type a - This instance of a is ambiguous: - it would escape the scope of its equation +val lambiguity : 'a t2 -> 'a = |}] let rambiguity (type a) (t2 : a t2) = @@ -594,12 +585,11 @@ let rambiguity (type a) (t2 : a t2) = ;; [%%expect{| -Line 4, characters 9-23: -4 | | Bool ((_ : a) as x) -> x - ^^^^^^^^^^^^^^ -Error: This pattern matches values of type a - This instance of a is ambiguous: - it would escape the scope of its equation +Lines 3-4, characters 4-23: +3 | ....Int (_ as x) +4 | | Bool ((_ : a) as x)..... +Error: The variable x on the left-hand side of this or-pattern has type + int but on the right-hand side it has type a |}] diff --git a/testsuite/tests/typing-gadts/principality-and-gadts.ml b/testsuite/tests/typing-gadts/principality-and-gadts.ml index 9a1d13961..d4e3b9b16 100644 --- a/testsuite/tests/typing-gadts/principality-and-gadts.ml +++ b/testsuite/tests/typing-gadts/principality-and-gadts.ml @@ -362,7 +362,7 @@ val foo : int foo -> int = Line 3, characters 26-31: 3 | | { x = (x : int); eq = Refl3 } -> x ^^^^^ -Warning 18: typing this pattern requires considering M.t and N.t as equal. +Warning 18: typing this pattern requires considering M.t and int as equal. But the knowledge of these types is not principal. val foo : int foo -> int = |}] diff --git a/testsuite/tests/typing-misc/build_as_type.ml b/testsuite/tests/typing-misc/build_as_type.ml new file mode 100644 index 000000000..03aa0bfa3 --- /dev/null +++ b/testsuite/tests/typing-misc/build_as_type.ml @@ -0,0 +1,155 @@ +(* TEST + * expect +*) + +let f = function + | ([] : int list) as x -> x + | _ :: _ -> assert false;; +[%%expect{| +val f : int list -> int list = +|}] + +let f = + let f' = function + | ([] : 'a list) as x -> x + | _ :: _ -> assert false + in + f', f';; +[%%expect{| +val f : ('a list -> 'a list) * ('a list -> 'a list) = (, ) +|}] + +let f = + let f' = function + | ([] : _ list) as x -> x + | _ :: _ -> assert false + in + f', f';; +[%%expect{| +val f : ('a list -> 'b list) * ('c list -> 'd list) = (, ) +|}] + +let f = + let f' (type a) = function + | ([] : a list) as x -> x + | _ :: _ -> assert false + in + f', f';; +[%%expect{| +val f : ('a list -> 'a list) * ('b list -> 'b list) = (, ) +|}] + +type t = [ `A | `B ];; +[%%expect{| +type t = [ `A | `B ] +|}] + +let f = function `A as x -> x | `B -> `A;; +[%%expect{| +val f : [< `A | `B ] -> [> `A ] = +|}] + +let f = function (`A : t) as x -> x | `B -> `A;; +[%%expect{| +val f : t -> t = +|}] + +let f : t -> _ = function `A as x -> x | `B -> `A;; +[%%expect{| +val f : t -> [> `A ] = +|}] + +let f = function + | (`A : t) as x -> + (* This should be flagged as non-exhaustive: because of the constraint [x] + is of type [t]. *) + begin match x with + | `A -> () + end + | `B -> ();; +[%%expect{| +Lines 5-7, characters 4-7: +5 | ....begin match x with +6 | | `A -> () +7 | end +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +`B +val f : t -> unit = +|}] + + +let f = function + | (`A : t) as x -> + begin match x with + | `A -> () + | `B -> () + end + | `B -> ();; +[%%expect{| +val f : t -> unit = +|}] + + +let f = function + | (`A : t) as x -> + begin match x with + | `A -> () + | `B -> () + | `C -> () + end + | `B -> ();; +[%%expect{| +Line 6, characters 6-8: +6 | | `C -> () + ^^ +Error: This pattern matches values of type [? `C ] + but a pattern was expected which matches values of type t + The second variant type does not allow tag(s) `C +|}] + +let f = function (`A, _ : _ * int) as x -> x;; +[%%expect{| +val f : [< `A ] * int -> [> `A ] * int = +|}] + +(* Make sure *all* the constraints are respected: *) + +let f = function + | ((`A : _) : t) as x -> + (* This should be flagged as non-exhaustive: because of the constraint [x] + is of type [t]. *) + begin match x with + | `A -> () + end + | `B -> ();; +[%%expect{| +Lines 5-7, characters 4-7: +5 | ....begin match x with +6 | | `A -> () +7 | end +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +`B +val f : t -> unit = +|}] + +let f = function + | ((`A : t) : _) as x -> + (* This should be flagged as non-exhaustive: because of the constraint [x] + is of type [t]. *) + begin match x with + | `A -> () + end + | `B -> ();; + +[%%expect{| +Lines 5-7, characters 4-7: +5 | ....begin match x with +6 | | `A -> () +7 | end +Warning 8: this pattern-matching is not exhaustive. +Here is an example of a case that is not matched: +`B +val f : t -> unit = +|}] diff --git a/testsuite/tests/typing-misc/disambiguate_principality.ml b/testsuite/tests/typing-misc/disambiguate_principality.ml index fd2cae38c..3148ef360 100644 --- a/testsuite/tests/typing-misc/disambiguate_principality.ml +++ b/testsuite/tests/typing-misc/disambiguate_principality.ml @@ -304,12 +304,6 @@ let u = function ;; [%%expect{| val u : M.r ref -> int = -|}, Principal{| -Line 3, characters 7-10: -3 | !x.lbl - ^^^ -Warning 18: this type-based field disambiguation is not principal. -val u : M.r ref -> int = |}] diff --git a/typing/typecore.ml b/typing/typecore.ml index eec62eda9..96d30c270 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -466,6 +466,22 @@ let enter_orpat_variables loc env p1_vs p2_vs = unify_vars p1_vs p2_vs let rec build_as_type env p = + let as_ty = build_as_type_aux env p in + (* Cf. #1655 *) + List.fold_left (fun as_ty (extra, _loc, _attrs) -> + match extra with + | Tpat_type _ | Tpat_open _ | Tpat_unpack -> as_ty + | Tpat_constraint cty -> + begin_def (); + let ty = instance cty.ctyp_type in + end_def (); + generalize_structure ty; + (* This call to unify can't fail since the pattern is well typed. *) + unify !env (instance as_ty) (instance ty); + ty + ) as_ty p.pat_extra + +and build_as_type_aux env p = match p.pat_desc with Tpat_alias(p1,_, _) -> build_as_type env p1 | Tpat_tuple pl -> @@ -1420,8 +1436,7 @@ and type_pat_aux ({ptyp_desc=Ptyp_poly _} as sty)) -> (* explicitly polymorphic type *) assert construction_not_used_in_counterexamples; - let cty, force = Typetexp.transl_simple_type_delayed !env sty in - let ty = cty.ctyp_type in + let cty, ty, force = Typetexp.transl_simple_type_delayed !env sty in unify_pat_types ~refine lloc env ty (instance expected_ty); pattern_force := force :: !pattern_force; begin match ty.desc with @@ -1810,8 +1825,7 @@ and type_pat_aux | Ppat_constraint(sp, sty) -> (* Pretend separate = true *) begin_def(); - let cty, force = Typetexp.transl_simple_type_delayed !env sty in - let ty = cty.ctyp_type in + let cty, ty, force = Typetexp.transl_simple_type_delayed !env sty in end_def(); generalize_structure ty; let ty, expected_ty' = instance ty, ty in @@ -3124,10 +3138,9 @@ and type_expect_ let (arg, ty',cty,cty') = match sty with | None -> - let (cty', force) = + let (cty', ty', force) = Typetexp.transl_simple_type_delayed env sty' in - let ty' = cty'.ctyp_type in begin_def (); let arg = type_exp env sarg in end_def (); @@ -3171,13 +3184,11 @@ and type_expect_ (arg, ty', None, cty') | Some sty -> begin_def (); - let (cty, force) = + let (cty, ty, force) = Typetexp.transl_simple_type_delayed env sty - and (cty', force') = + and (cty', ty', force') = Typetexp.transl_simple_type_delayed env sty' in - let ty = cty.ctyp_type in - let ty' = cty'.ctyp_type in begin try let force'' = subtype env ty ty' in force (); force' (); force'' () diff --git a/typing/typetexp.ml b/typing/typetexp.ml index a55e53d00..822c8279c 100644 --- a/typing/typetexp.ml +++ b/typing/typetexp.ml @@ -687,9 +687,17 @@ let transl_simple_type_univars env styp = let transl_simple_type_delayed env styp = univars := []; used_variables := TyVarMap.empty; + begin_def (); let typ = transl_type env Extensible styp in + end_def (); make_fixed_univars typ.ctyp_type; - (typ, globalize_used_variables env false) + (* This brings the used variables to the global level, but doesn't link them + to their other occurences just yet. This will be done when [force] is + called. *) + let force = globalize_used_variables env false in + (* Generalizes everything except the variables that were just globalized. *) + generalize typ.ctyp_type; + (typ, instance typ.ctyp_type, force) let transl_type_scheme env styp = reset_type_variables(); diff --git a/typing/typetexp.mli b/typing/typetexp.mli index 5475abbc3..602b7c7af 100644 --- a/typing/typetexp.mli +++ b/typing/typetexp.mli @@ -23,10 +23,13 @@ val transl_simple_type: Env.t -> bool -> Parsetree.core_type -> Typedtree.core_type val transl_simple_type_univars: Env.t -> Parsetree.core_type -> Typedtree.core_type -val transl_simple_type_delayed: - Env.t -> Parsetree.core_type -> Typedtree.core_type * (unit -> unit) +val transl_simple_type_delayed + : Env.t + -> Parsetree.core_type + -> Typedtree.core_type * type_expr * (unit -> unit) (* Translate a type, but leave type variables unbound. Returns - the type and a function that binds the type variable. *) + the type, an instance of the corresponding type_expr, and a + function that binds the type variable. *) val transl_type_scheme: Env.t -> Parsetree.core_type -> Typedtree.core_type val reset_type_variables: unit -> unit