Infer with-kinds for GADTs, using Tof_kind for existentials

jane/doc/proposals/kind-inference.md

@@ -480,7 +480,7 @@ m_portability = portable
     Γ ⊢ κᵢ ≤ χᵢ
   κ₀' = κ₀{τsⱼ/[['aᵢ]]}
   ∀ Ξ:
-    mode m_Ξ ≤ Ξ(κ₀')
+    mode mⱼ_Ξ ≤ Ξ(κ₀')
     ∀ σ ∈ types_for(Ξ, field_typesⱼ), with σ ≤ Ξ(κ₀')
   value ≤ lay(κ₀')
 if [@@unboxed]:

testsuite/tests/parsetree/source_jane_street.ml

@@ -1258,14 +1258,8 @@ type existential_abstract : immutable_data with (type : value mod portable) abst
   | Mk : ('a : value mod portable) abstract -> existential_abstract
 [%%expect{|
 type 'a abstract
-Lines 2-3, characters 0-67:
-2 | type existential_abstract : immutable_data with (type : value mod portable) abstract =
-3 |   | Mk : ('a : value mod portable) abstract -> existential_abstract
-Error: The kind of type "existential_abstract" is value
-         because it's a boxed variant type.
-       But the kind of type "existential_abstract" must be a subkind of
-         immutable_data with (type : value mod portable) abstract
-         because of the annotation on the declaration of the type existential_abstract.
+type existential_abstract =
+    Mk : ('a : value mod portable). 'a abstract -> existential_abstract
 |}]
 
 (* not yet supported *)