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
Comments
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. |
Comment author: heidegger Thanks a lot for your helping hint. Then I will try to restructure my code to deal with that restriction. |
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. |
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. |
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. |
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
The text was updated successfully, but these errors were encountered: