#13388: local module type substitution can fail by Octachron · Pull Request #13540 · ocaml/ocaml

Octachron · 2024-10-10T13:15:09Z

Local substitutions for module types

module type t := sig end

or

s with module type t := sig end

may fail to produce well-formed types when trying to substitute a module type path inside the type of first class module, for instance

module type s = sig
  module type t := sig end
  type u := (module t)
end

Before this PR, the part of Typemod module handling the erasure of local substitution was tracking independently whenever a substitution could be applied safely or not on a type expression. However, this logic was incomplete and did not cover correctly the composition of substitutions.

Rather than extending this logic as proposed in #13524, this PRs introduces an alternative (and easier to maintain) approach which splits substitutions from the Subst module in two variants belonging to the same type family and distinguished by a phantom type parameter:

standard substitutions that are guaranteed to succeed
local substitutions that may fail

With this two types, the definition of substitution composition is defined in one place the Subst module.
Local substitutions are created by adding a generic module type substitution to a substitution and
applying a local substitution require to handle the failure case.

With this change, the Typemod module can use the new local substitutions to detect whenever a substitution fail to create a well-formed type.

module type s = sig
  module type t := sig end
  module type r := t
  type s := (module r)
end

4 |   type s := (module r)
     ^^^^^^^^^^^^^^^^^^^^
Error: The module type "r" is not a valid type for a packed module:
      it is defined as a local substitution (temporary name)
      for an anonymous module type. (see manual section 12.7.3)

without affecting the rest of the typechecker.

Local substitutions for module types ``` module type t := sig end ``` or ``` s with module type t := sig end ``` may fail when trying to substitute the module type path inside the type of first class module. Before this commit, the `Typemod` logic was duplicating part of the substitution composition logic to detect those failing substitutions in advance but failed to detect many cases. This commit introduces an alternative (and easier to maintain) approach which splits substitutions in two types belonging to the same type family: - standard substitutions that are guaranteed to succeed - local substitutions that may fail With this change, `Typemod` can use local substitution without affecting the rest of the typechecker.

gasche · 2024-10-10T15:28:32Z

+
+  val compose: local -> local -> local res
+  (** Due to the eager nature of composition for module types, composition of
+      local substitution may fail. *)


The way I read this is "this may be eager, and so it may fail". But as a user, I may want the guarantee that this is eager, so that it fails in my code when I expect it to fail. (The alternative in some cases is not to fail later, but to never fail because some ill-formed types appear during composition but not in the final result.)

gasche · 2024-10-10T15:29:26Z

The design looks nice and I feel much better about this approach.

Silly question: what is a "local" substitution, why are those substitutions called local?

Octachron · 2024-10-10T15:34:28Z

The "local substitution" name is the one used in the manual for

type t := int * float

to convey the point that those substitutions only exist inside the local scope of the module. I agree that the name doesn't completely fit in the context of the typechecker code.

gasche

Curiosity question: is there an interface to substitute module names with non-path structures? If yes, where can it be found? How is the validity of the result checked?

gasche · 2024-10-10T19:14:23Z

+(** Standard substitution*)
+
+type local = [`local] s
+(** Local substitution *)


Naming proposal: some substitutions are "safe" (they always preserve well-formedness of the objects they operate on), some are "unsafe" (they may introduce ill-formed terms, which are detected at runtime). (Gets rid of "local" here, which is good).

Unsafe was the first name of those variants, I have reverted the interface to this naming scheme.

On reading the file below, I find unsafe a bit unclear, I would prefer unsafe_subst or just [`Unsafe] subst. Maybe just type safe = [`Safe], and then safe subst?

Nitpick: now you define type unsafe but there is no corresponding type safe alias, which could be slightly annoying for someone who would want to use this type explicitly. Could you introduce a safe type?

gasche · 2024-10-10T19:16:25Z

+  Path.t -> params:type_expr list -> body:type_expr -> 'a s -> 'a s
+val add_module: Ident.t -> Path.t -> 'a s -> 'a s
+val add_module_path: Path.t -> Path.t -> 'a s -> 'a s
+val add_modtype_id_to_path: Ident.t -> Path.t -> 'a s -> 'a s


Naming proposal: add_modtype : Ident.t -> Path.t -> 'a s -> 'a s. It is only safe to expand a module type to a path, so it makes to name this as the canonical substitution operation for module types, as we are doing for modules above.

I have aligned those function names to the one used for modules.

Octachron · 2024-10-11T08:25:35Z

Module substitutions are limited to path substitutions and this is one of the main difference between open struct ... end and local substitutions.

lpw25 · 2024-10-11T10:19:44Z

I think I would expect add_type_path, add_module_path and add_modtype_path as they can also produce ill-formed results. I also think it might be worth considering splitting out all of the unsafe ones out into an entirely separate type. They add a bunch of complexity to Subst and Subst is one of the most important operations for the performance of the type-checker. Having a simple and efficient Subst module that defines syntactic substitutions, and then a separate, less performance sensitive, more complicated file than defines the many ad-hoc things that := syntax allows might be a cleaner approach.

Octachron · 2024-10-14T12:59:16Z

Moving all module type editing functions to the Unsafe submodule felt like a good idea to expose the point that they are now exactly standard substitutions. I have done so.

This introduces a small amount of "noise" in the current state because some checks for recursive modules also use add_type_path.

Having a separate full modules sounds like an interesting avenue to investigate, at least if we can keep code duplication to a minimum. However, my opinion is that it is probably better to fix the current bug now, and explore this idea as a subsequent refactorisation later.

gasche · 2024-10-14T13:34:46Z

  when two local substitutions are incompatible (for instance `module type
  S:=sig end type t:=(module S)`)
-  (Florian Angeletti, report by Nailen Matschke, review by Gabriel Scherer)
+  (Florian Angeletti, report by Nailen Matschke, review by Gabriel Scherer, and


I would remove the oxford comma, we don't do usually that in the Changes file.

The use of the oxford comma varies quite a lot within the Changes file.

gasche · 2024-10-14T13:37:35Z

+(** Standard substitution*)
+
+type local = [`local] s
+(** Local substitution *)


On reading the file below, I find unsafe a bit unclear, I would prefer unsafe_subst or just [`Unsafe] subst. Maybe just type safe = [`Safe], and then safe subst?

gasche · 2024-10-14T13:38:39Z

+  val add_type_path: Path.t -> Path.t -> 'k subst -> 'k subst
+  val add_type_function:
+    Path.t -> params:type_expr list -> body:type_expr -> 'k subst -> 'k subst
+  val add_module_path: Path.t -> Path.t -> 'k subst -> 'k subst


I find it confusing that these functions are in Unsafe, but their type remains safety-polymorphic. Did you just forget to return unsafe, or is the idea that it would break too much code so you prefer to brand them in the submodule without changing their type for now, or forever?

Oops, I forgot to change those types, the interesting point with this move is that it require very little changes.
Concerning, the name I would propose:

type unsafe = [`Unsafe] ... module Unsafe: sig type t = unsafe subst ... end

Yep, this is my favorite proposal as well.

gasche

I believe that the PR is correct and that it simplifies and improves the codebase -- besides fixing a bug. Approved.

gasche · 2024-10-15T12:25:34Z

+(** Standard substitution*)
+
+type local = [`local] s
+(** Local substitution *)


Nitpick: now you define type unsafe but there is no corresponding type safe alias, which could be slightly annoying for someone who would want to use this type explicitly. Could you introduce a safe type?

Octachron · 2024-10-15T12:49:50Z

I have added the safe type flag (and updated the documentation) while rebasing.

Octachron · 2024-10-17T09:29:09Z

As a bug fix, I am planning to cherry-pick the fix to 5.3 .

Octachron · 2024-10-23T13:56:54Z

Cherry-picked to 5.3 (542549a) since this is a bug fix.

…4224)

gasche reviewed Oct 10, 2024

View reviewed changes

Octachron added 2 commits October 11, 2024 10:11

review: names

25cf172

update Changes

705a516

gasche reviewed Oct 14, 2024

View reviewed changes

gasche approved these changes Oct 15, 2024

View reviewed changes

Octachron added 3 commits October 15, 2024 14:41

review: isolate all unsafe substitutions

e0d7cfc

self-review: document assert false

eb1f6d5

review: rename

0a01326

Octachron force-pushed the explicit_local_substitution branch from 582fc50 to 0a01326 Compare October 15, 2024 12:49

Octachron merged commit 4142635 into ocaml:trunk Oct 17, 2024

Octachron mentioned this pull request Oct 17, 2024

Fatal error: Subst.modtype_path when destructively substituting a packed non-path module type #13388

Closed

Octachron added a commit that referenced this pull request Oct 23, 2024

Merge pull request #13540 from Octachron/explicit_local_substitution

542549a

rtjoa added a commit to oxcaml/oxcaml that referenced this pull request Jun 27, 2025

local module type substitution can fail (backport ocaml/ocaml#13540)

cf6d700

rtjoa mentioned this pull request Jun 27, 2025

local module type substitution can fail (backport ocaml/ocaml#13540) oxcaml/oxcaml#4224

Merged

rtjoa added a commit to oxcaml/oxcaml that referenced this pull request Jun 27, 2025

local module type substitution can fail (backport ocaml/ocaml#13540)

facfc9b

rtjoa mentioned this pull request Jun 30, 2025

Better errors for illegal recursive modules (backport ocaml/ocaml#13646) oxcaml/oxcaml#4240

Merged

rtjoa added a commit to oxcaml/oxcaml that referenced this pull request Jul 2, 2025

local module type substitution can fail (backport ocaml/ocaml#13540)

17918f0

ccasin pushed a commit to oxcaml/oxcaml that referenced this pull request Jul 3, 2025

local module type substitution can fail (backport ocaml/ocaml#13540) (#…

4fe54d6

…4224)

ccasin pushed a commit to oxcaml/oxcaml that referenced this pull request Jul 5, 2025

local module type substitution can fail (backport ocaml/ocaml#13540) (#…

fee1098

…4224)

Conversation

Octachron commented Oct 10, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gasche commented Oct 10, 2024

Uh oh!

Octachron commented Oct 10, 2024

Uh oh!

gasche left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Octachron commented Oct 11, 2024

Uh oh!

lpw25 commented Oct 11, 2024

Uh oh!

Octachron commented Oct 14, 2024

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Octachron Oct 14, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gasche left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Octachron commented Oct 15, 2024

Uh oh!

Octachron commented Oct 17, 2024

Uh oh!

Octachron commented Oct 23, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Octachron commented Oct 10, 2024 •

edited

Loading

gasche left a comment •

edited

Loading

Octachron Oct 14, 2024 •

edited

Loading