Hello,

> Can I look at the code which does not type check without Obj.magic?
> Ideally something like if I comment out Obj.magic then I get a type
> error, and if I comment it in then the code type checks, so that I can
> identify the point of the issue? (In the context of this simplified
> example of Boxes & Validator)

Yes, and thank you for taking an interest! I do have a warning though:
this code is not correct, in the sense that, it doesn't type and it
*shouldn't* type (because while in this case Validator.Boxes.t *is*
equivalent to B.t, there is nothing but my "good will" that guarantees in
the specs of the modules that this is so).

Attempts to make this correct (for the type checker) with "with type"
conditions have failed.

The mutually recursive version I posted in the previous message is an
"evolution" from this (and that mutually recursive version, contrarily to
this one is "correct").

  <code:"code_min_with_objmagic.ml">
  module type BOXES_PROVIDER =
  sig
    type t
  end

  module type VALIDATOR =
  sig
    module Boxes : BOXES_PROVIDER

    type t = Me of int | Node of t * t | B of Boxes.t

    val fold_on_B : (Boxes.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a
  end


  module BoxesProvider(Validator : VALIDATOR) : BOXES_PROVIDER =
  struct

    module rec A : sig
      type t = | Anil
  	     | Aout of Validator.t

      val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool
    end =
    struct
      type t = | Anil
  	     | Aout of Validator.t

      (* There is no equality between Validator.Boxes.t and B.t, i.e.:
         failing to see this is not a problem with the typechecker.
         To get the type error, replace with "let crosstype x = x". *)

      let crosstype (x : Validator.Boxes.t) =
        ((Obj.magic x) : B.t)

      let o_f p1 p2 =
        let rec aux = function
  	| Anil    -> false
  	| Aout tv ->
  	    Validator.fold_on_B (fun x -> B.o_f p1 p2 (crosstype x)) (||) false tv
        in
        aux
    end

    and B : sig
      type t = | Bnil
  	     | Bout of A.t * t
  		
      val o_f : ('a -> bool) -> ('a -> bool) -> t -> bool

    end =
    struct
      type t = | Bnil
  	     | Bout of A.t * t
  		
      let o_f p1 p2 =
        let rec aux = function
  	| Bnil        -> false
  	| Bout(a, tv) -> (A.o_f p1 p2 a) || (aux tv)
        in
        aux
    end

    type t = B.t

  end


  module rec Validator : VALIDATOR (* with type Boxes.t =
Validator.Boxes.t ?? *) =
  struct

    module Boxes = BoxesProvider(Validator)

    type t = Me of int | Node of t * t | B of Boxes.t

    let fold_on_B f combinator default =
      let rec aux = function
        | Node(b1, b2) -> combinator (aux b1) (aux b2)
        | B r	     -> f r
        | _  	     -> default
      in
      aux
  end
  </code>

> >   (********************)
> >   (* MODULE Validator *)
> >   (********************)
> >
> >   and Validator : sig
> >
> >     (* This type has been simplified for explanatory purposes. *)
> >     (* IDEALLY, Boxes.B.t would simply be B.t. *)
> >     type t = Me of int | Node of t * t | B of Boxes.B.t
> >
> >     val fold_on_B : (Boxes.B.t -> 'a) -> ('a -> 'a -> 'a) -> 'a -> t -> 'a
> >
> >   end =
>
> But B is not in the scope, isn't it?

Indeed. What I meant to say is, "IDEALLY, Boxes.B.t would simply be
Boxes.t" (and Validator would not need to know about submodules A and/or
B).

Please, of course, don't hesitate to ask for any other details you might
need (and don't hesitate to tell me if this Obj.magic code is not what you
needed!).

All the best,
Jérémie