Fixing the limitations on destructive substitutions

[v-gb]

With trunk, one cannot write any of the following:

module type S2 = S1 with type t := int * int
module type S2 = S1 with type 'a t := int
module type S2 = S1 with type M.t := int

because the type being removed must be at the root of the signature and be replaced by a type constructor applied to the exact same parameters.

This pull request lifts these limitations, by allowing the same substitutions as non-destructive
substitutions, except I disallow substituting types defined inside modules that are aliased later in the signature:

sig
  module M : sig type t end
  module M2 = M
end with type M.t := int

as I didn't know whether that should be an error, or should substitute through the alias, or expand the alias and substitute inside of it. I doubt it matters in practice, so I went with the error.

It should be pretty clear why fixing these limitations is good: it's useful, it makes the language more regular because it's expected to work by analogy with non-destructive substitutions, working around it is annoying and makes type errors worse by introducing irrelevant names.

What's not done (for now):

• manual changes
• proper ocamldoc fix
• Changes entry
• sorting out the Obj.size hack. I think I'm working around a bootstrapping issue?
• sorting out the bug described below

Now, about the implementation:

I chose to make Subst extensible through some ad-hoc callbacks. It's simple, at least.
I thought of not using subst, but it looks like nothing else in the typer knows how to copy types.
I also thought of making subst support replacing type constructor applications by type declarations, but the dependencies in the typer look awkward if we do that. Also, it forces to write code to compose substitutions containing these new cases, even though it's dead code. Finally, it forces to extend subst to supports rewriting paths instead of idents, which may not be that simple, and bumps against the problem of how to do the substitution of M.t -> int in module B = M? At least with the current solution, this resolution is in Typemod, next to the problem.

There's one bug left:

module type S = sig
  module type S1 = sig type t type a val x : t end
  module M1 : S1
  type a = M1.t
  module M2 : S1
  type b = M2.t
end with type M1.a = int and type M2.a = int and type M1.t := int;;

is rewritten wrongly (look at the last val x), because of duplicate Ident.t in the type when using 'with .. and .. and':

module type S =
  sig
    module type S1 = sig type t type a val x : int end
    module M1 : sig type a = int val x : int end
    type a = int
    module M2 : sig type t type a = int val x : int end
    type b = M2.t
  end

I'm relying on an invariant that the Idents bound in a signature are all different. Clearly it doesn't hold here, but I am not sure if this is simply not an invariant, or if it should be but it's broken temporarily?

[garrigue]

Let me look into that after ICFP.
Concerning the use of Obj.size in subst.ml, clearly it shouldn't be needed. You just have to bootstrap.
Also, I'm not completely convinced by the use of callbacks in subst.ml. At least, for path substitutions it would be natural to use a path map, like in env.ml.

[gasche]

(For anyone wondering, ICFP is between September 18th and September 24th this year, and Jacques is and has been doing an awful lot of organization work for it.)

[v-gb]

I tried using a path map in subst.ml, see trunk...sliquister:generalize-destr-subst3. I can clean up the history a bit and replace the current pull request, if you think it's better.

[lpw25]

With trunk, one cannot write any of the following:

module type S2 = S1 with type t := int * int
module type S2 = S1 with type 'a t := int
module type S2 = S1 with type M.t := int

I haven't looked at the patch yet but, depending on how much effort it is, I might suggest splitting the third case into a separate pull request, as it's soundness is much less clear than the other cases. All the existing uses of := succeed as long as the new type is a compatible replacement, whereas a nested type or module will probably have to fail if the containing module is referenced anywhere else in the module type for something other than a projection.

For example,

module F (X : sig type t end) : sig type t end = ...

module type S = sig
  module M : sig type t end
  val v : F(M).t
end

module type T = S with M.t := int

will need to be an error. Although:

module F (X : sig type t end) : sig type t = X.t end = ...

module type S = sig
  module M : sig type t end
  val v : F(M).t
end

module type T = S with M.t := int

should probably be allowed.

[v-gb]

I recommend that people read commit by commit, rather than the whole diff (but not for the branch with path maps, as I haven't cleaned up the history).
Deep destructive substitution is the last commit, so it's already separate from the rest.

About soundness, if you look at the third commit, you'll see that the typer already allows broken signatures (I haven't checked if this leads to segfaults). I left the behavior unchanged because I don't know what to do about it, but for the new kinds of substitutions, an error is returned instead.
The implemented check is essentially what you say: when removing M.N.x, I check the usage of M and M.N other than projecting from them, ie aliases and applicative functor types arguments. I didn't think of expanding away the functor application in the case where it doesn't type anymore, so that last example is rejected. It's not clear how I would implement it, as right now, the check and substitution are separate passes on the ast.

[v-gb]

I was asked a couple of days ago about why we can't write a type expression on the rhs of a destructive substitution. @garrigue, have you had a chance to take a look at this feature?

I rebased the feature, and switched the implementation to the one with path substitutions. Although while writing some of the changes, I saw that nondep_type/nondep_supertype implement a deep copy of types more simply that subst.ml, so perhaps that would be another way to go.

[garrigue]

Sorry, I knew that I had something on my plate, but couldn't find it anymore. I will look at this soon.

[garrigue]

Indeed, reusing the code for nondep_type could be a good idea. Are you thinking of a generalization similar to type_iterators? The dangerous part is touchy problems about sharing, and how to handle recursive types properly.

[v-gb]

I wasn't thinking of anything specific, I simply noticed that nondep_type does some kind of rewriting on types and doesn't use subst.ml for that, and so it could make sense to do the same here.
If the typer implemented some generalization of type_iterators that allows to rewrite types, I would have certainly tried using it before changing subst.ml.

[trefis]

I just ran into this issue again this morning.
After reading the discussion here I am unsure what the state of this PR is. Could the current implementation be merged if it was rebased or would it need to be rewritten as discussed in the last messages?

[v-gb]

Well, this pull request needs more than a rebase to be merged: it needs a review.

[garrigue]

Sorry to be dragging my feet on this one. It is going to be merged once I review it properly.

[garrigue]

Again, sorry for the long delay.
The formal decision was taken at the dev meeting in February, but I still had some qualms.
Not about the goal, which is clearly desired, but about the approach, in particular extensive changes to subst.ml for an application that was not originally intended.

After a final review, I think that the code in its current form is fine, and the design choices reasonable.
Namely, there are 3 functions that copy types in the compiler: Subst.typexp, Ctype.copy_rec and Ctype.nondep_type_rec. At one point, I thought that avoiding code duplication in the way it is done by Btype.type_iterators would be cleaner. However, they serve different goals: Subst was explicitly intended for substitution in modules, copy_rec for instantiation before unification, and nondep_type_rec for capture avoidance in the module system. The first 2 use Btype.save_desc to handle recursive types, while the last one uses a hashtable. Subst and nondep_type_rec handle modules and their components too, while copy_rec only handles types. As a result, while there is code duplication, it is not that big (only 2 real copies rather than 3), and the merging would be non trivial (need to generalize multiple aspects).

So, if for the time being we keep these implementations, the next question is which one to use for destructive substitutions. And there the natural answer is Subst, as this is really just a variant of its original goal (it was already used for simpler form of destructive substitutions, but this is not the main criterion). There is a bit of spaghetti in the need of a forward definition for type application, but this is getting frequent when introducing advanced features that do not fit in the original stratified implementation. Overall, the change are minimal and readable.

In conclusion, @sliquister , could you rebase the code, so that we merge it in trunk ASAP. 👍

[garrigue]

See my comment in the discussion.

[lpw25]

I was also in the process of reviewing this change. I'm pretty sure there are a couple of bugs as well as some tidying up that would be useful. So @garrigue could you hold off on the merge until I've finished reviewing it -- should be done today or tomorrow.

[v-gb]

@garrigue Thanks!

In addition to issues Leo may have uncovered, the bug in the initial description should still be present, so I need to take a look at that before the code gets merged.

[lpw25]

This is taking me a bit longer than I expected, but I've finished looking at the first part -- the commit that allows general expressions for type substitutions -- and thought I would report what I've found so far.

There are two main issues. The first is the assert false in Subst.type_path when the type is intended to be replaced by an expression. Currently only the call to type_path for a TConstr is protected from this, but there are other calls to type_path and they trigger the assertion. For example:

# module type S = sig
    type t = [ `Foo ]
    type s = private [< t ]
  end;;

# module type T = S with type t := [ `Foo ];;
Fatal error: exception File "typing/subst.ml", line 103, characters 23-29:
  Assertion failed

or:

# module type S = sig
    type t
    type t += T
  end;;

# module type T = S with type t := int;;
Fatal error: exception File "typing/subst.ml", line 103, characters 23-29:
  Assertion failed

That first example (and a couple of other cases like it) can be fixed by simply dropping the path in question because it is only used for printing anyway. The second example would be addressed by #1253 as long as the substitution used Type_path whenever possible. (As a side note I would prefer Type_expr to Type_function for the name of the constructor in Subst).

The second problem is the use of Ctype.apply with an empty environment. Whilst this is ok for simple cases it doesn't work in general. For example,

# type ('a, 'b) foo = Foo;;

# type 'a s = 'b list constraint 'a = (int, 'b) foo;;

# module type S = sig
    type 'a bar = (int, 'a) foo
    type 'a t
      constraint 'a = (int, 'b) foo
    val x : string bar t
end;;

# module type T = S with type 'a t := 'a s * bool;;
Fatal error: exception Ctype.Cannot_apply

I'm less sure what to do about this case. Tracking the environment during substitution would be a major pain and damage performance. I think that probably we would need to ban type expression substitution for type definitions which have constraints. Then the parameters would be guaranteed to be simple type variables and could be substituted using link_type rather than a full unification. This would probably also allow us to avoid having Subst call a function from Ctype since the simpler version of apply required when the parameters are garuateed to be variables (and everything is guaranteed to be at generic level) could probably be in Btype.

[v-gb]

Ok, I think I follow your first point. #1253 would make the following code ill-typed

sig
  type t
  type t += T
end with type t := int * int

so we can assume that if an extensible type constructor is substituted, it's only by a type constructor with the same parameters?

For the second problem, it doesn't seem necessary to have an environment, because the constraints on the type constructor and the type expression are checked to be identical. Litteraly replacing string bar t by string bar s * bool should work without doing any unification. Now, I don't know if there is a function that does that in the typer.

[garrigue]

I'm not sure what is going wrong here. It should be OK for unification to assume that all undefined types are abstract, and in that case the above case should not fail, so I'm a bit confused.
Concretely, at this point constraints are already enforced, so that the problem is completeness, not soundness.
This said, I believe that unification might still fail for lack of some type abbreviations. We could use the outside environment, rather than just empty.

[lpw25]

For the second problem, it doesn't seem necessary to have an environment, because the constraints on the type constructor and the type expression are checked to be identical

For my above example the parameter of the substituting expression is something like:

(int, 'b) foo

and the body of the substituting expression is something like:

(int, 'b) foo list * bool

The 'bs are guaranteed to be physically equal so we can instantiate the expression by unifying the applied arguments with the parameters, which will mutate the 'b appropriately. However this requires the local environment since you cannot know what 'b will unify with without the definition of bar. As you suggest, you might try to directly mutate the parameter however I don't think there is any guarantee that the foo node in the parameter is physically equal to the foo node in the body. With a bit of effort we can also get examples where only the 'b and not the foo are present in the body:

type 'a foo = Foo

class c = object end

type 'a s = [ `Foo of 'b ] constraint 'a = 'b foo

type 'b r = [ `Foo of 'b | `Baz of 'b ]

module type S = sig
    type ('a, 'b) bar = 'a foo
    type 'a t
      constraint 'a = #c foo
    val x : (< foo: string >, < foo: bool >) bar t
end

module type T = S with type 'a t := [ 'a s | #c r ]

Here the parameter for the type expression is:

(< .. > as 'b) foo

and the body is

[ `Foo of <..> as 'b | `Baz of <..> as 'b ]

so just trying to mutate the parameter will not produce the correct body. The correct resulting type for T is:

sig
  type ('a, 'b) bar = 'a foo
  val x : [ `Foo of < foo : string > | `Baz of < foo : string > ]
end

however if we changed bar's definition to:

type ('a, 'b) bar = 'b foo

then the correct resulting type would be:

sig
  type ('a, 'b) bar = 'b foo
  val x : [ `Foo of < foo : bool > | `Baz of < foo : bool > ]
end

which demonstrates the need for an accurate environment.

[garrigue]

I see 3 solutions to this problem of substituting constrained types:

• Check beforehand that this doesn't happen, and fail when one tries to do that. Also, this means keeping the original behavior if we are substituting with a path, for backwards compatibility.
• Catch the error in apply, and give a proper error message. Not 100% compatible, but this might be ok. We can also use the external environment rather than empty, but this only stones half of the problem.
• Do the right thing, computing correct environment. This only needs to be done when doing a destructive substitution, so the cost is not a problem. But the coffee becomes spaghetti...

For now I believe that the first one is the best, as it doesn't remove any option for the future.

[lpw25]

I think that the best solution is to prevent using type expressions in destructive substitution when the type has constrained parameters. This is similar to your first option but has a clearer, less implementation-dependent criteria for rejecting these substitutions.

With this restriction the parameters are guaranteed to be type variables and so can be mutated directly with link_type avoiding unification and the need for an environment.

[lpw25]

Another possibility would be to have a separate set of functions for doing destructive substitutions that preserve the environment. This would mean having another set of functions for traversing types, but it would separate the potentially failing substitutions associated with these more expressive destructive substitutions from the normal substitutions used the rest of the time.

[lpw25]

In particular, using a separate set of functions for destructive substitution would allow the additional checks for type M.N.t := ... and module M.N := ... to be done during the substitution rather than as a separate check.

[garrigue]

So what you are suggesting is my option 1, but willingly breaking backward compatibility?
There is a drawback: it becomes impossible to erase type definitions with constrained parameters.
I'm afraid this is a real regression in practice.
Also, after checking that the parameters are not constrained (i.e. all distinct type variables), it is fine to use Ctype.apply, since unify just does link_type then.

By the way, I'm not sure what you mean by "destructive substitutions that preserve the environment".

[lpw25]

So what you are suggesting is my option 1, but willingly breaking backward compatibility?

No, it would only restrict destructive substitutions if they are using a general type expression rather than a type path. So all existing ones would work but the new more relaxed substitutions wouldn't be available for constrained types.

it is fine to use Ctype.apply, since unify just does link_type then

Sure, I just have a slight preference for using a specific function for this restricted case to make it clearer what invariant is being relied upon rather than just passing Ctype.apply an empty environment because it happens to work.

By the way, I'm not sure what you mean by "destructive substitutions that preserve the environment".

Sorry, bad writing on my part. I meant that the separate set of functions would preserve the environment. I now think this is the best option. There are enough awkward corners around these more expressive destructive substitutions that I think they justify having their own functions rather than using Subst. I think we should add a new module (destructsubst.ml?) that includes an implementation of substitution whilst maintaining an accurate environment and performing the checks needed for type M.t := ... substitutions. We could also move the merge_constraints functions from typemod.ml there.

[v-gb]

There is no particular advantage to changing the signature of Subst.add_{type,module}, so I reverted these changes.

[yallop]

module type S2 = S1 with type 'a t := int

It'd be useful to be able to write with type _ t := int, which is currently disallowed, here.

[v-gb]

Indeed. In fact, I'm surprised that with type _ t = int is rejected in the parser.
But perhaps it's preferable to have this pull request only make destructive substitutions support the same right hand sides as plain substitutions, and then support underscores in a subsequent pull request for both kinds of substitutions.

[gasche]

@garrigue is this ok for merging now?

[garrigue]

It's ok with me, if @lpw25 has nothing to add.
This is a "new" feature, so I'm not too concerned by rough edges, as long as it is sound and has no regressions.

[lpw25]

I've added a couple of small comments inline. There are also two larger issues:

1. merge_constraints only calls check_usage_of_path_of_substituted_item on the parts of the signature after the definition. However, with e.g. recursive modules there can be references earlier in the signature as well.

2. Similarly, the environment created by merge constraints only contains items from earlier in the signature, however items from later in the signature may be referenced as well. Since this is the environment used for calls to check_usage_of_path_of_substituted_item it can produce false positives.

You can probably ignore the second point in this PR, as it's actually a preexisting bug in merge_constraints. For example, in 4.04.1:

# module type S = sig
    module rec M : sig
      type t = N.t
    end
    and N : sig
      type t = int
    end
  end;;
              module type S =
  sig module rec M : sig type t = N.t end and N : sig type t = int end end
# module X = struct type t = int end;;
module X : sig type t = int end
# module type T = S with module M := X;;
Characters 16-36:
  module type T = S with module M := X;;
                  ^^^^^^^^^^^^^^^^^^^^
Error: In this `with' constraint, the new definition of M
       does not match its original definition in the constrained signature:
       Modules do not match:
         sig type t = int end
       is not included in
         sig type t = N.t end
       Type declarations do not match:
         type t = int
       is not included in
         type t = N.t

This PR provides a new symptom of this bug, but it doesn't really cause it.

However, the first point is solely the responsibility of this PR and should really be fixed.

[lpw25]

This call to type_path seems pointless since we already have the path as the argument to Path _.

[lpw25]

Depressingly this assert false can be triggered due to MPR#7611. I wouldn't bother changing it, but thought I should probably mention it.

[lpw25]

It seems that strict is always true at every call site. If so it should probably be removed.

[v-gb]

I should have addressed all of Leo's remarks (except the one in subst.ml which we talked about directly).

[lpw25]

Looks good to me. I'll merge this now and look at fixing the existing bug in merge_constraints in another PR.