Thanks. it helps.
Here's what I really want, is there any way to walk around if not possible?

S1 is not written by me.
--------------------------------------------------------------------
module type S1 = sig
  module Inner  : sig
    type 'a t
    val add : 'a t -> 'a t -> int
  end
end

let f1
    (type s)
    (type a)
    (module Y : S1 with type s Inner.t = a) (y: s Y.Inner.t) =
  Y.Inner.add y y
------------------------------------------------------------------------------------------------------------
On Thu, Jun 7, 2012 at 11:22 PM, Jacques Garrigue <
garrigue@math.nagoya-u.ac.jp> wrote:

> On 2012/06/08, at 11:35, Hongbo Zhang wrote:
>
> > Hi, List
> >  I am not sure this is a bug or not?
> >
> >  Below is a contrived example:
> > ------------------
> >  module type S = sig
> >    type t=int
> >    module  X : sig type u   end
> >  end
> >
> >  let f ( module X : S)  (y:X.X.u) =
> >  3
> > --------------------
> > Error: This pattern matches values of type X.X.u
> >      but a pattern was expected which matches values of type X.X.u
> >      The type constructor X.X.u would escape its scope
> > -- Thanks
>
> Definitely, this is not a bug.
> Type X.X.u is abstract, and showing it outside (as by taking an argument
> of that type) would be meaningless.
>
> What you might have meant is:
>
>  let f (type a) (module X : S with type X.u = a) (y : X.X.u) = 3
>
> This is typable (but I'm not sure it means anything...)
>
> Jacques Garrigue
>



-- 
-- Bob