Modular explicits

[samsa1]

First draft of modular explicit.

Currently labels are not supported and modes are also not handled.

More testing and code refactoring would need to be done in order to be production ready, thus this PR should not be merged !

However feel free to hack a bit with modular explicit in order to give feedback about syntax, GADTs filtering, typing bugs

[samsa1]

The current version should be able to pass tests however the type display is quite horrible. The implementation of shadowing display on the upstream version is much nicer to look which leads to better results with modular explicits.

[samsa1]

There is a bug related to layout that I've detected but haven't managed to fix yet.

On another notice an extension of modular explicit with labels is available at :
https://github.com/samsa1/flambda-backend/tree/modular-explicit-labels

[lpw25]

I've reviewed as far as unification. The main issue is that unification needs to enforce sharing between its inputs to ensure principality. This requires a change in how you are representing the identifiers that are bound by Tfunctor. It's really quite hard to find examples that this breaks -- I've included one in my comments -- but it is a fundamental part of how the type-checker works and I think your PR needs to respect it.

[lpw25]

Why not do the updates of env inside the call to enter_functor_for rather than remembering the old value and passing that in?

[lpw25]

I don't think it is a good idea to leave these identifiers in the environment after the unification is finished. They can't be looked up by name, so it's probably sound, but it's surprising and likely to lead to bugs in weird places. For example:

module type S = sig type t val plus : t -> t -> t end

type ('a, 'b, 'c) eq = Refl : ('a, 'a, {Norm : S} -> Norm.t) eq

let foo (type a) (e : (a, int, {M : S} -> M.t) eq) =
  match e with
  | Refl -> Norb.foo

currently gives:

File "foo.ml", line 7, characters 12-20:
7 |   | Refl -> Norb.foo
                ^^^^^^^^
Error: Unbound module Norb
Hint: Did you mean Norm?

with a hint that refers to a module that shouldn't be in scope. In general it is a good idea to be hygienic around issues of scoping.

[samsa1]

As the handling of the environment during unification is different on the upstream compiler this problem doesn't occur. However the method proposed below might be a good way to obtain a good result

[lpw25]

Here and in some other places you break the property that unification makes types physically equal -- so that future mutations of one input affect the other. This breaks OCaml's model of the world and, in particular, it's approach to ensuring principality.

For example, the following code is not principal, and triggers an ambiguity error upstream if you use -principal, but this branch gives no error:

type float2 = float

let forty_two : float2 = 42.0

type 'a ty =
  | Float : float ty
  | String : string ty

let bar (type a) p (ty : a ty) (a : a) =
  match ty with
  | Float ->
      let r = ref None in
      r.contents <- Some forty_two;
      let bar () =
        match r.contents with
        | None -> 3.5
        | Some x -> x
      in
      r.contents <- Some a;
      bar ()
  | String -> assert false

I think you need to change your approach slightly so that the identifiers bounds by Tfunctor nodes are mutable such that one can be mutated to be permanently considered equal to another. This would allow you to have unification continue to make types physically equal.

I even wonder if it might be better for these identifiers to be a separate type from Ident.t with their own constructor in Path.t and their own table in Env.t.

[samsa1]

Having their own table in Env.t would allow a simple fix to not keeping things in scope. Thus making it a separate type from Ident.t could be an efficient method.

[samsa1]

The problem of principality should now be solved due to the implementation of an unscoped type for identifiers that are unifiable.

[lpw25]

From a quick scan these latest commits look really good. I'm away next week, but I'll try to do a more thorough review of this the week after.

[lpw25]

I had hoped to get through this whole PR by now (ideally quite a lot before now), but I've still got ctype.ml and parts of typecore.ml to get through. I'm posting what I have now since I'm about to take a few days off, there are already plenty of comments and you've waited long enough.

[lpw25]

I think it should be pretty easy to support modes on these, and you'll need to so that you can give a most general type to functions with first-class module parameters. Here you just need to copy the mode stuff from the code just above.

[lpw25]

(Weird indentation)

[lpw25]

ret is a very confusing name for something that includes both the argument and the return type of the functor.

[lpw25]

The logic in this next section is a little convoluted. I think it could be simplified by doing things in two steps:

1. Inspecting the expected type and producing an expected type for the pattern and an expected type the rest of the function (which includes an Ident.unscoped that should be instantiated away for the parameter's identifier). Both of these expected types can just be unification variables if there is no useful information in the expected type.
2. Typing the pattern and unifying it with the expected pattern type -- giving an error if the signature cannot be inferred. This part can be split off into its own type_functor_argument function.

[github-actions]

Parser Change Checklist

This PR modifies the parser. Please check that the following tests are updated:

• parsetree/source_jane_street.ml

This test should have examples of every new bit of syntax you are adding. Feel free to just check the box if your PR does not actually change the syntax (because it is refactoring the parser, say).