Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Make Tsubst directly retain two arguments, instead of nesting a Ttuple #10174

Merged
merged 17 commits into from
Feb 1, 2021
Merged

Make Tsubst directly retain two arguments, instead of nesting a Ttuple #10174

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
458882b
Add an optional argument to Tsubst; avoid abusive uses of Ttuple to l…
t6s Jan 27, 2021
d5c2c03
comment on the arguments of Tsubst; adapt printtyp to the new Tsubst
t6s Jan 27, 2021
2f8c0a8
fix fold_type_expr to handle the second component of Tsubst
t6s Jan 28, 2021
02bb2da
properly ignore Tsubst cases in mark_loops and tree_of_typexp
t6s Jan 28, 2021
2e1e69d
partially revert the previous commit because filter_params is using T…
t6s Jan 28, 2021
fa18e1a
assert false when calling fold_type_expr on Tsubst
garrigue Jan 28, 2021
4882078
deref Tlink in fold_type_expr
garrigue Jan 28, 2021
1b86a27
fix the handling of Tsubst and comments
t6s Jan 28, 2021
0662c26
remove Btype.norm_univar
garrigue Jan 29, 2021
b8553b7
assert false for Tsubst outside of copying functions
garrigue Jan 29, 2021
fa7f26d
one missing assertion
garrigue Jan 29, 2021
1c0e65e
rather group
garrigue Jan 29, 2021
856f9cc
Tsubst in ocamldoc
garrigue Jan 29, 2021
9b9d88e
add change log and assertion that Tsubst doesn't occur in copy_sep
garrigue Jan 31, 2021
7bbfd63
update comment
garrigue Jan 31, 2021
6a10cc3
depend
garrigue Feb 1, 2021
c7d2ffa
check-typo
garrigue Feb 1, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
19 changes: 15 additions & 4 deletions .depend
View file
Open in desktop
Expand Up @@ -6284,6 +6284,8 @@ toplevel/trace.cmi : \
typing/path.cmi \
parsing/longident.cmi \
typing/env.cmi
toplevel/byte/topdirs.cmi : \
parsing/longident.cmi
toplevel/byte/topeval.cmo : \
utils/warnings.cmi \
typing/types.cmi \
Expand Down Expand Up @@ -6363,11 +6365,20 @@ toplevel/byte/topeval.cmi : \
typing/path.cmi \
parsing/parsetree.cmi \
typing/env.cmi
toplevel/byte/toploop.cmi : \
utils/warnings.cmi \
typing/types.cmi \
typing/path.cmi \
parsing/parsetree.cmi \
typing/outcometree.cmi \
parsing/longident.cmi \
parsing/location.cmi \
typing/env.cmi
toplevel/byte/topmain.cmo : \
toplevel/byte/trace.cmi \
toplevel/toploop.cmi \
toplevel/byte/toploop.cmi \
toplevel/byte/topeval.cmi \
toplevel/topdirs.cmi \
toplevel/byte/topdirs.cmi \
toplevel/topcommon.cmi \
typing/printtyp.cmi \
typing/path.cmi \
Expand All @@ -6382,9 +6393,9 @@ toplevel/byte/topmain.cmo : \
toplevel/byte/topmain.cmi
toplevel/byte/topmain.cmx : \
toplevel/byte/trace.cmx \
toplevel/toploop.cmx \
toplevel/byte/toploop.cmi \
toplevel/byte/topeval.cmx \
toplevel/topdirs.cmx \
toplevel/byte/topdirs.cmi \
toplevel/topcommon.cmx \
typing/printtyp.cmx \
typing/path.cmx \
Expand Down
8 changes: 7 additions & 1 deletion Changes
View file
Open in desktop
Expand Up @@ -8,6 +8,12 @@ Working version
'let* x = x in ...' and 'let%ext x = x in ...' respectively.
(Stephen Dolan, review by Gabriel Scherer)

### Type system:

- #10174: Make Tsubst more robust by avoiding strange workarounds
(Takafumi Saikawa and Jacques Garrigue, review by Gabriel Scherer and
Florian Angeletti)

### Runtime system:

- #9284: Add -config option to display the configuration of ocamlrun on stdout,
Expand Down Expand Up @@ -69,7 +75,7 @@ Working version
with respect to closing.
(Xavier Leroy, report by Jacques-Henri Jourdan, review by Guillaume
Munch-Maccagnoni, Gabriel Scherer, Jacques-Henri Jourdan)

- #10139: Remove confusing navigation bar from stdlib documentation.
Removes the 'Up', 'Previous' and 'Next' links from the top of each standard
library module's documentation.
Expand Down
4 changes: 2 additions & 2 deletions ocamldoc/odoc_misc.ml
View file
Open in desktop
Expand Up @@ -506,8 +506,8 @@ let remove_option typ =
| Types.Tnil
| Types.Tvariant _
| Types.Tpackage _ -> t
| Types.Tlink t2
| Types.Tsubst t2 -> iter t2.Types.desc
| Types.Tlink t2 -> iter t2.Types.desc
| Types.Tsubst _ -> assert false
in
Types.Private_type_expr.create (iter typ.Types.desc)
~level:typ.Types.level ~scope:typ.Types.scope ~id:typ.Types.id
9 changes: 5 additions & 4 deletions ocamldoc/odoc_str.ml
View file
Open in desktop
Expand Up @@ -32,23 +32,24 @@ let string_of_variance t (co,cn) =
let rec is_arrow_type t =
match t.Types.desc with
Types.Tarrow _ -> true
| Types.Tlink t2 | Types.Tsubst t2 -> is_arrow_type t2
| Types.Tlink t2 -> is_arrow_type t2
| Types.Ttuple _
| Types.Tconstr _
| Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
| Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
| Types.Tsubst _ -> assert false

let raw_string_of_type_list sep type_list =
let buf = Buffer.create 256 in
let fmt = Format.formatter_of_buffer buf in
let rec need_parent t =
match t.Types.desc with
Types.Tarrow _ | Types.Ttuple _ -> true
| Types.Tlink t2 | Types.Tsubst t2 -> need_parent t2
| Types.Tconstr _ ->
false
| Types.Tlink t2 -> need_parent t2
| Types.Tconstr _
| Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
| Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
| Types.Tsubst _ -> assert false
in
let print_one_type variance t =
Printtyp.mark_loops t;
Expand Down
10 changes: 5 additions & 5 deletions ocamldoc/odoc_value.ml
View file
Open in desktop
Expand Up @@ -76,8 +76,6 @@ let parameter_list_from_arrows typ =
Types.Tarrow (l, t1, t2, _) ->
(l, t1) :: (iter t2)
| Types.Tlink texp
| Types.Tsubst texp ->
iter texp
| Types.Tpoly (texp, _) -> iter texp
| Types.Tvar _
| Types.Ttuple _
Expand All @@ -89,6 +87,8 @@ let parameter_list_from_arrows typ =
| Types.Tpackage _
| Types.Tvariant _ ->
[]
| Types.Tsubst _ ->
assert false
in
iter typ

Expand All @@ -114,10 +114,10 @@ let dummy_parameter_list typ =
{ Odoc_parameter.sn_name = normal_name label ;
Odoc_parameter.sn_type = t ;
Odoc_parameter.sn_text = None }
| Types.Tlink t2
| Types.Tsubst t2 ->
| Types.Tlink t2 ->
(iter (label, t2))

| Types.Tsubst _ ->
assert false
| _ ->
Odoc_parameter.Simple_name
{ Odoc_parameter.sn_name = normal_name label ;
Expand Down
8 changes: 8 additions & 0 deletions testsuite/tests/typing-misc/filter_params.ml
View file
Open in desktop
@@ -0,0 +1,8 @@
(* TEST
* expect
*)

type ('a, 'b) t constraint 'a = 'b
[%%expect{|
type ('b, 'a) t constraint 'a = 'b
|}]
4 changes: 1 addition & 3 deletions toplevel/genprintval.ml
View file
Open in desktop
Expand Up @@ -473,9 +473,7 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct
find row.row_fields
| Tobject (_, _) ->
Oval_stuff "<obj>"
| Tsubst ty ->
tree_of_val (depth - 1) obj ty
| Tfield(_, _, _, _) | Tnil | Tlink _ ->
| Tsubst _ | Tfield(_, _, _, _) | Tnil | Tlink _ ->
fatal_error "Printval.outval_of_value"
| Tpoly (ty, _) ->
tree_of_val (depth - 1) obj ty
Expand Down
17 changes: 4 additions & 13 deletions typing/btype.ml
View file
Open in desktop
Expand Up @@ -300,7 +300,7 @@ let rec fold_row f init row =
let iter_row f row =
fold_row (fun () v -> f v) () row

let fold_type_expr f init ty =
let rec fold_type_expr f init ty =
match ty.desc with
Tvar _ -> init
| Tarrow (_, ty1, ty2, _) ->
Expand All @@ -320,8 +320,8 @@ let fold_type_expr f init ty =
let result = f init ty1 in
f result ty2
| Tnil -> init
| Tlink ty -> f init ty
| Tsubst ty -> f init ty
| Tlink ty -> fold_type_expr f init ty
| Tsubst _ -> assert false
| Tunivar _ -> init
| Tpoly (ty, tyl) ->
let result = f init ty in
Expand Down Expand Up @@ -487,15 +487,6 @@ let rec copy_kind = function
let copy_commu c =
if commu_repr c = Cok then Cok else Clink (ref Cunknown)

(* Since univars may be used as row variables, we need to do some
encoding during substitution *)
let rec norm_univar ty =
match ty.desc with
Tunivar _ | Tsubst _ -> ty
| Tlink ty -> norm_univar ty
| Ttuple (ty :: _) -> norm_univar ty
| _ -> assert false

let rec copy_type_desc ?(keep_names=false) f = function
Tvar _ as ty -> if keep_names then ty else Tvar None
| Tarrow (p, ty1, ty2, c)-> Tarrow (p, f ty1, f ty2, copy_commu c)
Expand All @@ -512,7 +503,7 @@ let rec copy_type_desc ?(keep_names=false) f = function
| Tsubst _ -> assert false
| Tunivar _ as ty -> ty (* always keep the name *)
| Tpoly (ty, tyl) ->
let tyl = List.map (fun x -> norm_univar (f x)) tyl in
let tyl = List.map f tyl in
Tpoly (f ty, tyl)
| Tpackage (p, n, l) -> Tpackage (p, n, List.map f l)

Expand Down
22 changes: 13 additions & 9 deletions typing/ctype.ml
View file
Open in desktop
Expand Up @@ -1134,7 +1134,7 @@ let rec copy ?partial ?keep_names scope ty =
let copy = copy ?partial ?keep_names scope in
let ty = repr ty in
match ty.desc with
Tsubst ty -> ty
Tsubst (ty, _) -> ty
gasche marked this conversation as resolved.
Show resolved Hide resolved
| _ ->
if ty.level <> generic_level && partial = None then ty else
(* We only forget types that are non generic and do not contain
Expand All @@ -1153,7 +1153,7 @@ let rec copy ?partial ?keep_names scope ty =
For_copy.save_desc scope ty desc;
let t = newvar() in (* Stub *)
set_scope t ty.scope;
Private_type_expr.set_desc ty (Tsubst t);
Private_type_expr.set_desc ty (Tsubst (t, None));
Private_type_expr.set_desc t
begin match desc with
| Tconstr (p, tl, _) ->
Expand Down Expand Up @@ -1182,17 +1182,17 @@ let rec copy ?partial ?keep_names scope ty =
(* We must substitute in a subtle way *)
(* Tsubst takes a tuple containing the row var and the variant *)
begin match more.desc with
Tsubst {desc = Ttuple [_;ty2]} ->
Tsubst (_, Some ty2) ->
(* This variant type has been already copied *)
Private_type_expr.set_desc ty (Tsubst ty2);
Private_type_expr.set_desc ty (Tsubst (ty2, None));
(* avoid Tlink in the new type *)
Tlink ty2
| _ ->
(* If the row variable is not generic, we must keep it *)
let keep = more.level <> generic_level && partial = None in
let more' =
match more.desc with
Tsubst ty -> ty
Tsubst (ty, None) -> ty
(* TODO: is this case possible?
possibly an interaction with (copy more) below? *)
| Tconstr _ | Tnil ->
Expand Down Expand Up @@ -1235,7 +1235,7 @@ let rec copy ?partial ?keep_names scope ty =
in
(* Register new type first for recursion *)
Private_type_expr.set_desc
more (Tsubst(newgenty(Ttuple[more';t])));
more (Tsubst (more', Some t));
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

All code paths aware of the this tuple encoding (aka the pattern matching above and one in Subst) never use more'. Since all other users would erroneously interpret this encoding as a real tuple, it seems to me that rather than the product type_expr * type_expr option, the non-encoded argument of Tsubst is a sum.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we were to just encode the current behavior of the algorithm in this type, you are correct.
However, it seems cleaner that the meaning of Tsubst be regular, i.e. its first argument is always a copy of the original node. Then the second argument is some special information used by the algorithm, here a copy of the enclosing Tvariant node.
We can ensure that we do not depart from the current behavior of the algorithm by checking that this second argument is always None when we use the first one. We will add such assertions.

(* Return a new copy *)
Tvariant (copy_row copy true row keep more')
end
Expand Down Expand Up @@ -1449,8 +1449,10 @@ let rec copy_sep cleanup_scope fixed free bound visited ty =
match ty.desc with
Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ | Tpackage _ ->
(ty,(t,bound)) :: visited
| Tvar _ | Tfield _ | Tnil | Tpoly _ | Tunivar _ | Tlink _ | Tsubst _ ->
| Tvar _ | Tfield _ | Tnil | Tpoly _ | Tunivar _ ->
visited
| Tlink _ | Tsubst _ ->
assert false
in
let copy_rec = copy_sep cleanup_scope fixed free bound visited in
Private_type_expr.set_desc t
Expand All @@ -1477,6 +1479,7 @@ let rec copy_sep cleanup_scope fixed free bound visited ty =
end

let instance_poly' cleanup_scope ~keep_names fixed univars sch =
(* In order to compute univars below, [sch] schould not contain [Tsubst] *)
let univars = List.map repr univars in
let copy_var ty =
match ty.desc with
Expand All @@ -1498,14 +1501,15 @@ let instance_poly ?(keep_names=false) fixed univars sch =

let instance_label fixed lbl =
For_copy.with_scope (fun scope ->
let ty_res = copy scope lbl.lbl_res in
let vars, ty_arg =
match repr lbl.lbl_arg with
{desc = Tpoly (ty, tl)} ->
instance_poly' scope ~keep_names:false fixed tl ty
| _ ->
[], copy scope lbl.lbl_arg
in
(* call [copy] after [instance_poly] to avoid introducing [Tsubst] *)
let ty_res = copy scope lbl.lbl_res in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the record, I don't really understand what is going on here. I suppose there is a problem when lbl_res and lbl_args share some parts of the type, but it's not clear who might introduce Tsubst. (I suppose instance_poly can introduce Tsubst nodes, and copy normalizes them away?)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the other way round: copy_sep (first phase of instance_poly) does not introduce (and should not see) Tsubst's, while copy does. Could add an assertion in copy_sep.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could add many assertions in copy_sep, I don't think this PR is the one where we want to start doing that.

Copy link
Contributor

@garrigue garrigue Jan 31, 2021 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We are already adding assertions about Tsubst everywhere, so why not in copy_sep.
Now all functions that call iter_type_expr are checking this, but copy_sep is using copy_type_desc instead, which explicitly allows Tsubst, hence the need for a specific assertion.
I do not pretend that this alone will make copy_sep self-explanatory :-)

(vars, ty_arg, ty_res)
)

Expand Down Expand Up @@ -2058,7 +2062,7 @@ let polyfy env ty vars =
| Tvar name when ty.level = generic_level ->
For_copy.save_desc scope ty ty.desc;
let t = newty (Tunivar name) in
Private_type_expr.set_desc ty (Tsubst t);
Private_type_expr.set_desc ty (Tsubst (t, None));
Some t
| _ -> None
in
Expand Down
17 changes: 12 additions & 5 deletions typing/printtyp.ml
View file
Open in desktop
Expand Up @@ -518,7 +518,9 @@ and raw_type_desc ppf = function
raw_type t1 raw_type t2
| Tnil -> fprintf ppf "Tnil"
| Tlink t -> fprintf ppf "@[<1>Tlink@,%a@]" raw_type t
| Tsubst t -> fprintf ppf "@[<1>Tsubst@,%a@]" raw_type t
| Tsubst (t, None) -> fprintf ppf "@[<1>Tsubst@,(%a,None)@]" raw_type t
| Tsubst (t, Some t') ->
fprintf ppf "@[<1>Tsubst@,(%a,@ Some%a)@]" raw_type t raw_type t'
| Tunivar name -> fprintf ppf "Tunivar %a" print_name name
| Tpoly (t, tl) ->
fprintf ppf "@[<hov1>Tpoly(@,%a,@,%a)@]"
Expand Down Expand Up @@ -915,7 +917,7 @@ let rec mark_loops_rec visited ty =
| Tfield(_, _, _, ty2) ->
mark_loops_rec visited ty2
| Tnil -> ()
| Tsubst ty -> mark_loops_rec visited ty
| Tsubst _ -> () (* we do not print arguments *)
Octachron marked this conversation as resolved.
Show resolved Hide resolved
| Tlink _ -> fatal_error "Printtyp.mark_loops_rec (2)"
| Tpoly (ty, tyl) ->
List.iter (fun t -> add_alias t) tyl;
Expand Down Expand Up @@ -1022,8 +1024,9 @@ let rec tree_of_typexp sch ty =
tree_of_typobject sch fi !nm
| Tnil | Tfield _ ->
tree_of_typobject sch ty None
| Tsubst ty ->
tree_of_typexp sch ty
| Tsubst _ ->
(* This case should only happen when debugging the compiler *)
Otyp_stuff "<Tsubst>"
| Tlink _ ->
fatal_error "Printtyp.tree_of_typexp"
| Tpoly (ty, []) ->
Expand Down Expand Up @@ -1162,8 +1165,12 @@ let filter_params tyl =
List.fold_left
(fun tyl ty ->
let ty = repr ty in
if List.memq ty tyl then Btype.newgenty (Tsubst ty) :: tyl
if List.memq ty tyl then Btype.newgenty (Ttuple [ty]) :: tyl
else ty :: tyl)
(* Two parameters might be identical due to a constraint but we need to
print them differently in order to make the output syntactically valid.
We use [Ttuple [ty]] because it is printed as [ty]. *)
(* Replacing fold_left by fold_right does not work! *)
[] tyl
in List.rev params

Expand Down
15 changes: 7 additions & 8 deletions typing/subst.ml
View file
Open in desktop
Expand Up @@ -155,12 +155,12 @@ let rec typexp copy_scope s ty =
else newty2 ty.level desc
in
For_copy.save_desc copy_scope ty desc;
Private_type_expr.set_desc ty (Tsubst ty');
Private_type_expr.set_desc ty (Tsubst (ty', None));
(* TODO: move this line to btype.ml
there is a similar problem also in ctype.ml *)
ty'
else ty
| Tsubst ty ->
| Tsubst (ty, _) ->
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we assert = None here?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This case actually failed at one test (poly.ml). I am now looking into the bug..

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is needed when the row variable of a polymorphic variant is Tunivar.

ty
| Tfield (m, k, _t1, _t2) when not s.for_saving && m = dummy_method
&& field_kind_repr k <> Fabsent && (repr ty).level < generic_level ->
Expand All @@ -179,8 +179,7 @@ let rec typexp copy_scope s ty =
(* Make a stub *)
let ty' = if s.for_saving then newpersty (Tvar None) else newgenvar () in
Private_type_expr.set_scope ty' ty.scope;
(* TODO: figure out why not use set_scope *)
Private_type_expr.set_desc ty (Tsubst ty');
Private_type_expr.set_desc ty (Tsubst (ty', None));
Private_type_expr.set_desc ty'
begin if has_fixed_row then
match tm.desc with (* PR#7348 *)
Expand Down Expand Up @@ -216,9 +215,9 @@ let rec typexp copy_scope s ty =
(* We must substitute in a subtle way *)
(* Tsubst takes a tuple containing the row var and the variant *)
begin match more.desc with
Tsubst {desc = Ttuple [_;ty2]} ->
Tsubst (_, Some ty2) ->
(* This variant type has been already copied *)
Private_type_expr.set_desc ty (Tsubst ty2);
Private_type_expr.set_desc ty (Tsubst (ty2, None));
(* avoid Tlink in the new type *)
Tlink ty2
| _ ->
Expand All @@ -228,7 +227,7 @@ let rec typexp copy_scope s ty =
(* Various cases for the row variable *)
let more' =
match more.desc with
Tsubst ty -> ty
Tsubst (ty, None) -> ty
| Tconstr _ | Tnil -> typexp copy_scope s more
| Tunivar _ | Tvar _ ->
For_copy.save_desc copy_scope more more.desc;
Expand All @@ -238,7 +237,7 @@ let rec typexp copy_scope s ty =
in
(* Register new type first for recursion *)
Private_type_expr.set_desc more
(Tsubst(newgenty(Ttuple[more';ty'])));
(Tsubst (more', Some ty'));
(* TODO: check if more' can be eliminated *)
(* Return a new copy *)
let row =
Expand Down