Semantic diffings for functor types and applications (#9331)

This commit improves the error messages for ill-typed functor applications and inclusion between functor types. It does so by computing a diff between the expected and the provided types, and find an application that minimizes the error. The set of changes also paves the way for better diff for inclusion checks between signatures.


* Implement a generic and variadic Wagner–Fischer algorithm for computing locally optimal
paths.
* Compute a full error tree for module type inclusion and equality errors
* Improve the error message for module type equality
* Expand the error message at the module level by using a diffing algorithm to
analyze erroneous functor multi-applications or inclusions using Levenshtein distance.


Co-authored-by: Florian Angeletti <florian.angeletti@inria.fr>
Co-authored-by: octachron <octa@polychoron.fr>

.depend

@@ -58,6 +58,11 @@ utils/consistbl.cmx : \
     utils/consistbl.cmi
 utils/consistbl.cmi : \
     utils/misc.cmi
+utils/diffing.cmo : \
+    utils/diffing.cmi
+utils/diffing.cmx : \
+    utils/diffing.cmi
+utils/diffing.cmi :
 utils/domainstate.cmo : \
     utils/domainstate.cmi
 utils/domainstate.cmx : \
@@ -703,17 +708,17 @@ typing/includemod.cmo : \
     typing/primitive.cmi \
     typing/predef.cmi \
     typing/path.cmi \
-    typing/oprint.cmi \
     typing/mtype.cmi \
     utils/misc.cmi \
+    parsing/longident.cmi \
     parsing/location.cmi \
     typing/includecore.cmi \
     typing/includeclass.cmi \
     typing/ident.cmi \
     typing/env.cmi \
+    utils/diffing.cmi \
     typing/ctype.cmi \
     file_formats/cmt_format.cmi \
-    utils/clflags.cmi \
     parsing/builtin_attributes.cmi \
     typing/btype.cmi \
     typing/includemod.cmi
@@ -725,29 +730,65 @@ typing/includemod.cmx : \
     typing/primitive.cmx \
     typing/predef.cmx \
     typing/path.cmx \
-    typing/oprint.cmx \
     typing/mtype.cmx \
     utils/misc.cmx \
+    parsing/longident.cmx \
     parsing/location.cmx \
     typing/includecore.cmx \
     typing/includeclass.cmx \
     typing/ident.cmx \
     typing/env.cmx \
+    utils/diffing.cmx \
     typing/ctype.cmx \
     file_formats/cmt_format.cmx \
-    utils/clflags.cmx \
     parsing/builtin_attributes.cmx \
     typing/btype.cmx \
     typing/includemod.cmi
 typing/includemod.cmi : \
     typing/types.cmi \
     typing/typedtree.cmi \
     typing/path.cmi \
+    parsing/longident.cmi \
     parsing/location.cmi \
     typing/includecore.cmi \
     typing/ident.cmi \
     typing/env.cmi \
+    utils/diffing.cmi \
     typing/ctype.cmi
+typing/includemod_errorprinter.cmo : \
+    typing/types.cmi \
+    typing/typedtree.cmi \
+    typing/printtyp.cmi \
+    typing/path.cmi \
+    typing/oprint.cmi \
+    utils/misc.cmi \
+    parsing/location.cmi \
+    typing/includemod.cmi \
+    typing/includecore.cmi \
+    typing/includeclass.cmi \
+    typing/ident.cmi \
+    typing/env.cmi \
+    utils/diffing.cmi \
+    utils/clflags.cmi \
+    typing/includemod_errorprinter.cmi
+typing/includemod_errorprinter.cmx : \
+    typing/types.cmx \
+    typing/typedtree.cmx \
+    typing/printtyp.cmx \
+    typing/path.cmx \
+    typing/oprint.cmx \
+    utils/misc.cmx \
+    parsing/location.cmx \
+    typing/includemod.cmx \
+    typing/includecore.cmx \
+    typing/includeclass.cmx \
+    typing/ident.cmx \
+    typing/env.cmx \
+    utils/diffing.cmx \
+    utils/clflags.cmx \
+    typing/includemod_errorprinter.cmi
+typing/includemod_errorprinter.cmi : \
+    typing/includemod.cmi
 typing/mtype.cmo : \
     typing/types.cmi \
     typing/subst.cmi \
@@ -1531,6 +1572,7 @@ typing/typemod.cmo : \
     parsing/longident.cmi \
     parsing/location.cmi \
     utils/load_path.cmi \
+    typing/includemod_errorprinter.cmi \
     typing/includemod.cmi \
     typing/ident.cmi \
     typing/env.cmi \
@@ -1563,6 +1605,7 @@ typing/typemod.cmx : \
     parsing/longident.cmx \
     parsing/location.cmx \
     utils/load_path.cmx \
+    typing/includemod_errorprinter.cmx \
     typing/includemod.cmx \
     typing/ident.cmx \
     typing/env.cmx \

Changes

@@ -3,6 +3,9 @@ Working version
 
 ### Language features:
 
+- #9331: Improve error messages for functor application and functor types.
+  (Florian Angeletti and Gabriel Radanne, review by Leo White)
+
 - #10013: Let-punning
   Allow 'let* x in ...' and 'let%ext x in ...' as shorthand for
     'let* x = x in ...' and 'let%ext x = x in ...' respectively.

compilerlibs/Makefile.compilerlibs

@@ -31,7 +31,8 @@ UTILS=utils/config.cmo utils/build_path_prefix_map.cmo utils/misc.cmo \
 	utils/terminfo.cmo utils/ccomp.cmo utils/warnings.cmo \
 	utils/consistbl.cmo utils/strongly_connected_components.cmo \
 	utils/targetint.cmo utils/int_replace_polymorphic_compare.cmo \
-	utils/domainstate.cmo utils/binutils.cmo utils/lazy_backtrack.cmo
+	utils/domainstate.cmo utils/binutils.cmo utils/lazy_backtrack.cmo \
+        utils/diffing.cmo
 UTILS_CMI=
 
 PARSING=parsing/location.cmo parsing/longident.cmo \
@@ -57,7 +58,8 @@ TYPING=typing/ident.cmo typing/path.cmo \
   typing/mtype.cmo typing/envaux.cmo typing/includecore.cmo \
   typing/tast_iterator.cmo typing/tast_mapper.cmo typing/stypes.cmo \
   file_formats/cmt_format.cmo typing/cmt2annot.cmo typing/untypeast.cmo \
-  typing/includemod.cmo typing/typetexp.cmo typing/printpat.cmo \
+  typing/includemod.cmo typing/includemod_errorprinter.cmo \
+  typing/typetexp.cmo typing/printpat.cmo \
   typing/patterns.cmo typing/parmatch.cmo \
   typing/typedecl_properties.cmo typing/typedecl_variance.cmo \
   typing/typedecl_unboxed.cmo typing/typedecl_immediacy.cmo \

dune

@@ -46,7 +46,7 @@
    config build_path_prefix_map misc identifiable numbers arg_helper clflags
    profile terminfo ccomp warnings consistbl strongly_connected_components
    targetint load_path int_replace_polymorphic_compare binutils local_store
-   lazy_backtrack
+   lazy_backtrack diffing
 
    ;; PARSING
    location longident docstrings syntaxerr ast_helper camlinternalMenhirLib
@@ -59,7 +59,8 @@
    ident path primitive types btype oprint subst predef datarepr
    cmi_format persistent_env env type_immediacy
    typedtree printtyped ctype printtyp includeclass mtype envaux includecore
-   tast_iterator tast_mapper cmt_format untypeast includemod
+   tast_iterator tast_mapper cmt_format untypeast
+   includemod includemod_errorprinter
    typetexp patterns printpat parmatch stypes typedecl typeopt rec_check
    typecore
    typeclass typemod typedecl_variance typedecl_properties typedecl_immediacy

parsing/location.ml

@@ -721,13 +721,19 @@ let batch_mode_printer : report_printer =
   let pp_txt ppf txt = Format.fprintf ppf "@[%t@]" txt in
   let pp self ppf report =
     setup_colors ();
-    (* Make sure we keep [num_loc_lines] updated. *)
+    (* Make sure we keep [num_loc_lines] updated.
+       The tabulation box is here to give submessage the option
+       to be aligned with the main message box
+    *)
     print_updating_num_loc_lines ppf (fun ppf () ->
-      Format.fprintf ppf "@[<v>%a%a: %a%a@]@."
+      Format.fprintf ppf "@[<v>%a%a%a: %a%a%a%a@]@."
+      Format.pp_open_tbox ()
       (self.pp_main_loc self report) report.main.loc
       (self.pp_report_kind self report) report.kind
+      Format.pp_set_tab ()
       (self.pp_main_txt self report) report.main.txt
       (self.pp_submsgs self report) report.sub
+      Format.pp_close_tbox ()
     ) ()
   in
   let pp_report_kind _self _ ppf = function

parsing/pprintast.ml

@@ -1692,3 +1692,4 @@ let core_type = core_type reset_ctxt
 let pattern = pattern reset_ctxt
 let signature = signature reset_ctxt
 let structure = structure reset_ctxt
+let module_expr = module_expr reset_ctxt

parsing/pprintast.mli

@@ -35,6 +35,8 @@ val signature: Format.formatter -> Parsetree.signature -> unit
 val structure: Format.formatter -> Parsetree.structure -> unit
 val string_of_structure: Parsetree.structure -> string
 
+val module_expr: Format.formatter -> Parsetree.module_expr -> unit
+
 val toplevel_phrase : Format.formatter -> Parsetree.toplevel_phrase -> unit
 val top_phrase: Format.formatter -> Parsetree.toplevel_phrase -> unit
 

testsuite/tests/typing-misc/pr6416.ml

@@ -83,11 +83,13 @@ Error: Signature mismatch:
          sig module A : functor (X : s) -> sig end end
        In module A:
        Modules do not match:
-         functor (X : s/1) -> sig end
+         functor (X : s/1) -> ...
        is not included in
-         functor (X : s/2) -> sig end
-       At position module A(X : <here>) : ...
-       Modules do not match: s/2 is not included in s/1
+         functor (X : s/2) -> ...
+       Module types do not match:
+         s/1
+       does not include
+         s/2
        Line 5, characters 6-19:
          Definition of module type s/1
        Line 2, characters 2-15:

testsuite/tests/typing-modules-bugs/pr7414_2_bad.compilers.reference

@@ -1,20 +1,16 @@
-File "pr7414_2_bad.ml", line 46, characters 28-34:
+File "pr7414_2_bad.ml", line 46, characters 22-35:
 46 |   let module Ignore = Force(Choose) in
-                                 ^^^^^^
-Error: Signature mismatch:
-       Modules do not match:
-         functor () -> sig module Choice : T val r : '_weak1 list ref ref end
-       is not included in
-         functor () -> S
-       At position functor () -> <here>
-       Modules do not match:
-         sig module Choice : T val r : '_weak1 list ref ref end
-       is not included in
-         S
-       At position functor () -> <here>
-       Values do not match:
-         val r : '_weak1 list ref ref
-       is not included in
-         val r : Choice.t list ref ref
-       File "pr7414_2_bad.ml", line 29, characters 2-31: Expected declaration
-       File "pr7414_2_bad.ml", line 40, characters 8-9: Actual declaration
+                           ^^^^^^^^^^^^^
+Error: Modules do not match:
+       functor () -> sig module Choice : T val r : '_weak1 list ref ref end
+     is not included in functor () -> S
+     Modules do not match:
+       sig module Choice : T val r : '_weak1 list ref ref end
+     is not included in
+       S
+     Values do not match:
+       val r : '_weak1 list ref ref
+     is not included in
+       val r : Choice.t list ref ref
+     File "pr7414_2_bad.ml", line 29, characters 2-31: Expected declaration
+     File "pr7414_2_bad.ml", line 40, characters 8-9: Actual declaration

testsuite/tests/typing-modules-bugs/pr7414_bad.compilers.reference

@@ -1,20 +1,16 @@
-File "pr7414_bad.ml", line 52, characters 22-28:
+File "pr7414_bad.ml", line 52, characters 16-29:
 52 | module Ignore = Force(Choose)
-                           ^^^^^^
-Error: Signature mismatch:
-       Modules do not match:
-         functor () -> sig module Choice : T val r : '_weak1 list ref ref end
-       is not included in
-         functor () -> S
-       At position functor () -> <here>
-       Modules do not match:
-         sig module Choice : T val r : '_weak1 list ref ref end
-       is not included in
-         S
-       At position functor () -> <here>
-       Values do not match:
-         val r : '_weak1 list ref ref
-       is not included in
-         val r : Choice.t list ref ref
-       File "pr7414_bad.ml", line 38, characters 2-31: Expected declaration
-       File "pr7414_bad.ml", line 33, characters 6-7: Actual declaration
+                     ^^^^^^^^^^^^^
+Error: Modules do not match:
+       functor () -> sig module Choice : T val r : '_weak1 list ref ref end
+     is not included in functor () -> S
+     Modules do not match:
+       sig module Choice : T val r : '_weak1 list ref ref end
+     is not included in
+       S
+     Values do not match:
+       val r : '_weak1 list ref ref
+     is not included in
+       val r : Choice.t list ref ref
+     File "pr7414_bad.ml", line 38, characters 2-31: Expected declaration
+     File "pr7414_bad.ml", line 33, characters 6-7: Actual declaration

testsuite/tests/typing-modules/aliases.ml

@@ -691,9 +691,9 @@ Error: Module type declarations do not match:
        does not match
          module type A = sig module M = F(List) end
        At position module type A = <here>
-       Modules do not match:
+       Module types do not match:
          sig module M = F(List) end
-       is not included in
+       is not equal to
          sig module M = F(List) end
        At position module type A = sig module M : <here> end
        Module F(List) cannot be aliased

testsuite/tests/typing-modules/applicative_functor_type.ml

@@ -19,13 +19,11 @@ type t = Set.Make(M).t
 Line 1, characters 9-22:
 1 | type t = Set.Make(M).t
              ^^^^^^^^^^^^^
-Error: The type of M does not match Set.Make's parameter
-       Modules do not match:
-         sig type t = M.t val equal : 'a -> 'a -> bool end
-       is not included in
-         Set.OrderedType
-       The value `compare' is required but not provided
-       File "set.mli", line 55, characters 4-31: Expected declaration
+Error: Modules do not match:
+       sig type t = M.t val equal : 'a -> 'a -> bool end
+     is not included in Set.OrderedType
+     The value `compare' is required but not provided
+     File "set.mli", line 55, characters 4-31: Expected declaration
 |} ]
 
 
@@ -43,15 +41,13 @@ type t = F(M).t
 Line 1, characters 9-15:
 1 | type t = F(M).t
              ^^^^^^
-Error: The type of M does not match F's parameter
-       Modules do not match:
-         sig type t = M.t val equal : 'a -> 'a -> bool end
-       is not included in
-         sig type t = M.t val equal : unit end
-       Values do not match:
-         val equal : 'a -> 'a -> bool
-       is not included in
-         val equal : unit
+Error: Modules do not match:
+       sig type t = M.t val equal : 'a -> 'a -> bool end
+     is not included in sig type t = M.t val equal : unit end
+     Values do not match:
+       val equal : 'a -> 'a -> bool
+     is not included in
+       val equal : unit
 |} ]