Generate full error traces during module inclusion

.depend

@@ -679,6 +679,7 @@ typing/includeclass.cmx : \
     typing/includeclass.cmi
 typing/includeclass.cmi : \
     typing/types.cmi \
+    typing/printtyp.cmi \
     parsing/location.cmi \
     typing/env.cmi \
     typing/ctype.cmi
@@ -689,6 +690,7 @@ typing/includecore.cmo : \
     typing/printtyp.cmi \
     typing/primitive.cmi \
     typing/path.cmi \
+    utils/misc.cmi \
     typing/ident.cmi \
     typing/errortrace.cmi \
     typing/env.cmi \
@@ -704,6 +706,7 @@ typing/includecore.cmx : \
     typing/printtyp.cmx \
     typing/primitive.cmx \
     typing/path.cmx \
+    utils/misc.cmx \
     typing/ident.cmx \
     typing/errortrace.cmx \
     typing/env.cmx \

Changes

@@ -19,6 +19,10 @@ Working version
 - #10328: Give more precise error when disambiguation could not possibly work.
   (Leo White, review by Gabriel Scherer and Florian Angeletti)
 
+- #10407: Produce more detailed error messages that contain full error traces
+  when module inclusion fails.
+  (Antal Spector-Zabusky, review by Florian Angeletti)
+
 ### Internal/compiler-libs changes:
 
 - #10433: Remove the distinction between 32-bit aligned and 64-bit aligned

testsuite/tests/printing-types/disambiguation.ml

@@ -9,14 +9,16 @@ Error: Type declarations do not match:
          type !'a x = private [> `x ] constraint 'a = 'a x
        is not included in
          type 'a x
-       Their constraints differ.
+       Their parameters differ
+       The type 'b x as 'b is not equal to the type 'a
 |}, Principal{|
 Line 1:
 Error: Type declarations do not match:
          type !'a x = private 'a constraint 'a = [> `x ]
        is not included in
          type 'a x
-       Their constraints differ.
+       Their parameters differ
+       The type [> `x ] is not equal to the type 'a
 |}];;
 
 

testsuite/tests/typing-extensions/extensions.ml

@@ -322,9 +322,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A of int
        Constructors do not match:
          A of float
-       is not compatible with:
+       is not the same as:
          A of int
-       The types are not equal.
+       The type float is not equal to the type int
 |}]
 
 module M : sig
@@ -348,9 +348,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A of 'a
        Constructors do not match:
          A of 'b
-       is not compatible with:
+       is not the same as:
          A of 'a
-       The types are not equal.
+       The type 'b is not equal to the type 'a
 |}]
 
 module M : sig
@@ -374,9 +374,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar = A of 'a
        Constructors do not match:
          A of 'a
-       is not compatible with:
+       is not the same as:
          A of 'a
-       The types are not equal.
+       The type 'a is not equal to the type 'b
 |}];;
 
 
@@ -401,9 +401,9 @@ Error: Signature mismatch:
          type ('a, 'b) bar += A : 'c -> ('c, 'd) bar
        Constructors do not match:
          A : 'd -> ('c, 'd) bar
-       is not compatible with:
+       is not the same as:
          A : 'c -> ('c, 'd) bar
-       The types are not equal.
+       The type 'd is not equal to the type 'c
 |}]
 
 (* Extensions can be rebound *)

testsuite/tests/typing-extensions/open_types.ml

@@ -117,7 +117,8 @@ Line 1, characters 0-37:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: This variant or record definition does not match that of type
          ('a, 'a) foo
-       Their constraints differ.
+       Their parameters differ
+       The type 'a is not equal to the type 'b
 |}]
 
 (* Check that signatures can hide exstensibility *)
@@ -236,7 +237,7 @@ Error: Signature mismatch:
          type foo = M.foo = private ..
        is not included in
          type foo = ..
-       A private type would be revealed.
+       A private extensible variant would be revealed.
 |}]
 
 

testsuite/tests/typing-gadts/ambiguity.ml

@@ -233,6 +233,10 @@ Error: Signature mismatch:
          val r : '_weak1 list ref
        is not included in
          val r : T.u list ref
+       The type '_weak1 list ref is not compatible with the type T.u list ref
+       Type '_weak1 is not compatible with type T.u = T.t
+       This instance of T.t is ambiguous:
+       it would escape the scope of its equation
 |}]
 
 module M = struct
@@ -264,4 +268,8 @@ Error: Signature mismatch:
          val r : '_weak2 list ref
        is not included in
          val r : T.t list ref
+       The type '_weak2 list ref is not compatible with the type T.t list ref
+       Type '_weak2 is not compatible with type T.t = T.u
+       This instance of T.u is ambiguous:
+       it would escape the scope of its equation
 |}]

testsuite/tests/typing-gadts/pr7160.ml

@@ -20,7 +20,8 @@ Lines 4-5, characters 0-77:
 Error: This variant or record definition does not match that of type 'a t
        Constructors do not match:
          Same : 'l t -> 'l t
-       is not compatible with:
+       is not the same as:
          Same : 'l1 t -> 'l2 t
-       The types are not equal.
+       The type 'l t is not equal to the type 'l1 t
+       Type 'l is not equal to type 'l1
 |}];;

testsuite/tests/typing-gadts/pr7378.ml

@@ -21,9 +21,10 @@ Lines 2-3, characters 2-37:
 Error: This variant or record definition does not match that of type X.t
        Constructors do not match:
          A : 'a * 'b * ('a -> unit) -> X.t
-       is not compatible with:
+       is not the same as:
          A : 'a * 'b * ('b -> unit) -> X.t
-       The types are not equal.
+       The type 'a -> unit is not equal to the type 'b -> unit
+       Type 'a is not equal to type 'b
 |}]
 
 (* would segfault

testsuite/tests/typing-gadts/return_type.ml

@@ -0,0 +1,36 @@
+(* TEST
+   * expect
+*)
+
+type i = int
+
+type 'a t = T : i
+[%%expect{|
+type i = int
+Line 3, characters 16-17:
+3 | type 'a t = T : i
+                    ^
+Error: Constraints are not satisfied in this type.
+       Type i should be an instance of 'a t
+|}]
+
+type 'a t = T : i t
+type 'a s = 'a t = T : i t
+[%%expect{|
+type 'a t = T : i t
+Line 2, characters 23-26:
+2 | type 'a s = 'a t = T : i t
+                           ^^^
+Error: Constraints are not satisfied in this type.
+       Type i t should be an instance of 'a s
+|}]
+
+type 'a t = T : i s
+and  'a s = 'a t
+[%%expect{|
+Line 1, characters 16-19:
+1 | type 'a t = T : i s
+                    ^^^
+Error: Constraints are not satisfied in this type.
+       Type i s should be an instance of 'a t
+|}]

testsuite/tests/typing-gadts/test.ml

@@ -1246,3 +1246,136 @@ Error: This expression has type a = int
        This instance of int is ambiguous:
        it would escape the scope of its equation
 |}];;
+
+module M = struct
+  type t
+end
+type (_,_) eq = Refl: ('a,'a) eq
+let f (x:M.t) (y: (M.t, int -> int) eq) =
+  let Refl = y in
+  if true then x else fun x -> x + 1
+[%%expect{|
+module M : sig type t end
+type (_, _) eq = Refl : ('a, 'a) eq
+Line 7, characters 22-36:
+7 |   if true then x else fun x -> x + 1
+                          ^^^^^^^^^^^^^^
+Error: This expression has type 'a -> 'b
+       but an expression was expected of type M.t = int -> int
+       This instance of int -> int is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+(* Check got/expected when the order changes *)
+module M = struct
+  type t
+end
+type (_,_) eq = Refl: ('a,'a) eq
+let f (x:M.t) (y: (M.t, int -> int) eq) =
+  let Refl = y in
+  if true then fun x -> x + 1 else x
+[%%expect{|
+module M : sig type t end
+type (_, _) eq = Refl : ('a, 'a) eq
+Line 7, characters 35-36:
+7 |   if true then fun x -> x + 1 else x
+                                       ^
+Error: This expression has type M.t = int -> int
+       but an expression was expected of type int -> int
+       This instance of int -> int is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+module M = struct
+  type t
+end
+type (_,_) eq = Refl: ('a,'a) eq
+let f w (x:M.t) (y: (M.t, <m:int>) eq) =
+  let Refl = y in
+  let z = if true then x else w in
+  z#m
+[%%expect{|
+module M : sig type t end
+type (_, _) eq = Refl : ('a, 'a) eq
+Line 8, characters 2-3:
+8 |   z#m
+      ^
+Error: This expression has type M.t but an expression was expected of type
+         < m : 'a; .. >
+       This instance of < m : int > is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+(* Check got/expected when the order changes *)
+module M = struct
+  type t
+end
+type (_,_) eq = Refl: ('a,'a) eq
+let f w (x:M.t) (y: (M.t, <m:int>) eq) =
+  let Refl = y in
+  let z = if true then w else x in
+  z#m
+[%%expect{|
+module M : sig type t end
+type (_, _) eq = Refl : ('a, 'a) eq
+Line 8, characters 2-3:
+8 |   z#m
+      ^
+Error: This expression has type M.t but an expression was expected of type
+         < m : 'a; .. >
+       This instance of < m : int > is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+type (_,_) eq = Refl: ('a,'a) eq
+module M = struct
+  type t = C : (<m:int; ..> as 'a) * ('a, <m:int; b:bool>) eq -> t
+end
+let f (C (x,y) : M.t) =
+  let g w =
+    let Refl = y in
+    let z = if true then w else x in
+    z#b
+  in ()
+[%%expect{|
+type (_, _) eq = Refl : ('a, 'a) eq
+module M :
+  sig
+    type t =
+        C : (< m : int; .. > as 'a) * ('a, < b : bool; m : int >) eq -> t
+  end
+Line 9, characters 4-5:
+9 |     z#b
+        ^
+Error: This expression has type $C_'a = < b : bool >
+       but an expression was expected of type < b : 'a; .. >
+       This instance of < b : bool > is ambiguous:
+       it would escape the scope of its equation
+|}]
+
+(* Check got/expected when the order changes *)
+type (_,_) eq = Refl: ('a,'a) eq
+module M = struct
+  type t = C : (<m:int; ..> as 'a) * ('a, <m:int; b:bool>) eq -> t
+end
+let f (C (x,y) : M.t) =
+  let g w =
+    let Refl = y in
+    let z = if true then x else w in
+    z#b
+  in ()
+[%%expect{|
+type (_, _) eq = Refl : ('a, 'a) eq
+module M :
+  sig
+    type t =
+        C : (< m : int; .. > as 'a) * ('a, < b : bool; m : int >) eq -> t
+  end
+Line 9, characters 4-5:
+9 |     z#b
+        ^
+Error: This expression has type $C_'a = < b : bool >
+       but an expression was expected of type < b : 'a; .. >
+       This instance of < b : bool > is ambiguous:
+       it would escape the scope of its equation
+|}]