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

A type for unification traces #2047

Merged

Conversation

Projects
None yet
4 participants
@Octachron
Copy link
Contributor

commented Sep 14, 2018

This PR proposes to create an explicit type for the unification trace.
Currently, this trace is encoded as a (type_expr * type_expr) list which
can exist in three modes:

  • a simple mode where an element is represented as a pair of type_expr (actual, expected)
  • an expanded mode where an element of the list represents a pair (short_representation, expanded_representation) for one type, and the whole type difference is encoded as two elements of the list:
    (short_actual, expanded_actual) :: (short_expected, expanded_expected) :: _
  • a degenerate mode where some elements have been expanded twice, thus both the expected and actual type are represented by a quadruplet:
    (short, expanded) :: (expanded, expanded_expanded) :: _ .
    The trace filtering in Printtyp removes most of those degenerate elements, but it sometimes fails on complex object types.

Moreover, some unification errors, like scope escapes, are not naturally representable as a difference of two types. In this case, unification functions resort to some artificial encodings into a difference of type expressions. Then the function Printtyp.mismatch try to recover the root cause behind a given unification trace, and may fail.

This PR proposes to define an explicit type for the unification trace.
With this type, the expanded or not status of type differences are tracked elements by elements, removing the possibility of double expansions.
Similarly, some specific errors are given their own variants and are directly tracked in the trace:

  • scope escape errors,
  • recursive occurrences of type variables,
  • tag mismatches for polymorphic variants
  • incompatible fields in object types

Simplifying the encoding for those errors may also help to give better contextual information in error messages (for instance for MPR#7565).

@gasche
Copy link
Member

left a comment

I started a review, it looks nice overall and interesting.

cc @trefis, @Armael and @garrigue.

| Incompatible_fields {name;diff} ->
Incompatible_fields { name; diff = switch_diff diff}
| x -> x
let switch x = List.map switch_elt x

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

To me permutation is swap, not switch (switch is rather a negation, turning on something that was off or conversely).

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

Indeed, swap sounds better.

type variant =
| No_intersection
| No_tags of position * (Asttypes.label * row_field) list
| Incompatible_types_for of string

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

Why does Incompatible_types_for carry only a string, while Incompatible_fields below also has a difference for the field types?

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

Mostly because I have an use case in mind for the type expressions in Incompatible_fields: adding an intermediary suberror message focused on the method. For instance,

In method m, type 'a. 'a -> 'a is not compatible with 'a -> 'a

which would be quite useful for a new version of #1212 .

Contrarily, Incompatible_types_for (I should add for_tag) is an final element that is only used to explain a previous difference between the actual and expected types.

let map f = List.map (map_elt f)


(* Convert [Simple x] to [f x x] and [Expanded(x,y)] to [f x y]*)

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

The documentation does not match the use of an option type below.

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

It was indeed out-of-sync.


let map_elt f = function
| Diff x -> Diff (map_diff f x)
| Escape Equation x -> Escape (Equation(f x))

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

I'm not sure why Escape Equation x parses correctly without parentheses.

This comment has been minimized.

Copy link
@trefis

trefis Sep 17, 2018

Contributor

Because there's no way (Escape Equation) x makes sense in a pattern context. And this is pretty remote from the concern of the PR.

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

I simplified this piece of exotic syntax.


exception Unify of t

let scope_escape x = Unify[Escape (Equation (short x))]

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

I find the idea of using a single-element eqution to represent this kind of escape a bit surprising, but maybe it's justified -- then maybe a comment at the declaration site of desc or Equation would help?

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

The name may be problematic: this error represents an ambivalent type becoming ambiguous due to escaping the scope of its equation. Maybe Ambiguous or Ambiguous_outside would be a better name?

| Tunivar _ ->
if TypeSet.mem t family then raise Occur
| Tunivar u ->
if TypeSet.mem t family then (univ := u; raise Occur)

This comment has been minimized.

Copy link
@gasche

gasche Sep 17, 2018

Member

Is it possible to have Occur carry an informative payload for all use sites? (Or is it exposed outside the module, or has no payload in some cases?). Or would using a let exception Occur_univ of .. be nice here?

This comment has been minimized.

Copy link
@Octachron

Octachron Sep 17, 2018

Author Contributor

Occur is currently shared with the code for detecting recursive type expressions. Decoupling the two seems fine.

@Octachron Octachron force-pushed the Octachron:a_precise_type_for_unification_traces branch from 9ca79b7 to fd6c2c4 Sep 21, 2018

@gasche
Copy link
Member

left a comment

Apologies for letting this one sleep for too long. I had another look at the PR just now, but there is not much I could do (in limited time) than look at the testsuite and find .reference files harder to read than expect-style tests.

This looks like nice work, but I would need much more time to review the ctype.ml changes to a reasonable degree of confidence, which won't happen this month. Maybe some others could have a look? cc @garrigue, @lpw25 and @trefis.

(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

This comment has been minimized.

Copy link
@gasche

gasche Oct 7, 2018

Member

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?

This comment has been minimized.

Copy link
@Octachron

Octachron Oct 7, 2018

Author Contributor

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.

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

This comment has been minimized.

Copy link
@gasche

gasche Oct 7, 2018

Member

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.

This comment has been minimized.

Copy link
@Octachron

Octachron Oct 7, 2018

Author Contributor

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.

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

This comment has been minimized.

Copy link
@gasche

gasche Oct 7, 2018

Member

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).

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

This comment has been minimized.

Copy link
@gasche

gasche Oct 7, 2018

Member

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

@trefis

This comment has been minimized.

Copy link
Contributor

commented Oct 7, 2018

I've been planning to having a look at this but it probably won't happy before a week or two.

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Oct 7, 2018

I will try to convert the problematic tests to expect tests shortly. Part of the problem is that this PR mainly affects edge cases where the error messages were already confused.

@trefis
Copy link
Contributor

left a comment

I had a first look, and it mostly looks OK.

I left a few comments here and there, but here are the things that should be addressed before approval/merging:

  1. rebasing
  2. the printing of some errors looks weird / broken (with Error: on its own line, and the error message on the line below)
  3. the cleanup looks unfinished: there are still some cases related to object where we interpret the "diff" trace after the fact instead of building a sensible one.
  4. some of the "helper" functions in the Unification_trace module have a weird taste. flatten in particular. I'll need to have another look at it to understand why (whether) it's needed.

On a more positive note: this PR is a must-have, and points (3) and (4) should not be considered blockers, the work can be continued later (although I'd like to have an answer for 3, even if no work needs to happen now)

@@ -116,8 +116,7 @@ let f (type a b) (x : (a, b) eq) =
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
Error:

This comment has been minimized.

Copy link
@trefis

trefis Oct 16, 2018

Contributor

The blank line doesn't look right

This comment has been minimized.

Copy link
@trefis

trefis Oct 16, 2018

Contributor

Actually, I think that the error message I would like to see here is:

Error: This pattern matches values of type (a, b) eq * b list
       This instance of b is ambiguous:
       it would escape the scope of its equation
@@ -2429,7 +2489,7 @@ let rec unify (env:Env.t ref) t1 t2 =
reset_trace_gadt_instances reset_tracing;
with Unify trace ->
reset_trace_gadt_instances reset_tracing;
raise (Unify ((t1, t2)::trace))
raise( Unify (Trace.diff t1 t2 :: trace) )

This comment has been minimized.

Copy link
@trefis

trefis Oct 16, 2018

Contributor

weird spacing

@@ -1842,37 +1803,68 @@ let explanation env unif t3 t4 : (Format.formatter -> unit) option =
fprintf ppf
"@,@[The %s object type has an abstract row, it cannot be closed@]"
(if t4.desc = Tnil then "first" else "second"))

This comment has been minimized.

Copy link
@trefis

trefis Oct 16, 2018

Contributor

Why are the three cases above still here?
Would their disappearance require cleaning up typeclass.ml?

This comment has been minimized.

Copy link
@Octachron

Octachron Oct 16, 2018

Author Contributor

It seems that emitting the right information in Ctype was enough.

| Trace.(Diff { got; expected }) ->
let t1 = trees_of_type_expansion got in
let t2 = trees_of_type_expansion expected in
[{Trace.got=t1; expected = t2 }]

This comment has been minimized.

Copy link
@trefis

trefis Oct 16, 2018

Contributor

Isn't this:

| Trace.Diff diff ->
  [ Trace.map_diff trees_of_type_expansion diff ]

?

This comment has been minimized.

Copy link
@Octachron

Octachron Oct 16, 2018

Author Contributor

Indeed.

@Octachron Octachron force-pushed the Octachron:a_precise_type_for_unification_traces branch from fd6c2c4 to 07a98ab Oct 16, 2018

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Oct 16, 2018

The point 1 and 2 should be fixed. For the point 2, I added an escape context in the trace.
For the point 3, I shall take a second look.
For the last point, part of the unnaturalness of flatten is that it serves as a bridge between Ctype where types may have been expanded or not, and Printtyp which expects every types to have been expanded. One alternative might be to do the translation before reaching Printtyp.

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Oct 16, 2018

I have a better look at the object error messages and integrated them more closely into the unification trace in b709dd9 . ( I have also added a simpler test for the abstract row error message that was only exercised through GADTs before).

@trefis

This comment has been minimized.

Copy link
Contributor

commented Oct 17, 2018

For the point 2, I added an escape context in the trace.

Thanks! The result looks nice for the error messages it applies to. And I can now confidently reply to #2108 (comment): yes, the error messages will look nice!

The implementation is a bit disappointing though: you're adding a new trace element constructor Escape_context, which is only used in one escape situation, and then you assert false when you encounter it in the explanation function.
I'd be happier if we could add the context directly in the Escape constructor. The hope would be to also use it in the other escape situations, e.g. https://github.com/ocaml/ocaml/pull/2047/files#diff-703e6d9fb61bc0f542a577ae13e22834R19 (I wish I could add some "unversal variable escape" examples to the list but these error messages look scary and I don't really want to get near them right now).

@trefis

This comment has been minimized.

Copy link
Contributor

commented Oct 17, 2018

I have a better look at the object error messages and integrated them more closely into the unification trace in b709dd9

Nice!

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Oct 17, 2018

Attaching the context to the Escape constructor also makes the printing function feels more regular, thus here is the commit b53a654 .

@trefis

trefis approved these changes Oct 17, 2018

Copy link
Contributor

left a comment

This looks good enough to go in for me at this point.
I think there's still some margin of improvement, but:

  • it already is much better than the current state of affairs
  • it seems fine to improve further in separate PRs (potentially from separate authors even!)

I don't know what @Octachron's view on the matter is, so I'll let him decide whether to merge now or keep working on it for while (in which case, feel free to ping me for additional review).

@Octachron Octachron force-pushed the Octachron:a_precise_type_for_unification_traces branch from b53a654 to e828147 Oct 17, 2018

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Oct 17, 2018

I think merging in this state is fine, I have cleaned up the history a bit (to remove some back-and-forth) and added change entry. I will merge once CI passes.

@Octachron Octachron merged commit b9dea2a into ocaml:trunk Oct 17, 2018

1 check passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details

Armael added a commit that referenced this pull request Nov 6, 2018

unification trace: properly track universal variable renaming (#2135)
* unification trace: track univar renaming

This PR fixes an inconsistency introduced by #2047 : when an universal type variable was renamed in Printtyp, the explanation part of the error message kept the original name leading to potentially confusing error messages.

This PR fixes this inconsistency by keeping the whole type expression in the explanation part of the unification message instead of just its original name (and add a test for this behavior).
@lpw25

This comment has been minimized.

Copy link
Contributor

commented Feb 26, 2019

I think this broke the error message for closing a self type. In 4.07.1 you get:

# let is_empty (x : < >) = ();;
val is_empty : <  > -> unit = <fun>
# class c = object (self) method private foo = is_empty self end;;
Characters 54-58:
  class c = object (self) method private foo = is_empty self end;;
                                                        ^^^^
Error: This expression has type < .. > but an expression was expected of type
         <  >
       Self type cannot be unified with a closed object type

whereas with 4.08 you get:

# let is_empty (x : < >) = ();;
val is_empty : <  > -> unit = <fun>
# class c = object (self) method private foo = is_empty self end;;
Line 1, characters 54-58:
1 | class c = object (self) method private foo = is_empty self end;;
                                                          ^^^^
Error: This expression has type < .. > but an expression was expected of type
         <  >
       The second object type has no method *dummy method*

Which leaks the internal "dummy method" nonsense. There appears to have been no test for this case which is probably why it was missed.

@gasche

This comment has been minimized.

Copy link
Member

commented Feb 26, 2019

@lpw25 could you create a Mantis issue to track the regression?

@Octachron

This comment has been minimized.

Copy link
Contributor Author

commented Feb 26, 2019

@lpw25 , you are right: I forgot to test for dummy methods before raising a Missing_field error. I have a fix, and shall send a PR shortly after some reverification.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.