Ekdohibs
/
ocaml
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

pattern aliases do not ignore type constraints (#1655)

master
Thomas Refis 2020-07-09 12:20:37 +02:00 committed by GitHub
parent 5940632496
commit 4edc4b9928
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 202 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Changes
View File

@ -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:

24
testsuite/tests/typing-gadts/or_patterns.ml
View File

@ -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 = <fun>
|}]
(* 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 = <fun>
|}]
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
|}]

2
testsuite/tests/typing-gadts/principality-and-gadts.ml
View File

@ -362,7 +362,7 @@ val foo : int foo -> int = <fun>
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 = <fun>
|}]

155
testsuite/tests/typing-misc/build_as_type.ml Normal file
View File

@ -0,0 +1,155 @@
(* TEST
* expect
*)
let f = function
| ([] : int list) as x -> x
| _ :: _ -> assert false;;
[%%expect{|
val f : int list -> int list = <fun>
|}]
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) = (<fun>, <fun>)
|}]
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) = (<fun>, <fun>)
|}]
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) = (<fun>, <fun>)
|}]
type t = [ `A | `B ];;
[%%expect{|
type t = [ `A | `B ]
|}]
let f = function `A as x -> x | `B -> `A;;
[%%expect{|
val f : [< `A | `B ] -> [> `A ] = <fun>
|}]
let f = function (`A : t) as x -> x | `B -> `A;;
[%%expect{|
val f : t -> t = <fun>
|}]
let f : t -> _ = function `A as x -> x | `B -> `A;;
[%%expect{|
val f : t -> [> `A ] = <fun>
|}]
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 = <fun>
|}]
let f = function
| (`A : t) as x ->
begin match x with
| `A -> ()
| `B -> ()
end
| `B -> ();;
[%%expect{|
val f : t -> unit = <fun>
|}]
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 = <fun>
|}]
(* 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 = <fun>
|}]
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 = <fun>
|}]

6
testsuite/tests/typing-misc/disambiguate_principality.ml
View File

@ -304,12 +304,6 @@ let u = function
;;
[%%expect{|
val u : M.r ref -> int = <fun>
|}, 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 = <fun>
|}]

31
typing/typecore.ml
View File

@ -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'' ()

10
typing/typetexp.ml
View File

@ -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();

9
typing/typetexp.mli
View File

@ -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