Mantis Bug Tracker
Main | My View | View Issues | Change Log | Roadmap
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0004615OCamlOCaml generalpublic2008-09-16 14:202012-08-07 08:59
Reporterheidegger 
Assigned To 
PrioritynormalSeveritytweakReproducibilityalways
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version3.10.2 
Target Version4.01.0+devFixed in Version 
Summary0004615: Typing recursive modules, maybe related to 4470?
DescriptionI 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 InformationThe 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:
  http://caml.inria.fr/mantis/view.php?id=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/ [^]
Tagsrecmod
Attached Filesgz file icon impl.tar.gz [^] (42,393 bytes) 2008-09-16 14:20

- Relationships
related to 0003476closedxleroy Bug in type checker with functors? 
related to 0004049closed module abbreviations may break type equality ? 

-  Notes
(0004646)
xleroy (administrator)
2008-10-03 11:26

 Thanks for the repro case. This is another instance of a known problem with applicative functors (see PR#3476, PR#4049). There is no easy fix except perhaps a compile-time flag to turn applicative functors off.
(0004662)
heidegger (reporter)
2008-10-04 20:56

 Thanks a lot for your helping hint. Then I will try to restructure my code to deal with that restriction.
(0007912)
xleroy (administrator)
2012-08-06 18:24

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

- Issue History
Date Modified Username Field Change
2008-09-16 14:20 heidegger New Issue
2008-09-16 14:20 heidegger File Added: impl.tar.gz
2008-09-23 02:37 doligez Status new => acknowledged
2008-10-03 11:26 xleroy Note Added: 0004646
2008-10-03 11:26 xleroy Assigned To => xleroy
2008-10-03 11:26 xleroy Relationship added related to 0003476
2008-10-03 11:27 xleroy Relationship added related to 0004049
2008-10-04 20:56 heidegger Note Added: 0004662
2012-08-06 18:22 xleroy Target Version => 4.01.0+dev
2012-08-06 18:24 xleroy Note Added: 0007912
2012-08-06 18:26 xleroy Assigned To xleroy =>
2012-08-06 22:55 frisch Tag Attached: recmod

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker