Why not just call merge_constraint here? That's definitely overkill, but it seems better than duplicating code. I don't see what merge_package_constraint does that's better than merge_constraint.

I don't think this works - trying to use merge_constraint for both things is the source of the problems fixed in this PR.

The key difference is that merge_package_constraint takes the constraint as an already-translated bit of typedtree, while merge_constraint takes it as a not-yet-translated parsetree type decl. That type decl is subsequently typechecked in the wrong type variable environment to support package constriants, which is why the old version used the fake malformed bit of parsetree described in the PR description above. I tried to explain there why obvious small tweaks to that approach don't work - maybe that makes more sense after this answer, but if not let me know and I'll try again.

I had missed the difference between the parsetree and the typedtree here -- an important distinction.

But I'm still not convinced we have to repeat all this code. You encountered two problems, but I think both can be addressed without duplicating the code:

1. We must make sure that the type in the original signature is abstract. (Why? I'm not sure. But let's not try to fix that today.)
2. We must allow variables to be used from the environment.

It seems relatively easy to accommodate both (1) and (2) with an extra parameter passed to merge_constraint, saying whether we're in a package type. For (1), we just do an extra check. For (2), we skip the TyVarEnv.reset() in transl_with_constraint. If that runs into trouble, then maybe merge_constraint decides between calling transl_with_constraint and the new transl_package_constraint (which I'm not bothered by, because it's so short).

It's possible there will be more obstacles on this path. I'm just concerned by duplicating so much code here. Also happy to chat about this live this afternoon, say.

I fairly strongly disagree. Maybe that would work, maybe it would not. (In practice I did try deleting the TyVarEnv.reset call you mention and that's not enough to get the correct tyvarenv. I did not deeply investigate why, but this contributes to my view that the old approach is very confusing and is best to ditch.)

But even if we could easily additionally parameterize merge_constraint, I think the approach I've proposed here is much better! I believe this PR considerably clarifies how package with constraints work. The old approach, of constructing a fake bit of parse tree (Bad!) and having a bunch of subtle special cases, was pretty confusing. It took me quite a while to work out what is allowed and what is not allowed for package constriants. In the new version, that's it's own function and you can just read it.

If the aim is to merge the merge_constraint function, an option that could probably work would be to add a With_type_package variant to the with_info type which takes a typed type declaration rather than a parsetree fragment. Then merge_package_constraint could be:

let merge_package_constraint initial_env loc sg lid cty =
  let _, s = merge_constraint initial_env loc sg lid (With_package_type cty) in
  s

(A dirty implentation is visible at 7c0ebd3)

However, I have mixed feeling about this idea: yes, the complex code of merge_constraint is shared, but this code is complex because it is mixing multiple functions with a small common spine. Thus I am not completely sure if this version is simpler than the version which is extracting the simple package type case from the chimeric aggregated function.

If the aim is to merge the merge_constraint function, an option that could probably work would be to add a With_type_package variant to the with_info type which takes a typed type declaration rather than a parsetree fragment.

I like this idea! It nicely isolates the behavior of package with type constraints so it's less spread out in special cases of merge_constraint and transl_with_constraint, and eliminates the need to construct fake parse tree. I will give it a try.

I have pushed a commit implementing @Octachron's idea.

Compared with his draft, I made a few changes:

1. I made a separate case in merge_constraint for With_type_package, rather than combining it into the With_type/With_typesubst case. I think this is clearer, even if it results in a couple duplicated lines.
2. I changed merge_constraint to only conditionally return the typed tree with_constraint (by returning an option). This constraint was unused and slightly nonsense in the With_type_package constraint case, so this seems clearer.
3. I kept the requirement that package with constraints only work on type declarations without manifests. A nice thing about his version is that we could potentially allow updating manifests with compatible definitions, but I believe this will require more thought around row variables (or at least more work to get good error messages in those cases), so I propose to leave it as future work. I have added a few more tests of this type. (Note this PR preserves today's behavior, it just gives it a clearer error message.)

I agree with @Octachron that there are trade offs here - the old version was maybe a little clearer by having two separate functions rather than combining them into one just to avoid duplicating the "common spine". But I think this approach is probably the best compromise, eliminating the need to build fake parsetree without duplicating too much code.

I am wondering if we want to share this logic for module aliases with merge_constraint by having a common update_module function. (I meant the special on Mty_alias _).

A nice idea, but I found it a little tricky to do cleanly because the merge_constraint code also checks which sort of constraint we have, here. (Though I confess I do not entirely understand why it does so.)

I think it may be useful in order to be future proof to test the private row case:

(* Ghosts haunted type definitions *)
module type Private_row = sig
  type a
  and t = private [< `A | `B ]
  and b
  and d = private [< `C ]
 end
 (* This is fine, the ghost type `t#row` is removed silently *)
 module type Test = Private_row with type t = [ `A ]
 (* This fail currently, but make sure that if no ghost appear here)
 type fail = (module Private_row with type t = [ `A ] )

Good idea - test added.

Extremely minor nitpicking (because I have the context in mind): the global error reporter currents prints error message inside a b box (@[%t@]), thus opening a second box inside the message has currently no effects at all and it might be better to avoid it.

Indeed - fixed.

Since we are by construction not in the destructive substitution case of the signature patching , maybe:

let return replace_by =
      Some ((), {Signature_group.ghosts; replace_by=Some replace_by})

?

Good point - I agree that is clearer, and have changed it.