I hope more knowledgeable people than me will offer an explanation, but after having looked briefly at the code it seems that we're indeed always "translating" the rhs of the constraint in the initial environment (i.e. the one just before the definition of the module type), and then checking that it is well-formed in the current environment.

That sort of makes sense to me, it's forcing the rhs of the constraint to refer only to things outside of the module type.

What I believe your patch does (if it was generalized to all the calls of transl_with_constraint) is to allow references to items that come before the one being constrained. I'm not sure that something we'd want.

Now, what's really surprising me is that in your example, t is supposed to exist in initial_env. So where does the Not_found come from? (Furthermore, my impression is that the new t shouldn't exist in env yet. But I probably misread that part)

Being a bit imaginative, here is a proposed explanation (but I am not sure it matches the code): mod with type t = foo and type u = bar is evaluated by iterating two calls to merge_constr (in the Pmty_with of transltype_mod_aux), as (mod with type t = foo) with type u = bar. During the first call (with t = foo), we end up with a signature where t is replaced by a new type declaration that is not part of the environment. So then when we process the second constraint with type u = bar, if bar mentions t we have a problem.

I agree with @trefis. t and ind should both be in the initial environment. The type definitions that the with constraints are applying to are in Sig and should be unrelated to the ones that are being looked up that come from the preceding include.

Here is a reproduction case for a similar problem with variance instead of separability:

module type Sig = sig
  type +'a abstract
  type +'a user = Foo of 'a abstract
end

module type Problem = sig
  include Sig
  module M : Sig
    with type 'a abstract = 'a abstract
     and type 'a user = 'a user
  type +'a foo = 'a M.user
end

11 |   type +'a foo = 'a M.user
       ^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this definition, expected parameter variances are not satisfied.
       The 1st type parameter was expected to be covariant,
       but it is injective invariant.

I was amused to trace the introduction of the initial_env vs. env usage back to @xavierleroy's df42185 in 1996. Yet another person who may be able to shine light on this issue.

@xavierleroy's df42185 in 1996. Yet another person who may be able to shine light on this issue.

24 years later, I'm afraid not. But @trefis 's explanation above (#9623 (comment)) feels very plausible to me: the right-hand sides must be defined in the initial environment but must still make sense when brought into the new signature. How this explains the loss of variance of separability info, I don't know.

I now propose a fix that feels more correct and more complete to me. Reviews would be very welcome -- this bug is causing a regression in at least the Jane Street codebase for 4.11.

There was something fundamentally flawed with the idea that we would type-check a definition in an environment, but then we could only check its well-formedness in a richer environment.

I think that the problem was that the initial_env should be used to type-check the right-hand-side of the constraint, but not to recompute declaration properties which depend on type_kind (in particular the variant/record declaration) which is only valid in the signature environment env. The proposed patch passes both environments to Typedecl.transl_with_constraint, and tries to use either one when appropriate.

I think that the problem was that the initial_env should be used to type-check the right-hand-side of the constraint, but not to recompute declaration properties which depend on type_kind (in particular the variant/record declaration) which is only valid in the signature environment env. The proposed patch passes both environments to Typedecl.transl_with_constraint, and tries to use either one when appropriate.

I'm not sure I understand this reasoning.
The right-hand side of a constraint is defined only using the original environment.
So I don't see why you would need to refer to the signature environment in it.
Basically, in a constraint you cannot refer to anything from the signature you are modifying.

Also, your scenario doesn't seem to make sense: even if the signature contains a type t, it will not be seen from the right-hand sides. The only place where the two environments interact is check_type_decl, but it only checks subsumption, and is already called with the right environment (env subsuming initial_env for paths).

I agree that your variance code demonstrates a bug, and I'm going to look into this.

@garrigue The problem that @gasche is getting at is that we pass not just the right-hand side of the constraint but also the definition from the signature to transl_with_constraint as orig_decl. The type_kind and type_param fields from that declaration are both used with operations that depend on the environment -- so they either need to be given the inner environment of the signature, or we need to stop using them.

I should probably also point out that the "internal" environment calculated by merge_constraint is also incorrect as it ignores recursion. The big red flag is that it calls Env.add_item which is always a mistake. You'll probably find that:

module type Sig = sig
  type +'a user = Foo of 'a abstract
  and +'a abstract
end

module type Problem = sig
  include Sig
  module M : Sig
    with type 'a abstract = 'a abstract
     and type 'a user = 'a user
  type +'a foo = 'a M.user
end

is broken even with your patch.

I should probably also point out that the "internal" environment calculated by merge_constraint is also incorrect as it ignores recursion. The big red flag is that it calls Env.add_item which is always a mistake.

I see the problem. In this case this could be solved by using an environment with the full signature, rather than expanding it incrementally. In general, like for functors, the variance (and other mutually recursive properties) should be computed on the final signature, after all substitutions are done. But maybe this last part can be delayed until we do it for functors.

@lpw25 I understand what you mean and I might see how to go in a direction of fixing this problem (rewrite merge_constraint to work on each recursive group separately), but it seems orthogonal to the aspect that I am attacking in the present PR (I propose to pass the signature environment to the call, and you propose to compute a better signature environment). Would you like to propose a separate fix for that part?

Example of problem with type_params:

module type Sig2 =
  sig type 'a u = 'a list type +'a t constraint 'a = 'b u end
type +'a t = 'b constraint 'a = 'b list
module type Sig3 = Sig2 with type 'a t = 'a t

@gasche The problem @lpw25 describes is that, if you're calling transl_with_constraint with an incomplete environment, you may still get the same kind of errors for mutual recursion. So I would say this is part of the same bug. But this can be easily fixed by first computing an environment extended with whole signature, and then incrementally overwriting it with the constrained definitions. I.e., you just need to add one line in merge_constraints.

@garrigue I pushed a new commit that changes the place where the type_params are unified, and in fact reduces the diff a bit thanks to (judicious? dangerous?) use of a shadowed env variable. Let me know what you think.

I needed to tweak your example slightly to get it to compile in my fixed version. As it is written, with my commit it fails with the following error:

module ParamsUnificationEnv = struct
   module type Sig =
    sig type 'a u = 'a list type +'a t constraint 'a = 'b u end
   type +'a t = 'b constraint 'a = 'b list
   module type Sig2 = Sig with type 'a t = 'a t
 end
 [%%expect{|
Line 5, characters 21-46:
5 |   module type Sig2 = Sig with type 'a t = 'a t
                         ^^^^^^^^^^^^^^^^^^^^^^^^^
Error: In this `with' constraint, the new definition of t
       does not match its original definition in the constrained signature:
       Type declarations do not match:
         type 'a t = 'a t constraint 'a = 'b u
       is not included in
         type +'a t constraint 'a = 'b u
       Their variances do not agree.
|}]

Two changes make this compile: I can drop the variance annotations

  module type Sig =
    sig type 'a u = 'a list type 'a t constraint 'a = 'b u end
  type 'a t = 'b constraint 'a = 'b list
  module type Sig2 = Sig with type 'a t = 'a t

or I can define type +'a t = b in the first Signature as well:

  module type Sig =
    sig type 'a u = 'a list type +'a t = 'b constraint 'a = 'b u end
  type +'a t = 'b constraint 'a = 'b list
  module type Sig2 = Sig with type 'a t = 'a t

Hm, it also works with with type +'a t = 'a t.

  module type Sig =
    sig type 'a u = 'a list type +'a t constraint 'a = 'b u end
  type +'a t = 'b constraint 'a = 'b list
  module type Sig2 = Sig with type +'a t = 'a t

@gasche My proposed solution would be what Jacques said: use Env.add_signature before entering a signature and remove the call to Env.add_item.

Hm, it also works with with type +'a t = 'a t

Does that actually check the variance? Once upon a time I submitted a bug report that it didn't, and I do not recall the outcome.

Does that actually check the variance? Once upon a time I submitted a bug report that it didn't, and I do not recall the outcome.

Since the call in transl_with_constraint has ~check:true I would expect it to.

I pushed a new commit that computes and uses full_env in the way @lpw25 and @garrigue suggested. (merge does not need an env parameter anymore.)

Note: I just confirmed that the regression tests proposed by @garrigue (for constraints / type_params unification) and @lpw25 (for Env.add_item) are indeed failing with the initial version of the patch.

Note that removing the env parameter to merge is not strictly equivalent: a constraint may result in an improved variance / immediacy / separability, that could be used in other definitions. On the other hand, this would be propagated to other type definitions only in a semi-arbitrary way (i.e. only propagate to following constraints, leaving unconstrained types unchanged, and no fixpoint computation).

Actually, the correct code for constrained parameters is a bit different. I will send you a patch in 1 minute.

The point is that unifying the parameters is the main cause to get inconsistent constraints, so this is better to delay the unification until after we have unified the params.

If I understand correctly, you are proposing to do the more-likely-to-fail unification first. Could we document the reason for this? (It makes the code more complex.) Is the idea that we get better error messages because they are expressed in terms of the type parameters, rather than the type expressions coming from constraint processing?

Secondary question: we have a few check under a if arity_ok test, which in particular avoids exceptions due to length mismatches in List.{map2,iter2}. I would suppose that we should also fail if the arities are distinct, but I don't see this anywhere in this function. Is there a check for this somewhere else, or do we support changing the arity in a constraint?

The point is that unifying the parameters is the main cause to get inconsistent constraints, so this is better to delay the unification until after we have unified the params.

If I understand correctly, you are proposing to do the more-likely-to-fail unification first. Could we document the reason for this? (It makes the code sensibly more complex.) Is the idea that we get better error messages because they are expressed in terms of the type parameters, rather than the type expressions coming from constraint processing?

Ok, maybe my explanation was not clear. This is the opposite. The goal of unifying the parameters before the constraints is to have unification fail on constraints rather than on parameters. The role of the unification on parameters is to inherit constraints from the original declaration, avoiding having to redeclare constraints by hand. Then, constraint unification will fail if the is a contradiction between the constraints in the original declaration and those added in the with .. = ... constraint ... = ... construct. If we do it the other way round, the error will be located on the parameter rather than on the constraint. Both are correct, just this way gives better locations for error messages.

Secondary question: we have a few check under a if arity_ok test, which in particular avoids exceptions due to length mismatches in List.{map2,iter2}. I would suppose that we should also fail if the arities are distinct, but I don't see this anywhere in this function. Is there a check for this somewhere else, or do we support changing the arity in a constraint?

After calling transl_with_constraint, there is a call to check_type_decl, which in turn calls Includemod.type_declarations, so the arity will eventually be checked. The idea is to get more uniform error messages. Constraints will also be checked again at that point (in particular, they cannot be more restrictive than in the original declaration). The only reason we may fail on constraints in transl_with_constraint is because we want to inherit constraints (and type_kind) from the original declaration.

At this point, you may have correctly deduced that writing parameter constraints in with constraints is actually pointless, since anyway you can only inherit the original constraints, and cannot even refine them. I think this is only allowed for backward compatibility reasons (originally there was no constraint inheritance, and there was really no need for sig_env). This may also be clearer in some cases.

Thanks for the explanation. I did as you recommend, delaying the constraint unification to after the parameter unification, with an explanatory comment. That said, I would rather be in favor of doing the constraint unification first, to get simpler code, especially since you explain that using constraints there is in fact useless.

The diff I propose looks like this:

     List.map (fun (ty, ty', loc) ->
       let cty = transl_simple_type env false ty in
       let cty' = transl_simple_type env false ty' in
-      (* Note: We delay the unification of those constraints
-         after the unification of parameters, so that clashing
-         constraints report an error on the constraint location
-         rather than the parameter location. *)
+      begin
+        try Ctype.unify_var env cty.ctyp_type tparam
+        with Ctype.Unify tr ->
+          raise(Error(cty.ctyp_loc, Inconsistent_constraint (env, tr)))
+      end;
       (cty, cty', loc)
     ) sdecl.ptype_cstrs
   in
@@ -1424,14 +1425,6 @@ let transl_with_constraint id row_path ~sig_env ~sig_decl ~outer_env sdecl =
       with Ctype.Unify tr ->
         raise(Error(cty.ctyp_loc, Inconsistent_constraint (env, tr)))
     ) tparams sig_decl.type_params;
-  List.iter (fun (cty, cty', loc) ->
-    (* Note: contraints must also be enforced in [sig_env] because
-       they may contain parameter variables from [tparams]
-       that have now be unified in [sig_env]. *)
-    try Ctype.unify env cty.ctyp_type cty'.ctyp_type
-    with Ctype.Unify tr ->
-      raise(Error(loc, Inconsistent_constraint (env, tr)))
-  ) constraints;

Thanks! (I gather that you are not in favor of doing the constraint unification earlier to simplify the code?)
I'll try to merge this soon (currently the CI is failing) to go back to 4.11 testing.

The CI failure is due to a test that was previously failing, and now passes, in tests/typing-sigsubst/sigsubst.ml:

(* Valid substitutions in a recursive module may fail due to the ordering of
   the modules. *)

module type S0 = sig
  module rec M : sig type t = M2.t end
  and M2 : sig type t = int end
end with type M.t = int
 [%%expect {|
-Lines 1-4, characters 17-23:
-1 | .................sig
-2 |   module rec M : sig type t = M2.t end
-3 |   and M2 : sig type t = int end
-4 | end with type M.t = int
-Error: In this `with' constraint, the new definition of M.t
-       does not match its original definition in the constrained signature:
-       Type declarations do not match:
-         type t = int
-       is not included in
-         type t = M2.t
+module type S0 =
+  sig module rec M : sig type t = int end and M2 : sig type t = int end end
 |}]

Please correct me if I'm wrong, but my understanding is that this is a welcome change, an improvement due to @lpw25's suggestion to use the whole signature to check the with-constraint.

The CI failures seem spurious: I compiled this PR rebased on top of trunk, and make all-typing was all green.

Well I rebased the PR to fix the CI failures, so if you observed the current state of the branch it is natural that it would work. (But I'll still wait for the CI results to merge, and cherry-pick to 4.11.)

I believe I pulled and rebased before you pushed the new version (i.e. I had to rebase myself), but I may have missed something.

Merged, and cherry-picked in 4.11 ( 003dd39 ).