Infer with-kinds for GADTs, using Tof_kind for existentials

[glittershark]

Infer full with-kinds for GADTs, using the new Tof_kind type to stand-in for existential type variables.

There's a big Note in jkind.ml explaining the approach here; see that for an overview.

Review all in one go, commit history is mostly not useful.

[goldfirere]

I have done some light review and have concerns, sadly. I just don't think we're going to get away this easily. Might be worth checking in with Leo or Stephen to see if they have wisdom we do not.

[github-actions]

Parser Change Checklist

This PR modifies the parser. Please check that the following tests are updated:

• parsetree/source_jane_street.ml

This test should have examples of every new bit of syntax you are adding. Feel free to just check the box if your PR does not actually change the syntax (because it is refactoring the parser, say).

[goldfirere]

Would be kinda cool to have

Suggested change

	Error: The kind of type "existential_abstract" is immutable_data
	with (type : value mod portable) abstract
	because it's a boxed variant type.
	But the kind of type "existential_abstract" must be a subkind of
	immediate
	because of the annotation on the declaration of the type existential_abstract.
	Error: The kind of type "existential_abstract" is
	immutable_data with (type : value mod portable) abstract
	because it's a boxed variant type.
	But the kind of type "existential_abstract" must be a subkind of
	immediate
	because of the annotation on the declaration of the type existential_abstract.

but not worth a lot of effort if that's hard. (This is just a change in spacing/newlines.)

[goldfirere]

Maybe add tests here like

module F3(M : S with type 'a b = 'a) = struct
  type t : value mod portable = M.t
  let foo (x : t @ nonportable) = use_portable x
end

and

module F4(M : S with type 'a b = 'a) = struct
  let foo (x : t @ contended) = use_uncontended x
end

[goldfirere]

Would be cool to demonstrate the asymmetry of the kind of box2. That is, I think (int, int ref) box2 will mode-cross contention, while (int ref, int) box2 will not. (Yes, I know both of these are uninhabited, but that's not the interesting detail here.)

[goldfirere]

Much of this computation duplicates work in for_boxed_variant. Maybe just inline this? That is, you traverse the result args to find all the bare Tvars, stored in a list. This list will be matched with the params in the call to apply. But it also can be turned into a set and subtracted from the free variables of the entire constructor. This approach has the nice property of making it even clearer that every variable free in a constructor's fields gets substituted away by the apply, either to a param or to a Tof_kind.

[goldfirere]

I think you'd probably need to pass Ctype.free_vars (or Btype.free_vars? not sure about the difference) into for_boxed_variant. That's a small shame.... but certainly no worse than the forward-declaration of this function.

[goldfirere]

Tupling here is, I believe, more efficient than mapping and set-unioning. Might be nice to have a comment explaining why do this (because, to me, mapping and set-unioning is a more direct statement of what you're trying to do).

[goldfirere]

Can't we arrange just to mark these best upon construction? I think that's better than doing it here.

[glittershark]

not trivially, since best jkinds can't be lr. Should we relax that requirement?