Optimize and improve debugging for with-kinds (#3630)

* Add relevant axes to normalize

* Be a bit more direct

* Add short-circuit in set_max_in_set

* Early bailouts in normalize

* Fix merge conflicts

* Add some [@nontail] annotations to avoid alloc'ing a closure

* Don't subst when there are no args

* More accurate empty-with-bounds test

* Make [is_max] a quick check

* Fix bug, and make it structurally harder to reintroduce

* Improvements to debugging of jkinds

* Another debug printer

* Normalize upon creation of a Violation

* Accept new output

* Print *types* not *type schemes*

* Unconditionally print with-bounds, accepting new output

* Strip out support for normalization during printing

* Make printing types easier

* Short-circuit when no axes are relevant

* Get all the modal bounds in one big go.

* Avoid map_type_expr in common case

* More debugging support

* Improve CR comment on failing test case

* Deal correctly with open types after unboxing

* Document mod-bounds functions

* more docs for is_obviously_max

* Update comment in typing/jkind.ml

* wrap a comment

* relevant_axes -> skip_axes

This difference, perhaps somewhat surprisingly, shows up on a (very quick)
profile!

* promote, after re-disabling inference

* fixes for relevant_axes->skip_axes

* promote failures after rebase

---------

Co-authored-by: Aspen Smith <[email protected]>

Author: goldfirere

testsuite/tests/typing-jkind-bounds/annots.ml

@@ -246,7 +246,17 @@ Line 1, characters 21-23:
                          ^^
 Error: This alias is bound to type "int list"
        but is used as an instance of type "('a : immediate)"
-       The kind of int list is value
+       The kind of int list is immutable_data
+         because it's a boxed variant type.
+       But the kind of int list must be a subkind of immediate
+         because of the annotation on the type variable 'a.
+|}, Principal{|
+Line 1, characters 21-23:
+1 | let x : int list as ('a : immediate) = [3;4;5]
+                         ^^
+Error: This alias is bound to type "int list"
+       but is used as an instance of type "('a : immediate)"
+       The kind of int list is immutable_data with int
          because it's a boxed variant type.
        But the kind of int list must be a subkind of immediate
          because of the annotation on the type variable 'a.
@@ -260,7 +270,17 @@ Line 1, characters 21-23:
                          ^^
 Error: This alias is bound to type "int list"
        but is used as an instance of type "('a : value mod global)"
-       The kind of int list is value
+       The kind of int list is immutable_data
+         because it's a boxed variant type.
+       But the kind of int list must be a subkind of value mod global
+         because of the annotation on the type variable 'a.
+|}, Principal{|
+Line 1, characters 21-23:
+1 | let x : int list as ('a : value mod global) = [3;4;5]
+                         ^^
+Error: This alias is bound to type "int list"
+       but is used as an instance of type "('a : value mod global)"
+       The kind of int list is immutable_data with int
          because it's a boxed variant type.
        But the kind of int list must be a subkind of value mod global
          because of the annotation on the type variable 'a.
@@ -1116,7 +1136,7 @@ type t : value mod global = { x : t_value }
 Line 1, characters 0-43:
 1 | type t : value mod global = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
@@ -1127,7 +1147,7 @@ type t : value mod aliased = { x : t_value }
 Line 1, characters 0-44:
 1 | type t : value mod aliased = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod aliased
          because of the annotation on the declaration of the type t.
@@ -1138,7 +1158,7 @@ type t : value mod many = { x : t_value }
 Line 1, characters 0-41:
 1 | type t : value mod many = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod many
          because of the annotation on the declaration of the type t.
@@ -1149,7 +1169,7 @@ type t : value mod portable = { x : t_value }
 Line 1, characters 0-45:
 1 | type t : value mod portable = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod portable
          because of the annotation on the declaration of the type t.
@@ -1160,7 +1180,7 @@ type t : value mod contended = { x : t_value }
 Line 1, characters 0-46:
 1 | type t : value mod contended = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod contended
          because of the annotation on the declaration of the type t.
@@ -1171,7 +1191,7 @@ type t : value mod external_ = { x : t_value }
 Line 1, characters 0-46:
 1 | type t : value mod external_ = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod external_
          because of the annotation on the declaration of the type t.
@@ -1255,7 +1275,7 @@ type t : value mod global = Foo of t_value
 Line 1, characters 0-42:
 1 | type t : value mod global = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
@@ -1266,7 +1286,7 @@ type t : value mod aliased = Foo of t_value
 Line 1, characters 0-43:
 1 | type t : value mod aliased = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod aliased
          because of the annotation on the declaration of the type t.
@@ -1277,7 +1297,7 @@ type t : value mod many = Foo of t_value
 Line 1, characters 0-40:
 1 | type t : value mod many = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod many
          because of the annotation on the declaration of the type t.
@@ -1288,7 +1308,7 @@ type t : value mod portable = Foo of t_value
 Line 1, characters 0-44:
 1 | type t : value mod portable = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod portable
          because of the annotation on the declaration of the type t.
@@ -1299,7 +1319,7 @@ type t : value mod contended = Foo of t_value
 Line 1, characters 0-45:
 1 | type t : value mod contended = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod contended
          because of the annotation on the declaration of the type t.
@@ -1310,7 +1330,7 @@ type t : value mod external_ = Foo of t_value
 Line 1, characters 0-45:
 1 | type t : value mod external_ = Foo of t_value
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of value mod external_
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-jkind-bounds/basics.ml

@@ -762,7 +762,7 @@ type t : any mod many = { x : t_value }
 Line 1, characters 0-39:
 1 | type t : any mod many = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of any mod many
          because of the annotation on the declaration of the type t.
@@ -773,7 +773,7 @@ type t : any mod contended = { x : t_value }
 Line 1, characters 0-44:
 1 | type t : any mod contended = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of any mod contended
          because of the annotation on the declaration of the type t.
@@ -784,7 +784,7 @@ type t : any mod portable = { x : t_value }
 Line 1, characters 0-43:
 1 | type t : any mod portable = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of any mod portable
          because of the annotation on the declaration of the type t.
@@ -795,7 +795,7 @@ type t : any mod many contended portable global = { x : t_value }
 Line 1, characters 0-65:
 1 | type t : any mod many contended portable global = { x : t_value }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with t_value
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of
          any mod global many contended portable
@@ -990,54 +990,69 @@ type ('a : immediate) t : value mod global = { mutable x : 'a }
 Line 1, characters 0-63:
 1 | type ('a : immediate) t : value mod global = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data
+Error: The kind of type "t" is mutable_data with 'a @@ many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
+
+       The first mode-crosses less than the second along:
+         locality: mod local ≰ mod global
 |}]
 
 type ('a : immediate) t : value mod aliased = { mutable x : 'a }
 [%%expect {|
 Line 1, characters 0-64:
 1 | type ('a : immediate) t : value mod aliased = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data
+Error: The kind of type "t" is mutable_data with 'a @@ many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod aliased
          because of the annotation on the declaration of the type t.
+
+       The first mode-crosses less than the second along:
+         uniqueness: mod unique ≰ mod aliased
 |}]
 
 type ('a : immediate) t : value mod contended = { mutable x : 'a }
 [%%expect {|
 Line 1, characters 0-66:
 1 | type ('a : immediate) t : value mod contended = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data
+Error: The kind of type "t" is mutable_data with 'a @@ many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod contended
          because of the annotation on the declaration of the type t.
+
+       The first mode-crosses less than the second along:
+         contention: mod uncontended ≰ mod contended
 |}]
 
 type ('a : immediate) t : value mod external_ = { mutable x : 'a }
 [%%expect {|
 Line 1, characters 0-66:
 1 | type ('a : immediate) t : value mod external_ = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data
+Error: The kind of type "t" is mutable_data with 'a @@ many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod external_
          because of the annotation on the declaration of the type t.
+
+       The first mode-crosses less than the second along:
+         externality: mod internal ≰ mod external_
 |}]
 
 type ('a : immediate) t : value mod external64 = { mutable x : 'a }
 [%%expect {|
 Line 1, characters 0-67:
 1 | type ('a : immediate) t : value mod external64 = { mutable x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is mutable_data
+Error: The kind of type "t" is mutable_data with 'a @@ many
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod external64
          because of the annotation on the declaration of the type t.
+
+       The first mode-crosses less than the second along:
+         externality: mod internal ≰ mod external64
 |}]
 
 (*************************************)
@@ -1234,7 +1249,7 @@ type 'a t : value mod aliased = { x : 'a @@ aliased }
 Line 1, characters 0-53:
 1 | type 'a t : value mod aliased = { x : 'a @@ aliased }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod aliased
          because of the annotation on the declaration of the type t.
@@ -1245,7 +1260,7 @@ type 'a t : value mod global = { x : 'a @@ global }
 Line 1, characters 0-51:
 1 | type 'a t : value mod global = { x : 'a @@ global }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
@@ -1547,7 +1562,7 @@ type 'a t : value mod global = { x : 'a }
 Line 1, characters 0-41:
 1 | type 'a t : value mod global = { x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod global
          because of the annotation on the declaration of the type t.
@@ -1558,7 +1573,7 @@ type 'a t : value mod many = { x : 'a }
 Line 1, characters 0-39:
 1 | type 'a t : value mod many = { x : 'a }
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a
          because it's a boxed record type.
        But the kind of type "t" must be a subkind of value mod many
          because of the annotation on the declaration of the type t.
@@ -1643,7 +1658,7 @@ Lines 11-12, characters 4-10:
 12 |      |> id
 Error: This expression has type "int t" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of int t is immutable_data
+       The kind of int t is immutable_data with int
          because of the definition of t at line 3, characters 0-21.
        But the kind of int t must be a subkind of value mod portable
          because of the definition of require_portable at line 2, characters 21-57.
@@ -1698,7 +1713,7 @@ Lines 11-12, characters 4-10:
 12 |      |> id
 Error: This expression has type "int t" but an expression was expected of type
          "('a : value mod portable)"
-       The kind of int t is immutable_data
+       The kind of int t is immutable_data with int
          because of the definition of t at line 3, characters 0-21.
        But the kind of int t must be a subkind of value mod portable
          because of the definition of require_portable at line 2, characters 21-57.

testsuite/tests/typing-jkind-bounds/composite.ml

@@ -181,9 +181,21 @@ Line 1, characters 13-20:
 1 | let foo (t : int ref t @@ contended) = use_uncontended t
                  ^^^^^^^
 Error: This type "int ref" should be an instance of type "('a : immutable_data)"
-       The kind of int ref is value mod many unyielding.
+       The kind of int ref is mutable_data.
        But the kind of int ref must be a subkind of immutable_data
          because of the definition of t at line 1, characters 0-46.
+|}, Principal{|
+Line 1, characters 13-20:
+1 | let foo (t : int ref t @@ contended) = use_uncontended t
+                 ^^^^^^^
+Error: This type "int ref" should be an instance of type "('a : immutable_data)"
+       The kind of int ref is mutable_data with int @@ many.
+       But the kind of int ref must be a subkind of immutable_data
+         because of the definition of t at line 1, characters 0-46.
+
+       The first mode-crosses less than the second along:
+         contention: mod uncontended ≰ mod contended
+         portability: mod portable with int ≰ mod portable
 |}]
 
 let foo (t : int t @@ local) = use_global t [@nontail]
@@ -319,9 +331,21 @@ Line 1, characters 13-20:
 1 | let foo (t : int ref t @@ contended) = use_uncontended t
                  ^^^^^^^
 Error: This type "int ref" should be an instance of type "('a : immutable_data)"
-       The kind of int ref is value mod many unyielding.
+       The kind of int ref is mutable_data.
        But the kind of int ref must be a subkind of immutable_data
          because of the definition of t at line 1, characters 0-73.
+|}, Principal{|
+Line 1, characters 13-20:
+1 | let foo (t : int ref t @@ contended) = use_uncontended t
+                 ^^^^^^^
+Error: This type "int ref" should be an instance of type "('a : immutable_data)"
+       The kind of int ref is mutable_data with int @@ many.
+       But the kind of int ref must be a subkind of immutable_data
+         because of the definition of t at line 1, characters 0-73.
+
+       The first mode-crosses less than the second along:
+         contention: mod uncontended ≰ mod contended
+         portability: mod portable with int ≰ mod portable
 |}]
 
 let foo (t : int t @@ aliased) = use_unique t
@@ -499,7 +523,9 @@ Line 1, characters 0-149:
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 Error: The kind of type "int list list list list list list list list list list
                         list list list list list list list list list list
-                        list list list list" is value
+                        list list list list" is immutable_data
+         with int list list list list list list list list list list list list list list
+list list list list list list
          because it's a boxed variant type.
        But the kind of type "int list list list list list list list list list
                             list list list list list list list list list list
@@ -567,7 +593,7 @@ type 'a t : immutable_data = Flat | Nested of 'a t t
 Line 1, characters 0-52:
 1 | type 'a t : immutable_data = Flat | Nested of 'a t t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a t t t t t
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.
@@ -606,11 +632,13 @@ Error:
 
 type ('a : immutable_data) t : immutable_data = Flat | Nested of 'a t t
 (* CR layouts v2.8: This should work once we get proper subsumption. *)
+(* CR layouts v2.8: If we can't get this accepted, investigate the terrible
+   /2 stuff in the error message. That scares me a bit. *)
 [%%expect {|
 Line 1, characters 0-71:
 1 | type ('a : immutable_data) t : immutable_data = Flat | Nested of 'a t t
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-Error: The kind of type "t" is value
+Error: The kind of type "t" is immutable_data with 'a t/2 t/2 t/2 t/2 t/2
          because it's a boxed variant type.
        But the kind of type "t" must be a subkind of immutable_data
          because of the annotation on the declaration of the type t.

testsuite/tests/typing-jkind-bounds/gadt.ml

@@ -152,6 +152,7 @@ module F :
 module Arg1 : sig type t1 = int -> int type t2 = string end
 module M1 : sig type t3 = F(Arg1).t3 type t4 = F(Arg1).t4 end
 >> Fatal error: Abstract kind with [with]: value mod portable
+with Arg1.t2
 Uncaught exception: Misc.Fatal_error
 
 |}]