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

[vicuna]

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

• b.mli

[vicuna]

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]

Comment author: kosik

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

[vicuna]

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]

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".