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

Merge pull request #1132 from lpw25/relax-poly-types 

* Relax the handling of explicit polymorphic types

* Fix level handling in unify_rows for the fixed case
master
Leo White 2020-01-20 16:06:34 +00:00 committed by GitHub
parent 82d7971b4f 33d4540a9d
commit 73554e3aa9
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 108 additions and 82 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
Changes
View File

@ -10,6 +10,9 @@ Working version
(Gabriel Radanne, Leo White and Gabriel Scherer,
request by Bikal Lem)
- #6673, #1132: Relax the handling of explicit polymorphic types
(Leo White, review by Jacques Garrigue and Gabriel Scherer)
### Runtime system:
- #9119: Make [caml_stat_resize_noexc] compatible with the [realloc]

8
testsuite/tests/typing-gadts/test.ml
View File

@ -816,9 +816,11 @@ let f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
Lines 1-2, characters 4-15:
1 | ....f : type a b. (a,b) eq -> [< `A of a | `B] -> [< `A of b | `B] =
2 | fun Eq o -> o..............
Error: This definition has type
('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c
which is less general than 'a0 'b0. ('a0, 'b0) eq -> 'c -> 'c
Error: This expression has type
'a 'b. ('a, 'b) eq -> ([< `A of 'b & 'a | `B ] as 'c) -> 'c
but an expression was expected of type
'a 'b. ('a, 'b) eq -> ([< `A of 'b & 'e | `B ] as 'd) -> 'd
The universal variable 'a would escape its scope
|}];;
let f : type a b. (a,b) eq -> [`A of a | `B] -> [`A of b | `B] =

12
testsuite/tests/typing-poly/poly.ml
View File

@ -1345,11 +1345,13 @@ val f : 'a -> int = <fun>
val g : 'a -> int = <fun>
type 'a t = Leaf of 'a | Node of ('a * 'a) t
val depth : 'a t -> int = <fun>
Line 6, characters 2-42:
6 | function Leaf _ -> 1 | Node x -> 1 + d x
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type 'a t -> int which is less general than
'a0. 'a0 t -> int
val depth : 'a t -> int = <fun>
val d : ('a * 'a) t -> int = <fun>
Line 9, characters 2-46:
9 | function Leaf x -> x | Node x -> 1 + depth x;; (* fails *)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This definition has type int t -> int which is less general than
'a. 'a t -> int
|}];;
(* compare with records (should be the same) *)

56
typing/ctype.ml
View File

@ -1991,32 +1991,35 @@ let enter_poly env univar_pairs t1 tl1 t2 tl2 f =
let univar_pairs = ref []
(* assumption: [ty] is fully generalized. *)
let reify_univars ty =
let rec subst_univar scope vars ty =
let ty = repr ty in
if ty.level >= lowest_level then begin
ty.level <- pivot_level - ty.level;
match ty.desc with
| Tvar name ->
For_copy.save_desc scope ty ty.desc;
let t = newty2 ty.level (Tunivar name) in
vars := t :: !vars;
ty.desc <- Tsubst t
| _ ->
iter_type_expr (subst_univar scope vars) ty
end
in
let vars = ref [] in
let ty =
For_copy.with_scope (fun scope ->
subst_univar scope vars ty;
unmark_type ty;
copy scope ty
)
in
newty2 ty.level (Tpoly(repr ty, !vars))
(**** Instantiate a generic type into a poly type ***)
let polyfy env ty vars =
let subst_univar scope ty =
let ty = repr ty in
match ty.desc with
| Tvar name when ty.level = generic_level ->
For_copy.save_desc scope ty ty.desc;
let t = newty (Tunivar name) in
ty.desc <- Tsubst t;
Some t
| _ -> None
in
(* need to expand twice? cf. Ctype.unify2 *)
let vars = List.map (expand_head env) vars in
let vars = List.map (expand_head env) vars in
For_copy.with_scope (fun scope ->
let vars' = List.filter_map (subst_univar scope) vars in
let ty = copy scope ty in
let ty = newty2 ty.level (Tpoly(repr ty, vars')) in
let complete = List.length vars = List.length vars' in
ty, complete
)
(* assumption: [ty] is fully generalized. *)
let reify_univars env ty =
let vars = free_variables ty in
let ty, _ = polyfy env ty vars in
ty
(*****************)
(* Unification *)
@ -2850,7 +2853,8 @@ and unify_row env row1 row2 =
end;
let fixed1 = fixed_explanation row1 and fixed2 = fixed_explanation row2 in
let more = match fixed1, fixed2 with
| Some _, _ -> rm1
| Some _, Some _ -> if rm2.level < rm1.level then rm2 else rm1
| Some _, None -> rm1
| None, Some _ -> rm2
| None, None -> newty2 (min rm1.level rm2.level) (Tvar None)
in

3
typing/ctype.mli
View File

@ -207,6 +207,7 @@ val instance_poly:
?keep_names:bool ->
bool -> type_expr list -> type_expr -> type_expr list * type_expr
(* Take an instance of a type scheme containing free univars *)
val polyfy: Env.t -> type_expr -> type_expr list -> type_expr * bool
val instance_label:
bool -> label_description -> type_expr list * type_expr * type_expr
(* Same, for a label *)
@ -265,7 +266,7 @@ val matches: Env.t -> type_expr -> type_expr -> bool
(* Same as [moregeneral false], implemented using the two above
functions and backtracking. Ignore levels *)
val reify_univars : Types.type_expr -> Types.type_expr
val reify_univars : Env.t -> Types.type_expr -> Types.type_expr
(* Replaces all the variables of a type by a univar. *)
type class_match_failure =

4
typing/mtype.ml
View File

@ -240,11 +240,11 @@ let enrich_typedecl env p id decl =
decl
else
let orig_ty =
Ctype.reify_univars
Ctype.reify_univars env
(Btype.newgenty(Tconstr(p, orig_decl.type_params, ref Mnil)))
in
let new_ty =
Ctype.reify_univars
Ctype.reify_univars env
(Btype.newgenty(Tconstr(Pident id, decl.type_params, ref Mnil)))
in
let env = Env.add_type ~check:false id decl env in

104
typing/typecore.ml
View File

@ -2154,28 +2154,24 @@ let rec list_labels_aux env visited ls ty_fun =
let list_labels env ty =
wrap_trace_gadt_instances env (list_labels_aux env [] []) ty
(* Check that all univars are safe in a type *)
let check_univars env expans kind exp ty_expected vars =
if expans && maybe_expansive exp then
lower_contravariant env exp.exp_type;
(* need to expand twice? cf. Ctype.unify2 *)
let vars = List.map (expand_head env) vars in
let vars = List.map (expand_head env) vars in
let vars' =
List.filter
(fun t ->
let t = repr t in
generalize t;
match t.desc with
Tvar name when t.level = generic_level ->
set_type_desc t (Tunivar name); true
| _ -> false)
vars in
if List.length vars = List.length vars' then () else
let ty = newgenty (Tpoly(repr exp.exp_type, vars'))
and ty_expected = repr ty_expected in
raise (Error (exp.exp_loc, env,
Less_general(kind, [Unification_trace.diff ty ty_expected])))
(* Check that all univars are safe in a type. Both exp.exp_type and
ty_expected should already be generalized. *)
let check_univars env kind exp ty_expected vars =
let ty, complete = polyfy env exp.exp_type vars in
let ty_expected = instance ty_expected in
if not complete then
raise (Error (exp.exp_loc, env,
Less_general(kind, [Unification_trace.diff ty ty_expected])));
try
unify env ty ty_expected
with Unify trace ->
raise(Error(exp.exp_loc, env, Expr_type_clash(trace, None, None)))
let generalize_and_check_univars env kind exp ty_expected vars =
generalize exp.exp_type;
generalize ty_expected;
List.iter generalize vars;
check_univars env kind exp ty_expected vars
let check_partial_application statement exp =
let rec f delay =
@ -3366,7 +3362,7 @@ and type_expect_
end;
let exp = type_expect env sbody (mk_expected ty'') in
end_def ();
check_univars env false "method" exp ty_expected vars;
generalize_and_check_univars env "method" exp ty_expected vars;
{ exp with exp_type = instance ty }
| Tvar _ ->
let exp = type_exp env sbody in
@ -3961,8 +3957,13 @@ and type_label_exp create env loc ty_expected
let arg = type_argument env sarg ty_arg (instance ty_arg) in
end_def ();
try
check_univars env (vars <> []) "field value" arg label.lbl_arg vars;
arg
if (vars = []) then arg
else begin
if maybe_expansive arg then
lower_contravariant env arg.exp_type;
generalize_and_check_univars env "field value" arg label.lbl_arg vars;
{arg with exp_type = instance arg.exp_type}
end
with exn when maybe_expansive arg -> try
(* Try to retype without propagating ty_arg, cf PR#4862 *)
Option.iter Btype.backtrack snap;
@ -3970,13 +3971,16 @@ and type_label_exp create env loc ty_expected
let arg = type_exp env sarg in
end_def ();
lower_contravariant env arg.exp_type;
unify_exp env arg ty_arg;
check_univars env false "field value" arg label.lbl_arg vars;
arg
begin_def ();
let arg = {arg with exp_type = instance arg.exp_type} in
unify_exp env arg (instance ty_arg);
end_def ();
generalize_and_check_univars env "field value" arg label.lbl_arg vars;
{arg with exp_type = instance arg.exp_type}
with Error (_, _, Less_general _) as e -> raise e
| _ -> raise exn (* In case of failure return the first error *)
in
(lid, label, {arg with exp_type = instance arg.exp_type})
(lid, label, arg)
and type_argument ?explanation ?recarg env sarg ty_expected' ty_expected =
(* ty_expected' may be generic *)
@ -4764,7 +4768,6 @@ and type_let
if is_recursive then current_slot := slot;
match pat.pat_type.desc with
| Tpoly (ty, tl) ->
begin_def ();
if !Clflags.principal then begin_def ();
let vars, ty' = instance_poly ~keep_names:true true tl ty in
if !Clflags.principal then begin
@ -4775,12 +4778,13 @@ and type_let
Builtin_attributes.warning_scope pvb_attributes
(fun () -> type_expect exp_env sexp (mk_expected ty'))
in
end_def ();
check_univars env true "definition" exp pat.pat_type vars;
{exp with exp_type = instance exp.exp_type}
exp, Some vars
| _ ->
Builtin_attributes.warning_scope pvb_attributes (fun () ->
type_expect exp_env sexp (mk_expected pat.pat_type)))
let exp =
Builtin_attributes.warning_scope pvb_attributes
(fun () -> type_expect exp_env sexp (mk_expected pat.pat_type))
in
exp, None)
spat_sexp_list pat_slot_list in
current_slot := None;
if is_recursive && not !rec_needed then begin
@ -4800,26 +4804,36 @@ and type_let
)
)
pat_list
(List.map2 (fun (attrs, _) e -> attrs, e) spatl exp_list);
(List.map2 (fun (attrs, _) (e, _) -> attrs, e) spatl exp_list);
let pvs = List.map (fun pv -> { pv with pv_type = instance pv.pv_type}) pvs in
end_def();
List.iter2
(fun pat exp ->
(fun pat (exp, _) ->
if maybe_expansive exp then
lower_contravariant env pat.pat_type)
pat_list exp_list;
iter_pattern_variables_type generalize pvs;
(* We also generalize expressions that are not bound to a variable.
This does not matter in general, but those types are shown by the
interactive toplevel, for example: {[
let _ = Array.get;;
- : 'a array -> int -> 'a = <fun>
]} *)
List.iter (fun exp -> generalize exp.exp_type) exp_list;
List.iter2
(fun pat (exp, vars) ->
match vars with
| None ->
(* We generalize expressions even if they are not bound to a variable
and do not have an expliclit polymorphic type annotation. This is
not needed in general, however those types may be shown by the
interactive toplevel, for example:
{[
let _ = Array.get;;
- : 'a array -> int -> 'a = <fun>
]}
so we do it anyway. *)
generalize exp.exp_type
| Some vars ->
generalize_and_check_univars env "definition" exp pat.pat_type vars)
pat_list exp_list;
let l = List.combine pat_list exp_list in
let l =
List.map2
(fun (p, e) pvb ->
(fun (p, (e, _)) pvb ->
{vb_pat=p; vb_expr=e; vb_attributes=pvb.pvb_attributes;
vb_loc=pvb.pvb_loc;
})