I think the recursive modules definitions do not completely propagate safe definitions: I get Exception: Undefined_recursive_module ("SimpleLayer.ml", 104, 23) with the attached code. Chris D. module type LAYER = sig type topT type topV val topInj : string -> topT val topOp : topT -> topV val topExt : topV -> string type t type v val inj : string -> t val op : t -> v val ext : v -> string end (* base module -- no lower layer present, empty types, all operations are errors *) (* *** ``safe'' module (section 7.8 of refman) *** *) module MakeBase = functor (Above : LAYER) -> struct type topT = Above.topT type topV = Above.topV let topInj = fun x -> Above.topInj x(*safe*) let topOp = fun x -> Above.topOp x (*safe*) let topExt = fun x -> Above.topExt x(*safe*) type t = EmptyT (* wouldn't revised syntax be nice *) type v = EmptyV let inj = fun _ -> raise (Failure "inj") let op = fun _ -> raise (Failure "op") let ext = fun _ -> raise (Failure "ext") end (* an intermediate level *) module MakeMiddle = functor (Below : LAYER) -> functor (Above : LAYER) -> struct type topT = Above.topT type topV = Above.topV let topInj = Above.topInj let topOp = Above.topOp let topExt = Above.topExt type t = | BelowT of Below.t | OneT of char | TwoT of char * topT type v = | BelowV of Below.v | StringV of string let inj = fun s -> (* ::= 1_ [OneT _] | 2_? [TwoT _ ?] | *) match (String.get s 0) with | '1' -> OneT (String.get s 1) | '2' -> TwoT(String.get s 1, topInj (String.sub s 2 ((String.length s)-2))) | _ -> BelowT (Below.inj s) let op = function | BelowT t -> BelowV (Below.op t) | OneT(c) -> StringV ("1" ^ (String.make 1 c)) | TwoT(c,t) -> StringV ("2" ^ (String.make 1 c) ^ (topExt (topOp t))) let ext = function | BelowV v -> Below.ext v | StringV s -> s end (* imagine there were more levels -- maybe even tree/graph structured *) (* top level -- close the open recursion of topInj and topExt *) (* *** ``safe'' module (section 7.8 of refman) *** *) module MakeTop = functor (Below : LAYER) -> struct type t = Below.t type v = Below.v let inj = fun x -> Below.inj x (*safe*) let op = fun x -> Below.op x (*safe*) let ext = fun x -> Below.ext x (*safe*) type topT = t type topV = v let topInj = fun x -> inj x (*safe*) let topOp = fun x -> op x (*safe*) let topExt = fun x -> ext x (*safe*) end (* simplest test *) module rec B : LAYER = MakeBase(T) and T : LAYER = MakeTop(B) (* simple test *) module rec B : LAYER = MakeBase(M) and M : LAYER = MakeMiddle(B)(T) (* imagine there were more levels *) and T : LAYER = MakeTop(M);; T.topOp (T.topInj "2x1x");; T.topExt (T.topOp (T.topInj "2x1x"))