I seem to have encountered a problem in type-checking of higher-order 
functors with type constraints -- it seems to me that the containment 
check is backwards.  Below I include complete code (between ======= 
makers).  This was tried in ocaml 3.09.01

Basically, I use singleton types to encode presence/absence of a 
semantic property.  I use type constraints to ensure that the functor 
cannot be applied if the constraint is not satisfied.  If I write 
everything "simply", it all works.  If I go higher-order, it fails.  
Below is what I can distill from a much much larger program and still 
show the issue.
=============
(* this works *)
module type DOMAIN = sig
    type kind
    type foo
    val  upd : foo -> foo
end

type domain_is_field

module Rational = struct
    type kind = domain_is_field
    type foo  = int * int
    let  upd (x,y) = (x-1, y+1)
end

module Integer = struct
    type kind
    type foo  = int
    let  upd x = x-1
end

module type UPDATE = sig
    type obj
    val update : obj -> obj
end

module DivisionUpdate(D:DOMAIN with type kind = domain_is_field) = struct
    type obj = D.foo
    let update a = D.upd a
end

(* this one is semantically incorrect! *)
module BadUpdate(D:DOMAIN) = struct
    type obj = D.foo
    let update a = D.upd a
end

(* works, as expected *)
module A = DivisionUpdate(Rational)
(* _correctly_ generates an error
module A = DivisionUpdate(Integer)
*)

(* However, if we go higher order: *)
module type UPDATE2 =
    functor(D:DOMAIN) -> sig
    type obj = D.foo
    val update : obj -> obj
end

(* this is the same as the "updates" above, just wrapped in a module *)
module Bar(D:DOMAIN)(U:UPDATE2) = struct
    module U = U(D)
    let update x = U.update x
end

(* works as there are no restrictions *)
module T3 = Bar(Integer)(BadUpdate) ;;

(* and now this does not work?!?! even though it should!*)
module T2 = Bar(Rational)(DivisionUpdate) ;;

============
The error I get on this very last line is
Signature mismatch:
Modules do not match:
  functor
    (D : sig type kind = domain_is_field type foo val upd : foo -> foo 
end) ->
    sig type obj = D.foo val update : D.foo -> D.foo end
is not included in
  UPDATE2
Modules do not match:
  DOMAIN
is not included in
  sig type kind = domain_is_field type foo val upd : foo -> foo end
Type declarations do not match:
  type kind
is not included in
  type kind = domain_is_field

and this last check seems to be looking at signature inclusion 
*backwards*, especially since it works if you do the same at the 'top 
level' instead of passing things in through a functor.

Or I am making a mistake somewhere above?

Jacques