Comment author: administrator

Dear Norman,

I'm not sure if I'm just being stupid or if I've tripped over a bug in
OCaml version 3.01. I'm trying to put together a fairly heavily
functorized interpreter, and the compiler refuses to permit me
an annotation on the signature of a functor. I've boiled it down
to the following small test case:

Let me try to explain what's going on. Then we can argue later
whether it's the right behavior :-)

Currently, OCaml requires "with" constraints on signatures to add
information to what was already known in the original signature, but
doesn't allow existing information to be replaced by some other
information. More technically, the result of "S with ..." should be a
subtype of S. E.g.

(sig type t end) with type t = int

is OK, since we're adding the information that t is int. Similarly,

(sig type t = int end) with type t = int

is OK too, since we're not changing anything. However,

(sig type t = int end) with type t = bool

is rejected on the grounds that we would get

sig type t = bool end

which is not a subtype of

sig type t = int end

This restriction is somewhat arbitrary: we could interpret "with" as
general surgery over signatures, replacing one part of a signature by
anything else. The current restriction is largely inspired by sharing
constraints in SML, which would not allow to share two rigid types
(e.g. "int" and "bool" in the last example above).

Coming back to your example, let's expand some of the signatures:

module type VALUE' = sig
type userdata
end

module type AST' = sig
module Value : VALUE'
end

module type INTERP' = sig
module Value : VALUE'
module Ast : AST' with module Value = Value
end

i.e.

module type INTERP' = sig
module Value : VALUE'
module Ast : sig module Value: sig type userdata = Value.userdata end end
end

module MkInterp' (A : AST') : INTERP' with module Ast = A = struct
module Value = A.Value
module Ast = A
end

Here, A has principal signature
sig
module Value: sig type userdata = A.Value.userdata end
end

so INTERP' with module Ast = A would be

sig
module Value : VALUE'
module Ast :
sig
module Value: sig type userdata = A.Value.userdata end
end
end

and the system complains that this is not a subtype of INTERP',
since Value.userdata and A.Value.Userdata are not known to be the same
type.

However, you can tell Caml that it is so, as follows:

module MkInterp' (A : AST') :
INTERP' with module Value = A.Value with module Ast = A
= struct
module Value = A.Value
module Ast = A
end

It typechecks, and with some luck maybe it does what you want :-)

Best wishes,

• Xavier

Comment author: administrator

Explanations of the implemented behavior seem to have satisfied the user.