I have written a list-of-sorted-lists merging function which takes 
advantage of a functional heap module by Jean-Christophe Filliatre. I 
would like to avoid the functorial style of the heap library by using 
local modules; however, the type system does not allow me to bind the 
"type t" of the local parameter module to a type variable, which is 
bound in the containing expression.

This is what I would like to have:

let rev_merge_list_rev_filter_append
    (cmp : 'a -> 'a -> int)
    (p : 'a -> bool)
    (ll : 'a list list)
    (accu : 'a list)
=
   let module Ordered = struct
     type t = Obj.t * (Obj.t list)
     let compare (x,tlx) (y,tly) = cmp ((Obj.obj x):'a) ((Obj.obj y):'a)
   end in
   let module Heap = Heap.Functional (Ordered)
   in
     ...


This is what I had to write.


let rev_merge_list_rev_filter_append
    (cmp : 'a -> 'a -> int)
    (p : 'a -> bool)
    (ll : 'a list list)
    (accu : 'a list)
=
   let module Ordered = struct
     type t = Obj.t * (Obj.t list)
     let compare (x,tlx) (y,tly) = cmp ((Obj.obj x):'a) ((Obj.obj y):'a)
   end in
   let module Heap = Heap.Functional (Ordered)
   in
     ...

Is this a limitation of the type theory or of the type checker? Is there 
any other way out than using the Obj module?

Alex

-- 
*********************************************************************
http://www.barettadeit.com/
Baretta DE&IT
A division of Baretta SRL

tel. +39 02 370 111 55
fax. +39 02 370 111 54

Our technology:

The Application System/Xcaml (AS/Xcaml)
<http://www.asxcaml.org/>

The FreerP Project
<http://www.freerp.org/>