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

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0003476OCamlOCaml generalpublic2005-02-18 11:252006-08-30 13:57
Reporteradministrator 
Assigned Toxleroy 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionwon't fix 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0003476: Bug in type checker with functors?
DescriptionHi,

this mail has already been sent to you once, but didn't show up in the
bug tracker (possibly a problem with the mail agent). To make sure you
get it, here it is again:

We have observed strange behaviour of the type checker when using
functors.

The following code does not compile:

---------------------------------------------------------------------------
module FF(X : sig end) =
struct
  type t
end

module M =
struct
  module X = struct end
  module Y = FF (X) (* XXX *)
  type t = Y.t
end

module F
  (Y : sig type t end)
  (M : sig type t = Y.t end) =
struct
end

module N = F (M.Y) (M)
---------------------------------------------------------------------------

The error is:

  Signature mismatch:
  Modules do not match:
    sig
      module X : sig end
      module Y : sig type t = FF(X).t end
      type t = Y.t
    end
  is not included in
    sig type t = M.Y.t end
  Type declarations do not match:
    type t = Y.t
  is not included in
    type t = M.Y.t

However, if we replace the line marked with "XXX" as follows (i.e.
expand the definition of the argument "X"):

  module Y = FF (struct end)

then the code compiles without problems. Are we overlooking a trivial
reason why the first code should be incorrect?

Our compiler version is 3.08.2.

Best regards,
Markus

--
Markus Mottl mmottl@janestcapital.com

TagsNo tags attached.
Attached Files

- Relationships
related to 0004049closed module abbreviations may break type equality ? 
related to 0004615acknowledged Typing recursive modules, maybe related to 4470? 
related to 0005058acknowledged improve type checking of applicative functors 
child of 0005302closed two names for same module are (wrongly) distinguished by the typechecker 

-  Notes
(0003756)
xleroy (administrator)
2006-08-30 13:57

 This is an unfortunate consequence of applicative functors.
In the example, there are two valid but incompatible signatures for M.Y:
M.Y : sig type t = FF(M.X).t end (because of applicative functors)
and
M.Y : sig type t = M.Y.t end (by regular strengthening)
Since the OCaml module system can only express one equality per type component of a structure, both type equalities cannot be expressed, and the system
chooses the first signature, while the second is what is needed to satisfy the sharing constraint in functor F. Replacing FF(X) by FF(struct end)
renders the special case for applicative functors inapplicable and the problem goes away.

I agree this is an unfortunate side-effect of applicative functors, and there are other such side-effects (see PR 0004049 for instance). There are no easy fixes: removing app. funct. would break too much code, and making sure app. funct. never cause such information loss is basically an open problem that would certainly require a major rewrite of the module type-checker. So, chalk it on bad design if you want, but I'm afraid this is a "won't fix" situation.


 following two type equations hold concerning M.Y.t:
M.Y.t = FF(M.X).t because of applicative functors, and
M.Y.t = M.Y.t

- Issue History
Date Modified Username Field Change
2005-11-18 10:14 administrator New Issue
2005-12-15 15:28 doligez Assigned To => xleroy
2005-12-15 15:28 doligez Description Updated
2006-08-29 17:30 doligez Relationship added related to 0004049
2006-08-30 13:57 xleroy Note Added: 0003756
2006-08-30 13:57 xleroy Status acknowledged => closed
2006-08-30 13:57 xleroy Resolution open => won't fix
2008-10-03 11:26 xleroy Relationship added related to 0004615
2010-05-24 10:15 shinwell Relationship added related to 0005058
2011-07-27 14:52 xclerc Relationship added child of 0005302

Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker