Use the typechecker to resolve import paths

[gasche]

This should fix the issue identified by #23.

The code is a bit complex (see the long documentation comment) because ppx_import supports querying the components of a module type, for example Map.OrderedType.t, which makes sense but is not a valid OCaml path.

I made a first much simpler and more naive attempt which does not support those sub-module-type names in paths (in particular, the testsuite does not pass), daf4cd5.

[whitequark]

I did not have a lot of time to review this, and don't foresee having it, but I very much like your approach and I trust your ability to implement it correctly, so please merge once you consider it acceptable.

[gasche]

I'm proud to have your trust, but I didn't have mine, so I went around and tested ppx_import users that I could find on opam. coq-serapi revealed a regression with the PR, that is due to an OCaml bug: the -rectypes flag is not passed as part of the ppx context, and loading a -rectypes-compiled signature is only allowed when -rectypes is set.

I worked around the problem by setting Clflags.recursive_types in all cases, which I think makes us type-check strictly more programs. (I also sent a PR upstream to propagate this information correctly, ocaml/ocaml#1921 ).

Right now the CI is broken by a change that I made to ease debugging (be more precise in the exceptions we catch) where I went overboard, I'll fix it. But now at least coq-serapi builds correctly, which is reassuring on correctness.

[gasche]

(There still seems to be issues with coq-serapi (as a good test case), I need to investigate further.)

[gasche]

I fixed the second coq-serapi failure, and now all of coq-serapi passes. It was fixed by a partial rewrite of this PR to be closer to the original source, and in particular it simplifies the logic a bit, which is nice. The previous version of the PR is available on my local branch use-typechecker-attempt2 -- the first naive attempt is use-typechecker-attempt1.

This is all nice and good, except... I don't really know what caused the second coq-serapi regression and why my new attempt fixes it. It seemed at first related to strengthening (the fact of adding more information to a module type by adding extra equalities), but I got rid of all strengthening in my attempt2 code, and the problem is still there. I've given up on understanding precisely where it comes from for now, but let me explain it below.

coq-serapi is a project that reproduces the API structure of the Coq project, to systematically add sexp serializes to all datatypes. In Coq, there is a file names.ml which looks as follows:

module Id = struct
  type t = ...
  ...
end

module Name = struct
  type t = Anonymous | Name of Id.t
end

In coq-serapi, there is a file serapi_names.ml which looks as follows:

module Id = struct
  type t = [%import: Names.Id.t] [@@deriving sexp]
end
module Name = struct
  type t = [%import: Names.Name.t] [@@deriving sexp]
end

With my wrong (old) patch, [%import: Names.Name.t] gets resolved as follows:

    type t = Names.Name.t =
      | Anonymous 
      | Name of Names.Id.t [@@deriving sexp]

With the good (new) patch, it gets resolved as follows:

    type t = Names.Name.t =
      | Anonymous 
      | Name of Id.t [@@deriving sexp]

The difference is Names.Id.t vs. Id.t in the argument of Name.

The first one is a regression, because when ppx_deriving traverses it to generate sexp, it wants to call a serializer on the argument of the Name constructor, and it calls Names.Id.t_of_sexp. But Names.Id is the module in Coq, and it has no t_of_sexp function.

On the other hand, the second elaboration, when fed to ppx_deriving, generates a call to Id.t_of_sexp instead -- and the module Id is shadowed locally by one for each a t_of_sexp function was precisely derived. So it works.

Why that works in the first place is rather fragile. But I'm more perplexed by the fact that I don't understand, between the two patches, what causes this difference in import generation. It looks like a module signature is getting strengthened somewhere in the wrong patch.

[gasche]

I'll try to test this PR against other the other consumers of ppx_import on OPAM this week, and merge if they all pass.

[gasche]

It seems that uwt and goblint build properly.

[gasche]

I don't see a "merge pull request" button for this PR, so I suspect that I may not have merge rights on this repository. (I don't know whether it is new, it seems that I have merged PRs previously in the project history.) @whitequark, would you merge on your end?

[whitequark]

@gasche I think someone deleted this repo by accident recently. Anyway, I gave you rights.

[gasche]

Thanks! (I remember now.) Would it be better if I volunteered to also prepare a new release?

[whitequark]

Please go ahead.

[mseri]

Would it be possible to have the new release? I am happy to do the PR for opam-repository if the version that supports 4.07 gets tagged