Lazy strengthening

[rleshchinskiy]

This PR adds strengthening as a first-class concept to the module type language. The main motivation is faster module type checking but this also makes the language more expressive, allowing more programs to type.

New syntax

Suppose we have

module type S = sig type t end
module M : S

The actual type of M is stronger than S - it is sig type t = M.t end. The new extension allows this type to be written as S with M (in the literature, S/M is often used). This effectively strengthens all types in S with the information that they are equal to those in M.

Expressivity

Previously, strengthening happened by actually adding information to all types in a module type. This meant that abstract module types couldn’t be strengthened. Consider

module F (Y : sig module type A module X : A end) = Y.X

We now infer the functor (Y : …) -> (Y.A with Y.X) for F where previously, we only could infer functor (Y : …) -> Y.A, thus losing information. See ocaml/ocaml#12204 for more details.

Efficiency

The main benefit of the extension, though, is that it allows us to type check some programs much quicker. Consider the following example.

module type S = sig
  type t
  val x : t 
  <lots of value declarations>
end
module M : S = …
module F (X : S) = …
module N = F(M)

To type N, we have to check that the type of M is a subtype of S. With the new extension, this is simple: M gets the type S with M and S with M < S always holds so the check finishes very quickly. Previously, we would infer the (large) type

sig
  type t = M.t
  val x : t
   …
end

for M by unfolding S and strengthening it. When checking F(M), we would then match this type against S which requires unfolding S again and then comparing the individual signature items.

Unused warnings

Suppose that x in the above example isn’t actually used anywhere. With this PR, we will indeed issue an unused declaration warning. This wasn’t the case previously as x was (implicitly) used while typing F(M) since were unfolding S.

[mshinwell]

@rleshchinskiy what's happening with this PR? (please add a description too if it's staying open)

[rleshchinskiy]

@rleshchinskiy what's happening with this PR? (please add a description too if it's staying open)

It's waiting for @lpw25 to review it

[ccasin]

I think I am on the hook to review this now, and having merged unboxed floats I'm ready to do it soon.

@rleshchinskiy I've had a quick look and believe I understand the idea here, but I don't have all the context Leo does. What do you think about writing a little documentation? I don't need a detailed design or anything, but we'll have to write some kind of user-facing documentation about the new module type form anyway, and it'll probably be easier to review if I can read that rather than guess what it will say.

[ccasin]

OK, I've had a look through. Thanks for the many helpful comments.

I think there are a few issues and have some questions and suggestions - see below - but this looks like it's going to be a nice improvement.