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.

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

Fix #11101 by making occur ty ty succeed #11109

Merged
merged 3 commits into from
Mar 15, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
4 changes: 4 additions & 0 deletions Changes
Original file line number Diff line number Diff line change
Expand Up @@ -491,6 +491,10 @@ OCaml 4.14.0
- #11025, #11036: Do not pass -no-pie to the C compiler on musl/arm64
(omni, Kate Deplaix and Antonio Nuno Monteiro, review by Xavier Leroy)

- #11101, #11109: A recursive type constraint fails on 4.14
(Jacques Garrigue, report and review by Florian Angeletti)


OCaml 4.13 maintenance branch
-----------------------------

Expand Down
34 changes: 34 additions & 0 deletions testsuite/tests/typing-misc/constraints.ml
Original file line number Diff line number Diff line change
Expand Up @@ -295,3 +295,37 @@ Error: The class constraints are not consistent.
Type int * int is not compatible with type float * float
Type int is not compatible with type float
|}]

(* #11101 *)
type ('node,'self) extension = < node: 'node; self: 'self > as 'self
type 'ext node = < > constraint 'ext = ('ext node, 'self) extension;;
[%%expect{|
type ('node, 'a) extension = 'a constraint 'a = < node : 'node; self : 'a >
type 'a node = < >
constraint 'a = ('a node, < node : 'a node; self : 'b > as 'b) extension
|}, Principal{|
type ('node, 'a) extension = < node : 'node; self : 'b > as 'b
constraint 'a = < node : 'node; self : 'a >
type 'a node = < >
constraint 'a = ('a node, < node : 'a node; self : 'b > as 'b) extension
|}]

class type ['node] extension =
object ('self)
method clone : 'self
method node : 'node
end
type 'ext node = < >
constraint 'ext = 'ext node #extension ;;
[%%expect{|
class type ['node] extension =
object ('a) method clone : 'a method node : 'node end
type 'a node = < > constraint 'a = < clone : 'a; node : 'a node; .. >
|}]

module Raise: sig val default_extension: 'a node extension as 'a end = struct
let default_extension = failwith "Default_extension failure"
end;;
[%%expect{|
Exception: Failure "Default_extension failure".
|}]
5 changes: 3 additions & 2 deletions typing/ctype.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1772,7 +1772,8 @@ let occur env ty0 ty =
try
while
type_changed := false;
occur_rec env allow_recursive TypeSet.empty ty0 ty;
if not (eq_type ty0 ty) then
occur_rec env allow_recursive TypeSet.empty ty0 ty;
!type_changed
do () (* prerr_endline "changed" *) done;
merge type_changed old
Expand Down Expand Up @@ -2702,7 +2703,7 @@ and unify3 env t1 t1' t2 t2' =
| _ ->
begin match !umode with
| Expression ->
occur_for Unify !env t1' t2';
occur_for Unify !env t1' t2;
link_type t1' t2
| Pattern ->
add_type_equality t1' t2'
Expand Down
2 changes: 2 additions & 0 deletions typing/types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -720,6 +720,7 @@ let log_type ty =
let link_type ty ty' =
let ty = repr ty in
let ty' = repr ty' in
if ty == ty' then () else begin
log_type ty;
let desc = ty.desc in
Transient_expr.set_desc ty (Tlink ty');
Expand All @@ -736,6 +737,7 @@ let link_type ty ty' =
| None, None -> ()
end
| _ -> ()
end
(* ; assert (check_memorized_abbrevs ()) *)
(* ; check_expans [] ty' *)
(* TODO: consider eliminating set_type_desc, replacing it with link types *)
Expand Down