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

Typing recursive modules, maybe related to 4470? #4615

Closed
vicuna opened this issue Sep 16, 2008 · 5 comments
Closed

Typing recursive modules, maybe related to 4470? #4615

vicuna opened this issue Sep 16, 2008 · 5 comments

Comments

@vicuna
Copy link

vicuna commented Sep 16, 2008

Original bug ID: 4615
Reporter: heidegger
Status: acknowledged (set by @damiendoligez on 2008-09-23T00:37:21Z)
Resolution: open
Priority: normal
Severity: tweak
Version: 3.10.2
Target version: later
Category: typing
Tags: recmod
Related to: #3476 #4049 #4470
Monitored by: @jberdine

Bug description

I get a strange error message from my ocaml 3.10.2 compiler.

The message tells me, that the implementation of a module
and the corresponding signature does not match.
Here is the important part of the message:

The Implementation:
val create_c_read :
ConstBasic.local_env -> Type.lenv
ConstBasic.prevar -> Vars.PreVar.t
ConstBasic.lsvar -> Vars.LSetVar.t
Syntax.label ->
ConstBasic.tau -> Type.t
t Const.t = True | False | Set of CSet.t

The Signature:
val create_c_read :
local_env -> Type.lenv
prevar -> Vars.PreVar.t
lsvar -> Vars.LSetVar.t
Syntax.label ->
tau -> Type.t
t ---

On the right side I looked up the type aliases in the file by
hand. Because they are equal, I think the type checker should
allow this module to pass typing. One interesting thing at this
error message is, that very similar functions pass the type checker,
so the type checker uses the type aliases at the other places, but
do not use it here.

I found a version where the modules type check. The changes are not important, but probibly this version may help to find my error or the error of the type checker. (the alternitive version is commented out, grep after "ALT:" to find the places in the file inf.ml).

Additional information

The main difference that I notice is, that for this function the
type alias has two module names in front (the Vars.PreVar part
of the type Vars.PreVar.t). This is not the case in the other
functions, that pass the type checker. Now I searched for some
information about recursive modules (the module is a recursive one)
and found some information about it under:
#4470

The output of the compiler:

Signature mismatch:
Modules do not match:
sig
module CSet :
sig ... end
type tvar = Vars.TVar.t
type levar = Vars.LEVar.t
type otvar = Vars.OTVar.t
type prevar = Vars.PreVar.t
type lsvar = Vars.LSetVar.t
type tau = Type.t
type pointer = Type.p
type local_env = Type.lenv
type obj = Type.r
type location_set = Type.phi
type precise = Type.q
type const = Const.t
type t = Const.t = True | False | Set of CSet.t
val c_true : t
val c_false : t
val c_and : t -> t -> t
val c_ands : t list -> t
val compare : t -> t -> int
val string_of : t -> string
val to_t : CSet.elt -> t
val to_t_1 : ('a -> CSet.elt) -> 'a -> t
val to_t_2 : ('a -> 'b -> CSet.elt) -> 'a -> 'b -> t
val to_t_3 : ('a -> 'b -> 'c -> CSet.elt) -> 'a -> 'b -> 'c -> t
val to_t_4 :
('a -> 'b -> 'c -> 'd -> CSet.elt) -> 'a -> 'b -> 'c -> 'd -> t
val to_t_5 :
('a -> 'b -> 'c -> 'd -> 'e -> CSet.elt) ->
'a -> 'b -> 'c -> 'd -> 'e -> t
val create_c_domain :
ConstBasic.local_env ->
ConstBasic.local_env -> Location.Loc.t -> ConstBasic.obj -> t
val create_c_domain_eq :
ConstBasic.location_set -> ConstBasic.local_env -> t
val create_c_pres : ConstBasic.precise -> ConstBasic.precise -> t
val create_c_eqset :
ConstBasic.location_set -> ConstBasic.location_set -> t
val create_c_eqobj : ConstBasic.obj -> ConstBasic.obj -> t
val create_c_eqlenv : ConstBasic.local_env -> ConstBasic.local_env -> t
val create_c_eqref : ConstBasic.pointer -> ConstBasic.pointer -> t
val create_c_eqtypes : ConstBasic.tau -> ConstBasic.tau -> t
val create_c_subtype : ConstBasic.tau -> ConstBasic.tau -> t
val create_c_disjoint :
ConstBasic.location_set -> ConstBasic.location_set -> t
val create_c_subset :
ConstBasic.location_set -> ConstBasic.location_set -> t
val create_c_exclude : Location.Loc.t -> ConstBasic.location_set -> t
val create_c_include : Location.Loc.t -> ConstBasic.location_set -> t
val create_c_demotation_lenv :
ConstBasic.local_env ->
ConstBasic.location_set -> ConstBasic.local_env -> t
val create_c_demotation_type :
ConstBasic.tau -> ConstBasic.location_set -> ConstBasic.tau -> t
val create_c_flow :
ConstBasic.local_env -> ConstBasic.tau -> ConstBasic.tau -> t
val create_c_read :
ConstBasic.local_env ->
ConstBasic.prevar ->
ConstBasic.lsvar -> Syntax.label -> ConstBasic.tau -> t
end
is not included in
sig
type tvar = Vars.TVar.t
type levar = Vars.LEVar.t
type otvar = Vars.OTVar.t
type prevar = Vars.PreVar.t
type lsvar = Vars.LSetVar.t
type tau = Type.t
type pointer = Type.p
type local_env = Type.lenv
type obj = Type.r
type location_set = Type.phi
type precise = Type.q
type const = Const.t
type t
val create_c_demotation_lenv :
local_env -> location_set -> local_env -> t
val create_c_demotation_type : tau -> location_set -> tau -> t
val create_c_include : Location.Loc.t -> location_set -> t
val create_c_exclude : Location.Loc.t -> location_set -> t
val create_c_subset : location_set -> location_set -> t
val create_c_disjoint : location_set -> location_set -> t
val create_c_subtype : tau -> tau -> t
val create_c_eqtypes : tau -> tau -> t
val create_c_eqref : pointer -> pointer -> t
val create_c_eqlenv : local_env -> local_env -> t
val create_c_eqobj : obj -> obj -> t
val create_c_eqset : location_set -> location_set -> t
val create_c_pres : precise -> precise -> t
val create_c_domain_eq : location_set -> local_env -> t
val create_c_domain :
local_env -> local_env -> Location.Loc.t -> obj -> t
val create_c_flow : local_env -> tau -> tau -> t
val create_c_read :
local_env -> prevar -> lsvar -> Syntax.label -> tau -> t
val string_of : t -> string
val compare : t -> t -> int
val c_true : t
val c_false : t
val c_and : t -> t -> t
val c_ands : t list -> t
end
Values do not match:
val create_c_read :
ConstBasic.local_env ->
ConstBasic.prevar ->
ConstBasic.lsvar -> Syntax.label -> ConstBasic.tau -> t
is not included in
val create_c_read :
local_env -> prevar -> lsvar -> Syntax.label -> tau -> t
Command exited with code 2.
make: *** [byte] Error 10

To compile the project, you need some ocamlfind packages, even one of my own (proglangUtils):
http://www.informatik.uni-freiburg.de/~linkenhe/

File attachments

@vicuna
Copy link
Author

vicuna commented Oct 3, 2008

Comment author: @xavierleroy

Thanks for the repro case. This is another instance of a known problem with applicative functors (see #3476, #4049). There is no easy fix except perhaps a compile-time flag to turn applicative functors off.

@vicuna
Copy link
Author

vicuna commented Oct 4, 2008

Comment author: heidegger

Thanks a lot for your helping hint. Then I will try to restructure my code to deal with that restriction.

@vicuna
Copy link
Author

vicuna commented Aug 6, 2012

Comment author: @xavierleroy

I've been sleeping on these PR for too long, and still have no idea how to address them. Unassigning them from myself.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

@github-actions github-actions bot added the Stale label May 18, 2020
@lpw25
Copy link
Contributor

lpw25 commented May 18, 2020

Judging by Xavier's analysis, I suspect that this issue was fixed when module aliases were added to the language. I'm not currently in a position to try the very old repro case, but I'm going to close anyway.

@lpw25 lpw25 closed this as completed May 18, 2020
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

3 participants