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

unexpected (?) typing error related to aliasing of types defined in recursive modules #7622

Closed
vicuna opened this issue Sep 5, 2017 · 4 comments

Comments

@vicuna
Copy link

vicuna commented Sep 5, 2017

Original bug ID: 7622
Reporter: kosik
Status: resolved (set by @xavierleroy on 2017-09-30T09:24:30Z)
Resolution: suspended
Priority: normal
Severity: minor
Version: 4.05.0
Category: typing
Tags: recmod
Monitored by: @gasche

Bug description

If my "b.mli" file contains the following code:

(1) module rec A :
(2) sig
(3) type t = T1
(4) end
(5)
(6) and B :
(7) sig
(8) type t = A.t = T1
(9) end

and I try to compile this file:

ocamlc -c b.mli

then I get the following error message:

File "b.mli", line 8, characters 9-26:
Error: This variant or record definition does not match that of type A.t
Their kinds differ.

I've asked about this on caml-list
https://sympa.inria.fr/sympa/arc/caml-list/2017-08/msg00043.html
but I haven't got a reply.

My questions:

  • What does the error message mean?
    (Is it really necessary to reject the above fragment as ill-typed?)
    • What is the kind of A.t?
    • What is the kind of B.t?
    • Why are the kinds of of B.t and A.t different?

Steps to reproduce

ocamlc -c b.mli

File attachments

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: @lpw25

In order to type-check the types of recursive modues you need to create an approximation of each module's type. So in your example, we create the approximation:

module rec A : sig
  type t
end

and B : sig
  type t
end

and use these approximations to type-checking the full module types. This fails because:

type t = A.t = T1

requires that A.t is a variant type, but in the approximation it is abstract.
This is what the error message is referring to: the "kind" of B.t's definition -- variant -- does not match the "kind" of A.t -- abstract.

I think this is an "expected" error rather than a bug -- by which I mean that people probably knew this kind of thing would fail but thought that the changes required to make it work -- which seem like they might be non-trivial to me -- were not worth the benefit of avoiding this error. Of course, at the very least a better error message would be nice.

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: kosik

Does that that, in short, mean that Ocaml does not support aliasing of types
(of variant kind) within recursive modules?

@vicuna
Copy link
Author

vicuna commented Sep 5, 2017

Comment author: @lpw25

Well you can do:

module rec A : sig
  type t = T1
end

and B' : sig
  type t = A.t
end

module B : sig
  type t = A.t = T1
  include module type of struct include B' end
    with type t := t
end

but, yeah, you can't directly re-expose the constructors of a variant from a mutually recursive module.

@vicuna
Copy link
Author

vicuna commented Sep 30, 2017

Comment author: @xavierleroy

I am skeptical that this combination of recursive modules and manifest types with exposed representation will ever be supported. Marking this PR "suspended".

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

1 participant