Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allowing extra 'type' fields in signature inclusion check #6356

Closed
vicuna opened this issue Mar 28, 2014 · 6 comments
Closed

Allowing extra 'type' fields in signature inclusion check #6356

vicuna opened this issue Mar 28, 2014 · 6 comments

Comments

@vicuna
Copy link

vicuna commented Mar 28, 2014

Original bug ID: 6356
Reporter: @alainfrisch
Status: feedback (set by @damiendoligez on 2014-07-16T13:49:23Z)
Resolution: open
Priority: low
Severity: feature
Category: typing
Has duplicate: #6637
Monitored by: bobot @yallop @hcarty @yakobowski

Bug description

It is slightly annoying having to maintain the same definition of a type (resp. class type / module type) in both the interface and the implementation of a module, especially when the definition is not required within the implementation itself.

For instance, for a structure such as:

module type S = sig ... end
module Make(X : S) = struct ... end

one might want to give a signature which gives a name to the result type:

module type S = sig ... end
module type T = sig ... end

module Make(X : S) : T with ...

But this doesn't work: one needs to copy the definition of T within the implementation.

What about extending the inclusion check to allow more type items in the supertype? I don't know if I really want to push for it, but I'm wondering if there is any deeper implication in allowing that. The patch would be rather trivial:

Index: typing/includemod.ml
===================================================================
--- typing/includemod.ml	(revision 14492)
+++ typing/includemod.ml	(working copy)
@@ -297,6 +297,8 @@
               (* Do not report in case of failure,
                  as the main type will generate an error *)
               Field_type (String.sub s 0 (String.length s - 4)), false
+          | (Sig_type _ | Sig_modtype _ | Sig_class_type _), name2 ->
+              name2, false
           | _ -> name2, true
         in
         begin try
@vicuna
Copy link
Author

vicuna commented Apr 2, 2014

Comment author: @alainfrisch

FWIW, this change enables two cases currently failing in testsuite/tests/typing-module/firstclass.ml:

module type S = sig type u type t end;;
module type S' = sig type t = int type u = bool end;;
module type S2 = sig type u type t type w end;;

let f2 (x : (module S2 with type t = 'a and type u = 'b)) =
  (x : (module S'));; (* no longer fails *)

let k (x : (module S2 with type t = 'a)) =
  (x : (module S with type t = 'a));; (* no longer fails *)

@vicuna
Copy link
Author

vicuna commented Apr 4, 2014

Comment author: @garrigue

I would be very careful with this kind of change, because basically you enter uncharted territory.
Some properties, like the substitution property for modules, would not work anymore
(it already doesn't work stricto sensu due to open and include, but we go to another level).
A proof of soundness would be a first step :-)

@vicuna
Copy link
Author

vicuna commented Oct 30, 2014

Comment author: @garrigue

By the way, the implementation could not be that simple.
I tried your patch, and the following program fails:

module M : sig module type T = sig val x : int end module F() : T end =
struct module F() = struct let x = 3 end end;;

The reason is that, when comparing component types, we work in the environment of the internal module, which does not contain any definition for T.
At least one would need to add such definitions to the environment; clearly we would need a semantics first.

@garrigue
Copy link
Contributor

It seems that this one contains all the remaining part of #6637, so I'm going to close that one.

The way to implement this is to add explicit substitutions and local definitions for module types.
This is some work, but maybe someone wants to do it.

@lpw25
Copy link
Contributor

lpw25 commented May 11, 2020

The way to implement this is to add explicit substitutions and local definitions for module types.
This is some work, but maybe someone wants to do it.

I would be very grateful if someone would: I keep getting this request from users.

@Octachron
Copy link
Member

Module type substitutions were implemented in #10133 .

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

4 participants