Version française
Home     About     Download     Resources     Contact us    
Browse thread
Recursive module signatures + functors
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Xavier Leroy <Xavier.Leroy@i...>
Subject: Re: [Caml-list] Recursive module signatures + functors
> I've been playing around with using recursive modules to implement mixins
> and don't understand why the type checker fails to accept code below.
> [...]
> I don't quite understand why the type system doesn't know that t and M.t
> are the same.

As Andreas said, this is an instance of the infamous "double vision"
problem.  The OCaml module type-checker can deal with this, but the
current implementation is incomplete and works only for generative
type definitions, not for type abbreviations.

Continuing Andreas' example:

module rec M : sig type t val f : t -> t end =
struct
   type t = N of int
   let f (x : M.t) = x
end

This is accepted because the type-checker can add a type equality
"t = M.t" while type-checking the body of the structure.  However,
with a type abbreviation

module rec M : sig type t val f : t -> t end =
struct
   type t = int
   let f (x : M.t) = x
end

there is already a type equality over t, namely "t = int", and the
current implementation of the type-checker is not able to record and
maintain several type equalities (here, t = int = M.t) over one type
constructor.

Likewise, your example goes through if you put "type t = Constr of ..."
instead of "type t = int".

> Is this a bug in the type checker or is there a reason that it does not
> unify 't' and 'M.t'?

Well, there is a technical reason, but I agree this limitation is a bug.

- Xavier Leroy