Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006882OCamltypingpublic2015-05-29 16:122017-03-14 10:45
Reportermbarbin 
Assigned Togarrigue 
PrioritynormalSeverityminorReproducibilityalways
StatusresolvedResolutionfixed 
PlatformOSOS Version
Product Version4.02.1 
Target VersionundecidedFixed in Version4.03.0 
Summary0006882: Apparently valid program rejected by the typer
DescriptionI suppose something going on with aliases. Here is the code, tried with 4.02.2.

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

module M = struct
  module A = struct type t = int end
  include Make (A)
end

(* Version 1: [id] below won't type:

   File "/tmp/a.ml", line 24, characters 23-24:
   Error: This expression has type T.t = Make(M.A).t
   but an expression was expected of type t = Make(A).t
*)
module T = M

(* Version 2: [id] below will type *)
(* module T = struct include M end *)

(* Version 3: [id] below will type *)
(* module X = M
 * module T = struct include X end *)

include T

let id (t : T.t) : t = t



The private part in [Make] can be replaced with something else, the error is still roughly the same, such as e.g.:

module Make ( X : sig end ) : sig
  type t = A
end = struct
  type t = A
end


TagsNo tags attached.
Attached Files

- Relationships
duplicate of 0006485resolvedgarrigue private lost after rebinding module 

-  Notes
(0013991)
mbarbin (reporter)
2015-05-29 17:07

vgatien-baron pointed out to me that a different workaround is to have Make being generative. As in turns out in my complete case the generative aspect matches better what I want. Just sharing this info in case it spreads some more light on this.
(0014013)
sliquister (reporter)
2015-06-02 20:50

I think I just stepped into the same problem:

module A = struct
  module Make(X : sig end) : sig
    type t = private int
  end = struct
    type t = int
  end
end

module First_try = struct
  module B = A (* inferred type: (module A) *)
  module C = struct include B end (* inferred type: sig module Make : functor (X : sig end) -> sig type t = A.Make(X).t end end *)
  module Res = B.Make(struct end) (* WRONG inferred type: sig type t end *)
end

module Second_try = struct
  module B = struct include A end (* inferred type: sig module Make = A.Make end *)
  module C = struct include B end (* inferred type: sig module Make = A.Make end *)
  module Res = B.Make(struct end) (* inferred type: sig type t = private int end *)
end

In that particular example, I think the problem is that the inferred type of First_try.C should be the same as the one of Second_try.C, ie when you look at the shallow structure of a module alias, you should get a bunch of val and type and modules, where module are aliases pointing to the original module (when possible) instead of strenghtened copies as right now.


It's not super clear though in the original example why [module T2 = struct include T end] has the right type [sig module A = M.A type t = Make(A).t end] but [include T] has the wrong type [module A : sig type t = int end].
(0014015)
garrigue (manager)
2015-06-03 02:33

This is not specific to aliases.
Actually, the problem was already there in previous versions of ocaml, before the introduction of module aliases.
And module aliases improve the situation. In ocaml 4.00, you get an error already with

  include M
  let id (x : M.t) : t = x

which works thanks to module aliases.
To allow this kind of example to work smoothly, one would need a stronger version of module aliases, which complicate significantly type inference. We are considering it for completeness, though.
(0014019)
sliquister (reporter)
2015-06-03 21:13

Stupid question: when the typer types the application of a functor with a type of say [functor (X : A) -> sig type t = F(A).t end] to something other than a module path, it seems that the typer essentially drops the equation from the return signature of the functor. Why can't the typer go in [F(A)] (with A substituted by its actual type), realize that [F(A).t] is defined as [type t = private int], and say the return type of the module is [sig type t = private int]?
(0017647)
garrigue (manager)
2017-03-14 10:45

This seems to work since 4.03.

- Issue History
Date Modified Username Field Change
2015-05-29 16:12 mbarbin New Issue
2015-05-29 16:20 shinwell Assigned To => garrigue
2015-05-29 16:20 shinwell Status new => assigned
2015-05-29 17:07 mbarbin Note Added: 0013991
2015-06-01 22:01 doligez Product Version => 4.02.1
2015-06-01 22:01 doligez Target Version => 4.02.3+dev
2015-06-02 20:50 sliquister Note Added: 0014013
2015-06-03 02:23 garrigue Relationship added duplicate of 0006485
2015-06-03 02:33 garrigue Note Added: 0014015
2015-06-03 21:13 sliquister Note Added: 0014019
2015-07-10 16:18 doligez Target Version 4.02.3+dev => 4.03.0+dev / +beta1
2016-04-18 11:54 doligez Target Version 4.03.0+dev / +beta1 => 4.03.1+dev
2017-02-16 14:01 doligez Target Version 4.03.1+dev => undecided
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-14 10:45 garrigue Note Added: 0017647
2017-03-14 10:45 garrigue Status assigned => resolved
2017-03-14 10:45 garrigue Fixed in Version => 4.03.0
2017-03-14 10:45 garrigue Resolution open => fixed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker