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 = sigmodule Inner : sigtype 'a tval add : 'a t -> 'a t -> intendendlet 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