Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007622OCamltypingpublic2017-09-05 10:132017-09-30 11:24
Reporterkosik 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionsuspended 
PlatformOSOS Version
Product Version4.05.0 
Target VersionFixed in Version 
Summary0007622: unexpected (?) typing error related to aliasing of types defined in recursive modules
DescriptionIf 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 Reproduceocamlc -c b.mli
Tagsrecmod
Attached Files? file icon b.mli [^] (135 bytes) 2017-09-05 10:13 [Show Content]

- Relationships

-  Notes
(0018221)
lpw25 (developer)
2017-09-05 14:55

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.
(0018222)
kosik (reporter)
2017-09-05 15:33

Does that that, in short, mean that Ocaml does not support aliasing of types
(of variant kind) within recursive modules?
(0018226)
lpw25 (developer)
2017-09-05 17:49

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.
(0018418)
xleroy (administrator)
2017-09-30 11:24

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

- Issue History
Date Modified Username Field Change
2017-09-05 10:13 kosik New Issue
2017-09-05 10:13 kosik File Added: b.mli
2017-09-05 14:55 lpw25 Note Added: 0018221
2017-09-05 15:33 kosik Note Added: 0018222
2017-09-05 17:49 lpw25 Note Added: 0018226
2017-09-06 15:35 frisch Tag Attached: recmod
2017-09-30 11:24 xleroy Note Added: 0018418
2017-09-30 11:24 xleroy Status new => resolved
2017-09-30 11:24 xleroy Resolution open => suspended


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker