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

A type for unification traces #2047

Merged
merged 4 commits into from
Oct 17, 2018
Merged

A type for unification traces #2047

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3de4098
a type for unification traces
Octachron Sep 10, 2018
233d666
Add context for unification errors
Octachron Oct 16, 2018
ca043e9
unification trace: reify object error earlier
Octachron Oct 16, 2018
e828147
unification trace: update Changes
Octachron Oct 17, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions .depend
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -323,7 +323,7 @@ typing/printtyp.cmx : utils/warnings.cmx typing/types.cmx \
typing/printtyp.cmi
typing/printtyp.cmi : typing/types.cmi typing/path.cmi \
typing/outcometree.cmi parsing/longident.cmi parsing/location.cmi \
typing/ident.cmi typing/env.cmi parsing/asttypes.cmi
typing/ident.cmi typing/env.cmi typing/ctype.cmi parsing/asttypes.cmi
typing/printtyped.cmo : typing/types.cmi typing/typedtree.cmi \
parsing/printast.cmi typing/path.cmi parsing/parsetree.cmi utils/misc.cmi \
parsing/longident.cmi parsing/location.cmi typing/ident.cmi \
Expand Down Expand Up @@ -405,7 +405,8 @@ typing/typecore.cmx : utils/warnings.cmx typing/typetexp.cmx \
parsing/ast_helper.cmx typing/annot.cmi typing/typecore.cmi
typing/typecore.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
typing/ident.cmi typing/env.cmi parsing/asttypes.cmi typing/annot.cmi
typing/ident.cmi typing/env.cmi typing/ctype.cmi parsing/asttypes.cmi \
typing/annot.cmi
typing/typedecl.cmo : utils/warnings.cmi typing/typetexp.cmi \
typing/types.cmi typing/typedtree.cmi typing/subst.cmi \
typing/printtyp.cmi typing/primitive.cmi typing/predef.cmi \
Expand All @@ -426,7 +427,7 @@ typing/typedecl.cmx : utils/warnings.cmx typing/typetexp.cmx \
parsing/ast_iterator.cmx parsing/ast_helper.cmx typing/typedecl.cmi
typing/typedecl.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
typing/includecore.cmi typing/ident.cmi typing/env.cmi \
typing/includecore.cmi typing/ident.cmi typing/env.cmi typing/ctype.cmi \
parsing/asttypes.cmi
typing/typedtree.cmo : typing/types.cmi typing/primitive.cmi typing/path.cmi \
parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
Expand Down Expand Up @@ -511,7 +512,8 @@ typing/typetexp.cmx : typing/types.cmx typing/typedtree.cmx \
parsing/ast_helper.cmx typing/typetexp.cmi
typing/typetexp.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
typing/includemod.cmi typing/env.cmi parsing/asttypes.cmi
typing/includemod.cmi typing/env.cmi typing/ctype.cmi \
parsing/asttypes.cmi
typing/untypeast.cmo : typing/typedtree.cmi typing/path.cmi \
parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
parsing/location.cmi typing/ident.cmi typing/env.cmi parsing/asttypes.cmi \
Expand Down
3 changes: 3 additions & 0 deletions Changes
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -424,6 +424,9 @@ Working version
for parser testing. See parsing/HACKING.adoc.
(Gabriel Scherer, review by Nicolás Ojeda Bär)

- GPR#2047: a new type for unification traces
(Florian Angeletti, review by Thomas Refis and Gabriel Scherer)

- GPR#2055: Add [Linearize.Lprologue].
(Mark Shinwell, review by Pierre Chambart)

Expand Down
6 changes: 0 additions & 6 deletions testsuite/tests/typing-gadts/ambiguity.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,6 @@ Line 3, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -132,7 +131,6 @@ Line 3, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -147,7 +145,6 @@ Line 3, characters 4-29:
| Refl, [(_ : b) | (_ : a)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -162,7 +159,6 @@ Line 4, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -177,7 +173,6 @@ Line 4, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -192,7 +187,6 @@ Line 4, characters 4-29:
| Refl, [(_ : b) | (_ : a)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
2 changes: 0 additions & 2 deletions testsuite/tests/typing-gadts/pr7618.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ Line 4, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand All @@ -37,7 +36,6 @@ Line 3, characters 4-29:
| Refl, [(_ : a) | (_ : b)] -> []
^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This pattern matches values of type (a, b) eq * b list
but a pattern was expected which matches values of type 'a
This instance of b is ambiguous:
it would escape the scope of its equation
|}]
Expand Down
29 changes: 29 additions & 0 deletions testsuite/tests/typing-misc/exotic_unifications.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
(* TEST
* expect
*)

class virtual t = object method virtual x: float end

class x = object(self: <x:int; ..>)
inherit t
end
[%%expect {|
class virtual t : object method virtual x : float end
Line 4, characters 16-17:
inherit t
^
Error: The method x has type int but is expected to have type float
Type int is not compatible with type float
|}]

let x =
let module M = struct module type t = sig end end in
(module struct end: M.t)
[%%expect {|
Line 3, characters 2-26:
(module struct end: M.t)
^^^^^^^^^^^^^^^^^^^^^^^^
Error: This expression has type (module M.t)
but an expression was expected of type 'a
The module type M.t would escape its scope
|}]
1 change: 1 addition & 0 deletions testsuite/tests/typing-misc/ocamltests
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
constraints.ml
disambiguate_principality.ml
exotic_unifications.ml
inside_out.ml
labels.ml
occur_check.ml
Expand Down
27 changes: 12 additions & 15 deletions testsuite/tests/typing-objects-bugs/pr4018_bad.compilers.reference
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,26 +16,23 @@ Error: This type entity = < destroy_subject : id subject; entity_id : id >
'a entity_container =
< add_entity : (< destroy_subject : < add_observer : 'a
entity_container ->
'e;
.. >;
'f;
.. >
as 'e;
.. >
as 'd) ->
'e;
'f;
notify : 'd -> id -> unit >
Type < destroy_subject : id subject; entity_id : id >
is not compatible with type
entity = < destroy_subject : id subject; entity_id : id >
Type entity = < destroy_subject : id subject; entity_id : id >
is not compatible with type < destroy_subject : 'e; .. > as 'd
Type
< add_observer : (id subject, id) observer -> unit;
notify_observers : id -> unit >
is not compatible with type
id subject =
< add_observer : (id subject, id) observer -> unit;
notify_observers : id -> unit >
Type < add_entity : 'd -> 'e; notify : 'd -> id -> unit >
notify_observers : id -> unit >
is not compatible with type
< add_observer : 'a entity_container -> 'f; .. > as 'e
Type (id subject, id) observer = < notify : id subject -> id -> unit >
is not compatible with type
'a entity_container =
< add_entity : 'd -> 'e; notify : 'd -> id -> unit >
Type < notify : id subject -> id -> unit > is not compatible with type
(id subject, id) observer = < notify : id subject -> id -> unit >
Types for method add_entity are incompatible
< add_entity : 'd -> 'f; notify : 'd -> id -> unit >
The first object type has no method add_entity
Copy link
Member

Choose a reason for hiding this comment

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

I find the error messages here fairly hard to review. Before the patch, the message is very strange (it starts by saying that two visually identical types are incompatibe). After the patch, some of the strageness is removed, but the error message remains unreadable and incomprehensible. I guess this is unavoidable (without substantially more work) and I am not suggesting/requesting any additional improvement to the error-message logic, but maybe this could be converted to an expect-test, to at least make the test cases more readable?

Copy link
Member Author

Choose a reason for hiding this comment

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

This original error message here is indeed extremely confusing because it lost track of which types were the actual and the expected due to a double expansion of the trace. In the first two suberrors, the error messages is in fact comparing the actual type with itself then the expected type with itself.

2 changes: 0 additions & 2 deletions testsuite/tests/typing-objects-bugs/pr4824a_bad.compilers.reference
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,3 @@ Error: Signature mismatch:
does not match
class c : 'a -> object val x : 'b end
The instance variable x has type 'a but is expected to have type 'b
This instance of 'b is ambiguous:
it would escape the scope of its equation
3 changes: 3 additions & 0 deletions testsuite/tests/typing-objects/Exemples.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,7 @@ Error: Type
point circle =
< center : point; move : int -> unit; set_center : point -> unit >
Type point is not a subtype of color_point
The first object type has no method color
|}];; (* Fail *)
fun x -> (x : color_point color_circle :> point circle);;
[%%expect{|
Expand All @@ -247,6 +248,7 @@ Error: Type
point circle =
< center : point; move : int -> unit; set_center : point -> unit >
Type point is not a subtype of color_point
The first object type has no method color
|}];;

class printable_point y = object (s)
Expand Down Expand Up @@ -544,6 +546,7 @@ Error: Type
is not a subtype of
int_comparable2 =
< cmp : int_comparable2 -> int; set_x : int -> unit; x : int >
The first object type has no method set_x
|}];; (* Fail : 'a comp2 is not a subtype *)
(new sorted_list ())#add c2;;
[%%expect{|
Expand Down
26 changes: 26 additions & 0 deletions testsuite/tests/typing-objects/abstract_rows.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
(* TEST
* expect
*)
type u = <x:int>
type t = private <u; ..>

let f (x:t) (y:u) = x = y;;
[%%expect{|
type u = < x : int >
type t = private < x : int; .. >
Line 4, characters 24-25:
let f (x:t) (y:u) = x = y;;
^
Error: This expression has type u but an expression was expected of type t
The second object type has an abstract row, it cannot be closed
|}]


let g (x:u) (y:t) = x = y;;
[%%expect{|
Line 1, characters 24-25:
let g (x:u) (y:t) = x = y;;
^
Error: This expression has type t but an expression was expected of type u
The first object type has an abstract row, it cannot be closed
|}]
1 change: 1 addition & 0 deletions testsuite/tests/typing-objects/ocamltests
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
abstract_rows.ml
dummy.ml
errors.ml
Exemples.ml
Expand Down
11 changes: 6 additions & 5 deletions testsuite/tests/typing-poly-bugs/pr5673_bad.compilers.reference
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,10 @@ Error: This expression has type
refer1 = < poly : 'a 'b 'c. ('b, 'c) #Classdef.cl2 as 'a >
but an expression was expected of type
refer2 = < poly : 'd 'b 'c. ('b, 'c) #Classdef.cl2 as 'd >
Type
('b, 'c) Classdef.cl1 =
< m : 'b -> 'c -> int; raise_trouble : int -> 'b >
Type ('b, 'c, ('b, 'c) Classdef.cl1) Classdef.cl0 = < >
is not compatible with type
< m : 'b -> 'c -> int; raise_trouble : int -> 'b >
The type variable 'e occurs inside 'e
('b0, 'c0, ('b0, 'c0) Classdef.cl1) Classdef.cl0
Type < m : 'b -> 'c -> int; .. > is not compatible with type
('b, 'c) Classdef.cl1 =
< m : 'b -> 'c -> int; raise_trouble : int -> 'b >
The universal variable 'b would escape its scope
Copy link
Member

Choose a reason for hiding this comment

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

Again, it is very hard to make sense of this error message (refer1 and refer2 seems identical modulo 'a -> 'd renaming, and it is unclear to me why raise_trouble makes 'b escape its scope), but I guess there is little to be done about it. Maybe expect-tests would be slightly less confusing.

Copy link
Member Author

Choose a reason for hiding this comment

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

It helps to refer to the mantis ticket, which explains that this is a problem with the escape check for universal type variable. In other words, the error is wrong, but at least the error message now points to the source of the problem.

2 changes: 1 addition & 1 deletion testsuite/tests/typing-poly/poly.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1098,7 +1098,7 @@ Line 2, characters 3-4:
Error: This expression has type < m : 'a. 'a * < m : 'a * 'b > > as 'b
but an expression was expected of type
< m : 'a. 'a * (< m : 'a * < m : 'c. 'c * 'd > > as 'd) >
Types for method m are incompatible
The universal variable 'a would escape its scope
Copy link
Member

Choose a reason for hiding this comment

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

Could we maybe have an [%%expect] block right after the ;;, which is where the error arises if I understand correctly (on fun), and a different block for the type declarations that follow and let f?

The error message doesn't make much sense (before or after the change) to a human reader, but I understand why this is an error: if you unfold the recursive < ... 'foo ...> as 'foo types into infinite types, you can see that the two types are incompatible in their level of polymorphism (the same variable 'a in the second type will occur infinitely many times, while it only occurs twice in the first one).

|}];;

fun (x : <m : 'a. 'a * ('a * <m : 'a. 'a * 'foo> as 'foo)>) ->
Expand Down
2 changes: 1 addition & 1 deletion testsuite/tests/typing-polyvariants-bugs-2/pr3918c.compilers.reference
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
File "pr3918c.ml", line 24, characters 11-12:
Error: This expression has type 'b Pr3918b.vlist = 'a
but an expression was expected of type 'b Pr3918b.vlist
The type variable 'a occurs inside 'a
The type variable 'a occurs inside ('d * 'c) Pr3918a.voption as 'c
Copy link
Member

Choose a reason for hiding this comment

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

(Again an expect-style test would help here.)

Loading