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

Apparently valid program rejected by the typer #6882

Closed
vicuna opened this issue May 29, 2015 · 5 comments
Closed

Apparently valid program rejected by the typer #6882

vicuna opened this issue May 29, 2015 · 5 comments

Comments

@vicuna
Copy link

vicuna commented May 29, 2015

Original bug ID: 6882
Reporter: mbarbin
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2017-03-14T09:45:35Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.02.1
Target version: undecided
Fixed in version: 4.03.0
Category: typing
Duplicate of: #6485

Bug description

I 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

@vicuna
Copy link
Author

vicuna commented May 29, 2015

Comment author: mbarbin

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.

@vicuna
Copy link
Author

vicuna commented Jun 2, 2015

Comment author: @sliquister

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

@vicuna
Copy link
Author

vicuna commented Jun 3, 2015

Comment author: @garrigue

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.

@vicuna
Copy link
Author

vicuna commented Jun 3, 2015

Comment author: @sliquister

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]?

@vicuna
Copy link
Author

vicuna commented Mar 14, 2017

Comment author: @garrigue

This seems to work since 4.03.

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

2 participants