Generate full error traces during module inclusion

[antalsz]

Introduction

This PR produces more detailed error messages during various kinds of module inclusion, taking advantage of the new structured error trace generation from #10170. Previously, these errors were “shallow”, ending as soon as there was an incompatibility; this patch makes them “deep”, reporting the reasons for those problems. For example, consider the following module:

module M : sig
  val x : bool * int
end = struct
  let x = false , "not an int"
end

This now produces the following error:

Error: Signature mismatch:
       Modules do not match:
         sig val x : bool * string end
       is not included in
         sig val x : bool * int end
       Values do not match:
         val x : bool * string
       is not included in
         val x : bool * int
       The type bool * string is not compatible with the type bool * int
       Type string is not compatible with type int

The last two bolded lines are new in this patch. Previously, the error message stopped two lines earlier, omitting the key detail that the reason there is an error is specifically that string is not equal to int.

This change brings module errors in line with ordinary type errors; indeed, the new, bolded part of the module inclusion error corresponds directly to the error trace produced for ordinary type errors. For example, in

let y = false, "still not an int" in
(y : bool * int)

the resulting error is

Error: This expression has type bool * string
       but an expression was expected of type bool * int
       Type string is not compatible with type int 

(These examples were also the example in #10170’s “Eventual goals” section, and the module M above now lives in the test suite as the first example in testsuite/tests/typing-misc/deep.ml.)

These improved error messages are generated for both moregen and type equality, and show up for every kind of module inclusion error: not just values with a different type in the signature, but constructors with different arguments, types with different parameters, classes with different methods, primitives with different names, and so on.

Code changes

This PR makes the following large-scale changes to the code:

• The Errortrace.t type, which wrapped up the three kinds of error traces into a single GADT, is now no longer passed around directly. Instead, Errortrace exposes three new types, one for each kind of error: unification_error, equality_error, and moregen_error. Each of these record types contains a corresponding trace (t) in the field named trace; the equality_error also contains a substitution (subst). All types that contain explanations of errors contain these _error types (or the sum type comparison_error that wraps an equality_error or a moregen_error) instead of raw traces; traces are only handled directly if they’re being built (as in typing/ctype.ml) or consumed (as in typing/printtyp.ml). This also meant changing a number of variable names from trace or tr to err. The advantage of this change is that we can bundle the extra information we need into equality_error, and also that we can tell the three kinds of errors apart more directly.

• The environment (Env.t) is propagated into the printing functions from outside, rather than maintaining duplicate copies of the environment alongside various errors.

• There is new text for printing out new kinds of moregen and equality errors that were previously not printed, and the moregen and equality errors themselves have their traces printed. Some text was changed slightly (constructor mismatches went from “is not compatible with” to “is not the same as”).

• A few new tests were added; these tests confirm that we print out longer traces for inclusion errors and catch some specific error cases that didn’t previously have tests.

• Some code in toplevel/topdirs.ml was changed to use a local exception type instead of Ctype.Unify (not directly related to the printing, but part of the global exception inspection that was necessary for some of the other changes).

The changes are structured into two commits: first, a commit that adds the new tests; and second, a commit that makes the actual code changes and updates all the necessary tests.

Detailed, file-by-file changes

This section documents the changes I made to every file, since this PR touches so many of them; it is not required reading, but hopefully helps review. There is nothing after this section in this PR, so if you don’t want to read the gory details, you can stop now.

The key files to look at are, in roughly descending order, typing/includecore.ml, typing/ctype.ml, and typing/errortrace.mli, as well as, to a lesser extent, their .mli (or .ml) files. The test file which contains the greatest number of changed error messages is testsuite/tests/typing-modules/inclusion_errors.ml; all of the test files except for the four with new tests from the first commit just contain improved error messages.

• .depend (modified):

  Inessential changes, autogenerated.

• Changes (modified):

  The proposed change description (currently lacking “reviewed-by” information).

• testsuite/tests/printing-types/disambiguation.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-extensions/extensions.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-extensions/open_types.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-gadts/ambiguity.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-gadts/pr7160.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-gadts/pr7378.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/deep.ml (new):

  New tests that generate type errors within more complex types during module inclusion (e.g., the initial example in this PR), showing that we generate full traces for module inclusion.

• testsuite/tests/typing-misc/enrich_typedecl.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/pr6416.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/pr6634.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/pr7668_bad.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/records.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-misc/variant.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/Test.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/applicative_functor_type.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/extension_constructors_errors_test.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/functors.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/inclusion_errors.ml (modified):

  New test cases and better error messages in test output. Since I was improving module inclusion errors, this is the file with by far the highest number of improved errors, as well as with errors for the most different inclusion cases. I also added three new tests that show how inclusion of private polymorphic variant types can fail; these don’t reflect new behavior, just new error messages.

• testsuite/tests/typing-modules/module_type_substitution.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/nondep_private_abbrev.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/pr10399.ml (new):

  This is a new test showing the new error traces, copied from issue Error message missing information about type inclusion #10399 by @jctis; the old error for this case was reported as a bug, and so I have copied the test case here so that we can see the improvement.

• testsuite/tests/typing-modules/pr6394.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/pr7818.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/pr7851.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/records_errors_test.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-modules/variants_errors_test.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-objects-bugs/pr3968_bad.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-objects/Tests.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-poly/poly.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-polyvariants-bugs/pr7817_bad.ml (modified):

  Better error messages in test output.

• testsuite/tests/typing-private/private.compilers.principal.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-private/private.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-short-paths/short-paths.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-sigsubst/test_locations.compilers.reference (modified):

  Better error messages in test output.

• testsuite/tests/typing-unboxed/test.ml (modified):

  New test cases and better error messages in test output. This file contains a number of errors where primitives’ definitions and signatures are incompatible; I added 14 more test cases for cases that were already caught but now have more detailed error messages. (One of these test cases, Good16, tests a case where we do not raise a primitive-mismatch error). I also had to renumber the various BadN modules, which contributes to some noise in the diff.

• testsuite/tests/typing-warnings/pr6587.ml (modified):

  Better error messages in test output.

• toplevel/topdirs.ml (modified):

  This file raised Ctype.Unify with an empty trace to record issues when trying to install a printing function; I replaced this with a custom exception, Bad_printing_function. The original use of Ctype.Unify was understandable, as unification was in fact invoked; however, instead of conjuring empty unification traces, I caught and replaced the exceptions coming out of Ctype.unify.

• typing/ctype.ml (modified):

  The biggest structural change to this file is that the exceptions Unify, Equality, and Moregen were each split into two pieces: Unify_trace, Equality_trace and Moregen_trace, which like the old exceptions contain raw traces (i.e., Errortrace.t) but are not exported; and Unify, Equality, and Moregen, which are exported and contain the new _error types from Errortrace (unification_error, equality_error, and moregen_error). This split is between “internal” and “external” errors: the _trace errors are used internally in unification, equality, and moregen, and the public-facing entry points rewrap these into the _error-based exceptions. The raise_for family of functions (raise_trace_for, raise_unexplained_for, occur_for, …) raise _trace exceptions now; these are caught and converted to the top-level exceptions in unify, unify_var, equal, and moregeneral. Within this file, no part of the implementation of unification, equality, or moregen ever catches the top-level Unify, Equality, and Moregen exceptions, with one exception: subst is implemented in terms of a forward reference to unify_var (now stored in a reference named unify_var' instead of unify'), and so it catches Unify. The other functions that have to be aware of raising Unify are the specialized unification functions filter_arrow and filter_method, which can raise Unify and the latter of which can rewrap a Unify_trace into Unify.

  When transforming an Equality_trace exception into an Equality exception, we also have to include the substitution; because this is built mutably, this involves saving the substitution reference before performing the equality comparison and dereferencing it on failure. This is most clearly done in equal, but is also done in other functions later in the file that invoke eqtype and catch Equality_trace.

  In addition to these changes, we apply the new _error types everywhere: the Subtype and Matches_failure exceptions use them instead of traces; the class_match_failure type contains them instead of traces; and because the class_match_failure type contains comparison_error in particular, we can also drop the class_match_failure_trace_type type entirely.

  There were also some functionality changes to some functions in this file: we generate more precise traces in moregen_row and eqtype_row. These functions matched on the presences of corresponding constructors in two polymorphic variants, and raised exceptions on failure; however, the exceptions were being caught and rewrapped in the wrong places. This only became visible now when we were printing out the traces, so we pushed the try … with … blocks that wrapped the trace with Variant (Incompatible_types_for l) inwards and used more specific errors in other cases, including the new Presence_not_guaranteed_for error. In moregen_row, we also had to roll back a link_type for better printing.

• typing/ctype.mli (modified):

  Errors in this file now use the new error types from Errortrace instead of raw traces:

  • The Unify, Equality, and Moregen exceptions now contain the new whole-error types Errortrace.unification_error,Errortrace.equality_error, and Errortrace.moregen_error, respectively, instead of just traces.
  • Similarly, the Subtype and Matches_failure exceptions contain Errortrace.unification_error instead of unification traces.
  • The class_match_failure error type now contains Errortrace.equality_error, Errortrace.moregen_error, and Errortrace.comparison_error instead of error traces; the use of Errortrace.comparison_error also allows us to drop the class_match_failure_trace_type type entirely.

• typing/errortrace.ml (modified):

  The changes here are the same as those to typing/errortrace.mli, which see: the additions of (1) new top-level error types and their attendant support; and (2) a new error case for equality and moregen. Because these are public-facing changes, I have documented them in typing/errortrace.mli.

• typing/errortrace.mli (modified):

  There were two major changes in this file: the additions of (1) new top-level error types and their attendant support; and (2) a new error case for equality and moregen.

  For the first change, I added three new types, one for each kind of error that contains a trace (i.e., a 'variant Errortrace.t for some 'variant): unification_error, equality_error, and moregen_error. The traces from Maintain more structural information in type-checking errors #10170 are still the core of the errors; however, since they only have a 2-way GADT distinction, and more importantly since the type equality case requires extra information (see below), we bundle them into three “top-level” error types. The distinction is that 'variety Errortrace.t values are currently being either built or processed, whereas *_error values are whole, complete error messages.

  All three of these types contain a trace, as the record field trace; equality_error also contains a substitution, in order to report error messages with more type variable names that more accurately reflect the original source.

  To support these new error types, I also added comparison_error, which wraps both equality_error and moregen_error the way that the comparison t trace type used to; and I added swap_unification_error, which just lifts swap_trace to the new unification_error type.

  The second change is the addition of the Presence_not_guaranteed_for error case, which shows up when the presence variables of polymorphic variants disagree between the structure and the signature in an incompatible way; see ctype.ml for where it’s raised.

• typing/includeclass.ml (modified):

  The printing code was updated to use the new equality_error and moregen_error types, including renaming local variables named trace to err.

• typing/includecore.ml (modified):

  This file contains the bulk of the new text for the new error messages. This means new printers for primitive_mismatch, value_mismatch, private_variant_mismatch, and private_object_mismatch; updating printing text elsewhere; and calls to these new functions, particularly from report_type_mismatch (which merged with report_type_mismatch0). The error reporting functions were also updated to propagate the environment (Env.t) in from outside, rather than pulling it from the mismatch values.

  This file also contains updates to the “mismatch” types that record error reasons, which come in three varieties: first, the Env.ts were dropped, since the desired environment is propagated in from the printing functions and should not be duplicated here; second, the direct Errortrace.ts were replaced with Errortrace.moregen_error or Errortrace.equality_error, as appropriate; and third, the constructor Openness of private_variant_mismatch was renamed to Only_outer_closed to more accurately reflect its meaning. These changes also required updating later parts of the file to handle the new Ctype.Equality error and build these new mismatch values with just the equality_error rather than with the trace and the available environment.

• typing/includecore.mli (modified):

  This file contains the interface-side versions of the above changes to typing/includecore.ml. First, the mismatch types were updated, as described above, to (1) remove Env.ts; (2) replace Errortrace.ts with either Errortrace.moregen_error or Errortrace.equality_error; and (3) rename the Openness constructor of private_variant_mismatch to Only_outer_closed. Second, the two exposed error-reporting functions, report_type_mismatch and report_extension_constructor_mismatch, gained an Env.t parameter. And third, we now expose report_value_mismatch as well.

• typing/includemod.ml (modified):

  This file now propagates moregen traces raised when a value has the wrong signature. These errors are captured by the Value_descriptions error case (in the Error.core_sigitem_symptom type); this constructor now carries an Includecore.value_mismatch value, which itself contains an Errortrace.moregen_error or other appropriate error information. When created, this mismatch information is included in the constructor

• typing/includemod.mli (modified):

  This file contains just the update to the Value_descriptions constructor from typing/includemode.ml (not the code to fill it); this constructor, which reflects disagreements between a value’s type and its type in the signature, now contains an explanation for the error, an Includecore.value_mismatch value.

• typing/includemod_errorprinter.ml (modified):

  This file now prints out the details of the Includemod.Error.Value_descriptions error, which reflects a disagreement between a value’s type and the type for it in the signature, using the new function Includecore.report_value_mismatch. It also propagates the environment in from the outside, rather than requiring every error to have a duplicate copy.

• typing/printtyp.ml (modified):

  I updated the name-printing machinery in this file by (1) wrapping it into a local module called Names, and (2) adding support for applying a substitution before looking up names. The first change allowed the mutable state to be encapsulated together, and required exposing a couple new functions to support existing direct queries to the mutable names list or similar; it also required updating the names of many function calls later in the file to refer to Names.foo instead of foo. The second change allowed for superior printing of equality errors, and is how we leverage the subst of equality_errors; before trying to get the name of a type, we first apply the substitution, which can produce a better name for the user. By applying these substitutions lazily rather than eagerly, we don’t overgenerate names and produce stray names such as 'a0 without a corresponding 'a.

  I also updated the printing code. I provided a new error message for the new Presence_not_guaranteed_for error message (see typing/errortrace.mli). I also gave the generic error and report_error functions a new subst parameter to support the substitutions coming out of equality, which uses the new Names.add_subst function. Finally, I updated the error-reporting functions (report_unification_error, report_equality_error, report_moregen_error, and Subtype.report_error to take the the new error types instead of traces (i.e., to take Errortrace.unification_error, Errortrace.equality_error, and Errortrace.moregen_error). (This is also where report_equality_error gets its substitution from; no other error-reporting functions provide substitutions.) I also added a new report_comparison_error function to print out the new Errortrace.comparison_error sum type.

• typing/printtyp.mli (modified):

  The error-reporting functions (report_unification_error, report_equality_error, report_moregen_error, and Subtype.report_error) take the new error types instead of traces (i.e., to take Errortrace.unification_error, Errortrace.equality_error, and Errortrace.moregen_error). I also added report_comparison_error to print out the new Errortrace.comparison_error sum type.

• typing/typeclass.ml (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly. This also required refactoring the code in this file that used these errors to be aware of this. In particular, the code built these error explanations now uses the new Ctype.Unify (or Ctype.Subtype) error, which often just involved renaming a variable named trace (or tr) to err but not always.

• typing/typeclass.mli (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly.

• typing/typecore.ml (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly. This also required refactoring the code in this file that used these errors to be aware of this. In particular, the code built these error explanations now uses the new Ctype.Unify error, which often just involved renaming a variable named trace (or tr) to err but not always.

• typing/typecore.mli (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly.

• typing/typedecl.ml (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly. This also required refactoring the code in this file that used these errors to be aware of this. In particular, the code built these error explanations now uses the new Ctype.Unify error, which often just involved renaming a variable named trace (or tr) to err but not always.

  Additionally, some of the errors in this file now contain an Env.t, and the printing code in this file was also taught to propagate the environment more deeply. This supports the changes in Includecore that keep the environment coming in from this outer layer rather than maintaining duplicates.

  Finally, the local function suffix for generating the appropriate ordinal suffix for numbers – "st" for 1, 21, …; "nd" for 2, 22, …; "rd" for 3, 23, …; and "th" for everything else – was moved to utils/misc.ml and renamed ordinal_suffix so it could be used elsewhere.

• typing/typedecl.mli (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly. Some of them also now contain an Env.t for printing purposes that they did not before.

• typing/typetexp.ml (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly. This also required refactoring the code in this file that used these errors to be aware of this. In particular, the code built these error explanations now uses the new Ctype.Unify error, which often just involved renaming a variable named trace (or tr) to err but not always.

  Additionally, a call to Ctype.expand_head was formerly guarded by try … with …, but this function cannot throw, so the try … with … was removed.

• typing/typetexp.mli (modified):

  This file’s errors now use Errortrace.unification_error instead of carrying around a trace (i.e., an Errortrace.unification Errortrace.t) directly.

• utils/misc.ml (modified):

  Added the function ordinal_suffix for generating the appropriate ordinal suffix for numbers – "st" for 1, 21, …; "nd" for 2, 22, …; "rd" for 3, 23, …; and "th" for everything else. This function was originally a local function named suffix in typing/typedecl.ml.

• utils/misc.mli (modified):

  Added the function ordinal_suffix for generating the appropriate ordinal suffix for numbers – "st" for 1, 21, …; "nd" for 2, 22, …; "rd" for 3, 23, …; and "th" for everything else. This function was originally a local function named suffix in typing/typedecl.ml.

[Octachron]

The detection of weakly polymorphic type seems to be failing here?

[antalsz]

Good catch, thanks! There were a couple of issues with the detection of weakly polymorphic types: mostly the problem was that moregen (and match_class_types) weren't undoing some of the setup work they did in the error case, but we did also have to provide an argument controlling the printing of weak types for some other cases.

[Octachron]

At first glance, the printed type has changed. Do you have any comments on what is happening in this file?

[antalsz]

Yes – the new type is actually more general, so this patch is improving this error. To wit, observe that what is changing is the second argument to the outer `App: it was

([ `Abs of string * expr | `App of 'a * exp ] as 'b)

where 'a referred to the whole type and 'b was unused. Now, it is instead

([> `App of [ `Abs of string * 'a | `App of expr * expr ] * exp ] as 'a)

where 'a is bound locally. Recall from earlier in the input that expr is

type expr =
  [ `Abs of string * expr
  | `App of expr * expr
  ]

Thus, rather than requiring exactly `Abs and `App, the new error message has a type that only requires `App, and can contain more constructors; moreover, this new type allows the first argument to this `App to be less constrained; rather than requiring it to be the entire type ('a), it only mandates that the input `Abs contain a string * 'a.

(I wanted to come up with a nice inclusion example you could paste here, but because the code doesn't compile, I couldn't quite figure out how to do so.)

[gasche]

I had a couple drive-by comments from skimming the errortrace.mli changes, but nothing major:

• It's slightly weird that the Errortrace module now defines errors (maybe it's about errors after all and not just error traces). If the responsibilities of the module are growing, we should eventually thing of naming it Type_error with a Trace submodule, but I don't think the change is warranted just yet so I'm fine with the current proposal.
• Instead of three types foo_error, bar_error and foobar_error I wondered if it would make sense to have a GADT foo error, taking extra information in just one case. This makes it easy to define swap on all errors types, but on the other hand we don't need that.

[antalsz]

Thank you for the careful review, @Octachron! The small changes you suggested have all been taken care of, but your suggestions about handling trace expansion and your observation that weak types were not being properly detected required some more invasive changes.

The biggest change was to Errortrace, which had its types completely refactored. Previously, the central type in this module was 'variant Errortrace.t, the type of traces, which contained descs. A desc contained a type and, optionally, its expansion. However, actual expansion was only done at the end, after a trace containing Nones for all the expansions had been produced. This lead to unnecessary complexity in code that handled these optional types, and required being able to flatten them down. Instead, we now have two types:

• 'variant Errortrace.trace, which contains types (type_exprs); and
• 'variant Errortrace.error, which contains types and their expansions (Errortrace.expanded_types, a record containing two type_exprs).

(We also set up a similar split in Subtype.) These are both specializations of ('a, 'variant) Errortrace.t, which contains 'as. We then use this type to revamp the errors:

• Ctype’s internal exceptions, {Unify,Equality,Moregen}_trace, now contain _ traces.
• Errortrace’s error types, {unify,equality,moregen}_error, now contain _ errors.

By keeping a distinction between traces and errors, we get some benefits:

1. We can replace the old flatten code with simply Errortrace.map, and need it less.
2. We can use the types to separate the notion of “partial trace being built up” and “complete error trace”.
3. We can ensure that we never forget to perform expansion (indeed, we weren’t doing it in enough places previously), improving the error messages; we can explicitly decide not to expand, as is sometimes necessary, but we can never do so by accident.

The other major change was to our handling of printing weakly polymorphic types. In one place, we fixed a bug – two functions that were part of the moregen check were instantiating variables at generic_level - 1 that were not getting regeneralized in the error case. Besides that, we also had to expose the distinction between printing types (and not detecting weakly polymorphic types during printing) and printing schemes (and detecting weakly polymorphic types during printing), as the new error trace printing could reveal that distinction. This was previously controlled by a boolean argument (formerly called sch); we changed this to a variant, Printtyp.type_or_scheme, and propagated it further throughout the printing code (calling it mode). This change was invasive, but not particularly deep.

As a more minor change, we now detect the different kinds of privacy-exposing violations, and print bespoke error messages (was it a private record constructor that was revealed, or a private type abbreviation, or…). And of course, I addressed all of the other smaller review comments.

Finally, one last note: I updated testsuite/tests/typing-misc/deep.ml to replace ref with option, and rebased this change back into the very first commit. This is because these example are intended to be simple, and avoid any use of weak polymorphism even by accident; I call this out here because it is the only change to an existing commit.

Detailed, file-by-file changes

Since some of these changes touched a lot of code, I felt it behooved me to write up the file-by-file changes again. However, I won’t comment on the specifics of any of the test files unless we added new tests to them (in a new commit, f341e13, that has been rebased into the past, between the old “new tests” commit and the first content commit) or something else significant happened; they’re all improvements.

• .depend (modified):

  Inessential changes, autogenerated.

• Changes (modified):

  @Octachron, I added you as a reviewer.

• testsuite/tests/typing-misc/deep.ml (modified):

  This was rebased all the way in the first commit, to use option instead of ref; these examples are intended to be simple, and avoid any use of weak polymorphism even by accident.

• testsuite/tests/typing-gadts/return_type.ml (new):

  New tests of what goes wrong if we don’t give GADT constructors return types that are syntactically identical to the expected types. If we do too much expansion when printing error messages, this can produce inferior or nonsensical errors.

• testsuite/tests/typing-modules/extension_constructors_errors_test.ml (modified):

  A new test, exposing multiple private variant constructors at once, to validate the grammar of the resulting error message.

• testsuite/tests/typing-modules/inclusion_errors.ml (modified):

  One new test ensuring that variable unification happens correctly, and several new tests for various kinds of privacy violations.

• testsuite/tests/typing-objects/errors.ml (modified):

  A new test of what goes wrong when we fail to conform to the expected class type and have a polymorphic variable; this can go wrong if we do not handle weakly polymorphic variables correctly.

• toplevel/topdirs.ml (modified):

  Deleted some review comments.

• typing/ctype.ml (modified):

  I updated the {Unify,Equality,Moregen}_trace exceptions to use the new trace type, the Subtype exception to use Subtype.error, and Escape to use type_expr escape (so it is pre-expansion, not post-expansion). Relatedly, I exposed some new trace-expansion machinery, particularly for creating Diffs of expanded_types, and performed expansion in more places for better error messages. There was also some code churn from removing or adjusting some of the convenience functions in Errortrace for this new reality (e.g., the removal of Errortrace.diff). The matches function now exposes an argument controlling whether it performs expansion or just duplicates the input, as it is called in a place where expansion produces worse error messages.

  I also fixed a bug in the moregeneral checks where it was not correctly regeneralizing variables in the error case (breaking the detection of weakly polymorphic types), and moved generalize_class_type here from Typeclass.

• typing/ctype.mli (modified):

  Expansion-related updates: I updated the Subtype exception to use Subtype.error, and I updated Escape to use type_expr escape (so it is pre-expansion, not post-expansion). Relatedly, I expose expanded_diff and unexpanded_diff, for creating Errortrace.Diffs of Errortrace.expanded_types in other modules; and I provide matches with an argument controlling whether it performs expansion or just duplicates the input, as it is called in a place where expansion produces worse error messages.

  I also expose generalize_class_type from here after moving it from Typeclass.

• typing/errortrace.ml (modified):

  This file contains the core of the updates for expansion-aware error traces: replacing desc with expanded_type, splitting t into trace and error, and removing the old desc-based machinery like short, flatten, and diff. The changes here are smaller than might be expected, as most of the difference is at use sites.

• typing/errortrace.mli (modified):

  Most of the changes to errortrace.ml are visible here, as the change to expansion-aware error traces is very user-visible.

• typing/includeclass.ml (modified):

  Propagate the new weak type detection argument through the error printing; these errors are the reason this is a parameter, instead of varying with the variety of trace we’re dealing with.

• typing/includeclass.mli (modified):

  The interface side of typing/includeclass.ml – expose the new weak type detection argument to report_error.

• typing/includecore.ml (modified):

  This module is augmented with better detection for exposed private things, in that it now detects what sort of private thing was exposed (in the new privacy_mismatch type) and reports it appropriately. It also now specifies that the calls to Printtyp.report_{equality,moregen}_error are printing type schemes, to get the superior detection of weakly polymorphic type variables.

• typing/includecore.mli (modified):

  We now expose the new privacy_mismatch type mentioned above.

• typing/includemod_errorprinter.ml (modified):

  This file now has to specify how the class inclusion errors are to be printed; it specifies they are both to be printed as type schemes, triggering the weak type detection.

• typing/printtyp.ml (modified):

  This file was hit by both major updates.

  Firstly, its operations on expanded types had to change from operating on pairs of types to operating on Errortrace.expanded_types. This mostly meant updates to pattern matching and/or variable names, or similar such things.

  Secondly, it was the core of the updates for better detection of weakly polymorphic variables. The changes are essentially about introducing the new type_or_scheme variant, and plumbing it through as mode instead of the boolean sch (or changing constant booleans to the constructors of this new type); no behavior was changed during printing. The only change was that the ability to provide a type_or_scheme was exposed more broadly.

  (On a more minor note, we also updated the type of filter_trace to line up the trace_format and the trace it took, for better type checking.)

• typing/printtyp.mli (modified):

  This file exposes the new type_or_scheme variant for controlling if types are printed without or with detection of weakly polymorphic variables (i.e., if they are printed as types or as type schemes). The function tree_of_typexp, which formerly took a bool, now takes a type_or_scheme; we also provide this as an extra argument to type_expansion and report_{equality,moregen,comparison}_error. (Unification never needs to think about weakly polymorphic variables, so report_unification_error doesn’t take a new argument, and nor does Subtype.report_error.)

  This file also uses the new Errortrace.expanded_type type, instead of pairs of two type_exprs.

• typing/typeclass.ml (modified):

  I moved generalize_class_type to Ctype, and changed the formerly-boolean arguments to Printtyp.tree_of_typexp to elements of the new Printtyp.type_or_scheme variant.

• typing/typecore.ml (modified):

  This file now uses the new types from Errortrace: Subtype.error instead of Subtype.t, and expanded_type instead of pairs of type_exprs. This file also explicitly constructs traces, and so had to expand them, carefully choosing the expansion behavior when doing so.

• typing/typecore.mli (modified):

  This file now uses the new types from Errortrace: Subtype.error instead of Subtype.t, and expanded_type instead of pairs of type_exprs.

• typing/typedecl.ml (modified):

  This file has to carefully avoid expansion when constructing traces or when calling Ctype.matches, as the expansion will otherwise take us past constraints and produce nonsensical error messages. We also update the first argument in the various calls to Printtyp.tree_of_typexp from false to the new Type constructor of Printtyp.type_or_scheme.

• typing/typetexp.ml (modified):

  I changed the formerly-boolean arguments to Printtyp.tree_of_typexp to elements of the new Printtyp.type_or_scheme variant.

[Octachron]

I have a handful of remarks and I still need to reread the PR in details, but overall the global structure seems good.

[Octachron]

Is this test not redundant?

[antalsz]

It's a bit redundant, but it's a regression test for #10399, so I want to include it.

[Octachron]

I agree that specializing this exception is probably a good idea (Self todo: check that this is not an issue in utop).

[Octachron]

Review note: this aligns the forward declaration name with the function name.

[Octachron]

The name of the universal variable does not seem compatible with the previous part of the error message.

[antalsz]

This is true, but is deeply tied into some questions about when we reset type names while printing which are not local changes. The fix involves getting things right across multiple lines of the error trace, and will likely involve making very invasive changes to all the tree_of_* code. Even without that, it requires generating some information up front for the whole trace, and only filling it in later. I think the best conclusion is that (1) there's a genuine bug here, but (2) this PR is not the place to fix it -- I'll start work on a PR to deal with this right after I'm done with this one.

[Octachron]

Yes, I agree that starting with an issue referencing the bug is good enough for now.

[antalsz]

I just submitted PR #10488, which should fix this error.

[Octachron]

The last commit looks fine.
I will have a last glance after this week-end, then I will merge on Monday.

[antalsz]

I've fixed Changes and rebased this onto trunk.

[Octachron]

Merged, thanks for the hard work!

[gasche]

Congratulations @antalsz and @Octachron for this hard work indeed.

[antalsz]

Thank you for the shepherding and review, @Octachron!

[avsm]

This would be a rather wonderful change to have in 4.13, if it's not too late to cherrypick...

[Octachron]

I do regret not reviewing this change in time for 4.13 .

Nevertheless, the change is quite extensive; and it might possibly raise some naked exceptions on some unknown pathological type errors for classes without the #8516 PR, which is not-yet merged.

[lpw25]

it might possibly raise some naked exceptions on some unknown pathological type errors for classes without the #8516 PR

I'm pretty sure it can't raise such exceptions -- or at least that it doesn't change things here. The filter_self_method used to raise Unify and there aren't any Unify handlers around the calls that you are worried about.