Recognize unrecoverable errors in Includemod

Stop the computation of a signature difference when the types start to diverge
in order to avoid trying to typecheck items in incoherent environments.

See ocaml#10836

Changes

@@ -527,6 +527,9 @@ OCaml 4.14.0
   toplevel, as in the bytecode toplevel.
   (David Allsopp, report by Nathan Rebours, review by Gabriel Scherer)
 
+- #10836, #?????: avoid internal typechecker errors when checking signature
+  inclusion in presence of incompatible types.
+  (Florian Angeletti, review by ????)
 
 OCaml 4.13 maintenance branch
 -----------------------------

testsuite/tests/typing-misc/distant_errors.ml

@@ -0,0 +1,34 @@
+(* TEST
+  * expect
+*)
+
+(** The aim of this file is to keep track of programs that are "far" from being well-typed *)
+
+
+(** Arity mismatch between structure and signature *)
+
+module M : sig
+  type (_, _) t
+  val f : (_, _) t -> unit
+end = struct
+  type _ t
+  let f _ = ()
+end
+
+[%%expect{|
+Lines 9-12, characters 6-3:
+ 9 | ......struct
+10 |   type _ t
+11 |   let f _ = ()
+12 | end
+Error: Signature mismatch:
+       Modules do not match:
+         sig type _ t val f : 'a -> unit end
+       is not included in
+         sig type (_, _) t val f : ('a, 'b) t -> unit end
+       Type declarations do not match:
+         type _ t
+       is not included in
+         type (_, _) t
+       They have different arities.
+|}]

typing/includemod.ml

@@ -104,6 +104,7 @@ module Error = struct
     missings: signature_item list;
     incompatibles: (Ident.t * sigitem_symptom) list;
     oks: (int * module_coercion) list;
+    unknowns: (signature_item * signature_item * int) list;
   }
   and sigitem_symptom =
     | Core of core_sigitem_symptom
@@ -361,6 +362,17 @@ let retrieve_functor_params env mty =
    Return the restriction that transforms a value of the smaller type
    into a value of the bigger type. *)
 
+(* When computing a signature difference, we need to distinguish between
+   recoverable errors at the value level and unrecoverable errors at the type
+   level that require us to stop the computation of the difference due to
+   incoherent types.
+*)
+type 'a recoverable_error = { error: 'a; recoverable:bool }
+let recoverable_error r =
+  Result.map_error (fun error -> { error; recoverable=true}) r
+let unrecoverable_error r =
+  Result.map_error (fun error -> { error; recoverable=false}) r
+
 (**
    In the group of mutual functions below, the [~in_eq] argument is [true] when
    we are in fact checking equality of module types.
@@ -606,13 +618,13 @@ and signatures  ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
      and the coercion to be applied to it. *)
   let rec pair_components subst paired unpaired = function
       [] ->
-        let oks, (shape_map, deep_modifications), errors =
+        let oks, (shape_map, deep_modifications), errors, unknowns =
           signature_components ~in_eq ~loc env ~mark new_env subst mod_shape
             Shape.Map.empty
             (List.rev paired)
         in
-        begin match unpaired, errors, oks with
-            | [], [], cc ->
+        begin match unpaired, errors, oks, unknowns with
+            | [], [], cc, [] ->
                 let shape =
                   if not deep_modifications && exported_len1 = exported_len2
                   then mod_shape
@@ -622,8 +634,14 @@ and signatures  ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
                   Ok (simplify_structure_coercion cc id_pos_list, shape)
                 else
                   Ok (Tcoerce_structure (cc, id_pos_list), shape)
-            | missings, incompatibles, cc ->
-                Error { env=new_env; Error.missings; incompatibles; oks=cc }
+            | missings, incompatibles, cc, unknowns ->
+                Error {
+                  Error.env=new_env;
+                  missings;
+                  incompatibles;
+                  oks=cc;
+                  unknowns
+                }
         end
     | item2 :: rem ->
         let (id2, _loc, name2) = item_ident_name item2 in
@@ -668,7 +686,7 @@ and signatures  ~in_eq ~loc env ~mark subst sig1 sig2 mod_shape =
 and signature_components  ~in_eq ~loc old_env ~mark env subst
     orig_shape shape_map paired =
   match paired with
-  | [] -> [], (shape_map, false), []
+  | [] -> [], (shape_map, false), [], []
   | (sigi1, sigi2, pos) :: rem ->
       let shape_modified = ref false in
       let id, item, shape_map, present_at_runtime =
@@ -682,17 +700,20 @@ and signature_components  ~in_eq ~loc old_env ~mark env subst
               | _ -> true
             in
             let shape_map = Shape.Map.add_value_proj shape_map id1 orig_shape in
+            let item = recoverable_error item in
             id1, item, shape_map, present_at_runtime
         | Sig_type(id1, tydec1, _, _), Sig_type(_id2, tydec2, _, _) ->
             let item =
               type_declarations ~loc ~old_env env ~mark subst id1 tydec1 tydec2
             in
+            let item = unrecoverable_error item in
             let shape_map = Shape.Map.add_type_proj shape_map id1 orig_shape in
             id1, item, shape_map, false
         | Sig_typext(id1, ext1, _, _), Sig_typext(_id2, ext2, _, _) ->
             let item =
               extension_constructors ~loc env ~mark  subst id1 ext1 ext2
             in
+            let item = unrecoverable_error item in
             let shape_map =
               Shape.Map.add_extcons_proj shape_map id1 orig_shape
             in
@@ -727,6 +748,7 @@ and signature_components  ~in_eq ~loc old_env ~mark env subst
                     true, Result.map (fun i -> Tcoerce_alias (env, p1, i)) item
                 | Mp_absent, Mp_present, _ -> assert false
               in
+              let item = unrecoverable_error item in
               id1, item, shape_map, present_at_runtime
             end
         | Sig_modtype(id1, info1, _), Sig_modtype(_id2, info2, _) ->
@@ -736,6 +758,7 @@ and signature_components  ~in_eq ~loc old_env ~mark env subst
             let shape_map =
               Shape.Map.add_module_type_proj shape_map id1 orig_shape
             in
+            let item = unrecoverable_error item in
             id1, item, shape_map, false
         | Sig_class(id1, decl1, _, _), Sig_class(_id2, decl2, _, _) ->
             let item =
@@ -744,6 +767,7 @@ and signature_components  ~in_eq ~loc old_env ~mark env subst
             let shape_map =
               Shape.Map.add_class_proj shape_map id1 orig_shape
             in
+            let item = unrecoverable_error item in
             id1, item, shape_map, true
         | Sig_class_type(id1, info1, _, _), Sig_class_type(_id2, info2, _, _) ->
             let item =
@@ -752,19 +776,28 @@ and signature_components  ~in_eq ~loc old_env ~mark env subst
             let shape_map =
               Shape.Map.add_class_type_proj shape_map id1 orig_shape
             in
+            let item = unrecoverable_error item in
             id1, item, shape_map, false
         | _ ->
             assert false
       in
-      let oks, (final_map, deep_modifications), errors =
-        signature_components ~in_eq ~loc old_env ~mark env subst
-          orig_shape shape_map rem
+      let oks, (final_map, deep_modifications), errors, unknowns as r =
+        match item with
+        | Error { recoverable = false; error } ->
+            let final_map = shape_map, !shape_modified in
+            [], final_map, [id,error], rem
+        | Error { recoverable = true; _ } | Ok _ ->
+            signature_components ~in_eq ~loc old_env ~mark env subst
+              orig_shape shape_map rem
       in
       let final_map = final_map, deep_modifications || !shape_modified in
       match item with
-      | Ok x when present_at_runtime -> (pos,x) :: oks, final_map, errors
-      | Ok _ -> oks, final_map, errors
-      | Error y -> oks , final_map, (id,y) :: errors
+      | Ok x when present_at_runtime ->
+          (pos,x) :: oks, final_map, errors, unknowns
+      | Ok _ -> oks, final_map, errors, unknowns
+      | Error {error; recoverable = true }  ->
+          oks, final_map, (id,error) :: errors, unknowns
+      | Error {recoverable=false; _ }  -> r
 
 and module_declarations  ~in_eq ~loc env ~mark  subst id1 md1 md2 orig_shape =
   Builtin_attributes.check_alerts_inclusion

typing/includemod.mli

@@ -93,6 +93,7 @@ module Error: sig
     missings: Types.signature_item list;
     incompatibles: (Ident.t * sigitem_symptom) list;
     oks: (int * Typedtree.module_coercion) list;
+    unknowns: ((Types.signature_item as 'it) * 'it * int) list
   }
   and sigitem_symptom =
     | Core of core_sigitem_symptom