Polymorphic parameters

[lpw25]

Seems self-explanatory

[antalsz]

This is a great change, and the code broadly makes sense to me. That said, I think the larger-scale changed structure needs to be clarified. My understanding is that this PR introduces a new invariant that Tarrows always start with a Tpoly. This needs to be called out somehow in the code, and I can see two ways:

1. This could be reflected structurally in the code, such as by adding a new type:

   and type_desc =
     (* ... *)
     | Tarrow of arrow_desc * type_arg * type_expr * commutable
     (* ... *)
   
   and type_arg =
     { arg_vars : type_expr list
     ; arg_type : type_expr }
   (** [{arg_vars = [a; b]; arg_type = t}] ==> ['a 'b. t]to arrow types
       Like [Tpoly], but mandatory for arguments  *)
   
   (* ... *)
   

   (Equivalently, type_arg could be inlined into the Tarrow constructor. And maybe it should be flipped around to match Tpoly.)

2. This could be left as an invariant, but documented, and possibly tagged with a type synonym:

   and type_desc =
     (* ... *)
     | Tarrow of arrow_desc * type_arg * type_expr * commutable
     (* ... *)
   
   and type_arg = type_expr
   (** A [type_arg] is a [type_expr] that is headed by a [Tpoly] constructor, as is
       required for the arguments to [Tarrow]s. This isn't checked, but functions
       that consume [type_arg]s are entitled to assume that it's true. *)
   
   (* ... *)
   

The important thing is that this invariant needs to be legible from the source code; as it stands, it has to be deduced from usage. The tradeoffs between (1) and (2) are fairly typical: on the one hand, if it's reflected structurally, things can't go wrong; on the other hand, then you lose out on having actual type_descs/type_exprs that are Tpolys around, which is potentially inconvenient. I can see arguments for both approaches, so I don't have a strong opinion about which approach to take.

On a related explanatory note, it would be good to see some user-facing documentation for this change (and I'd appreciate some clarification on the principality check, although I'm not sure how important that actually is). And upstream will ask for a changelog entry when we bring this to them; is there a reason not to just write one now?

[goldfirere]

I know this is an annoying comment, but it would be really helpful (I think, to all of us, not just newbie me) to have a design document describing this change. That is, this patch is an implementation. But what is the specification of that implementation? Without a specification, it's hard to assess the correctness of an implementation. That is, I can try to read this and figure out whether we've introduced new soundness bugs (clearly bad), but it would be nice if I could do more than just that -- by assessing whether this implementation correctly, optimally implements a specification.

Important bonus of having a specification: we then have a document to describe to others (e.g. upstream) what we are up to -- very valuable!

[goldfirere]

Haven't really gotten to the code proper yet -- still trying to understand the specification as hinted at in the poly_params.ml file. But there's enough to plumb there! More to come, but I thought getting these preliminary thoughts out there might be helpful, in case I time out later.

[antalsz]

I had one place I'd like an extra comment, but this looks good to me :-)

[lpw25]

I think that this PR just needs a couple of changes now:

1. The use of the new feature should be guarded by an extension flag.
2. There should be user documentation in the jane/doc folder.

I think the user documentation plus the typing rules should hopefully be a sufficient spec for the feature.

[goldfirere]

I think the user documentation plus the typing rules should hopefully be a sufficient spec for the feature.

Yes, I agree.

[goldfirere]

Gaining steam understanding the code. More soon.

[goldfirere]

As discussed, I'm timing out here. But this has been really educational for me!

I do hope the "please comment this more" comments are not too annoying. It's very hard as a current outsider to know what the right level is for documentation, but my (very pleasant) experience in working in a heavily commented compiler suggests that more would be better.

[lpw25]

This is rebased on 4.14 and should be ready to merge once CI has run