"Jacques Carette" <carette@mcmaster.ca> wrote:
> 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.

Well, yes. That's contravariance.

> (* 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) ;;

No, it should not work. Bar(Rational) has the signature

  functor(U: functor(D:DOMAIN)->S1) -> S2

i.e. argument signature

  functor(D:DOMAIN)->S1

but you are trying to apply it to module DivisionUpdate, which has signature

  functor(D:DOMAIN')->S1

where DOMAIN'=(DOMAIN with type kind = domain_is_field). This is a
*sub*signature of DOMAIN! Since functors are necessarily contravariant in
their argument, however, it had to be a *super*signature of DOMAIN instead
to allow passing the functor to Bar.

That is, the problem with your example boils down to this:

  module type DOMAIN = sig type kind end
  module type DOMAIN' = sig type kind = unit end

  module Bar (U : functor(D : DOMAIN) -> sig end) = struct end
  module Up (D : DOMAIN') = struct end

  module T = Bar(Up)

-->

  Signature mismatch:
  Modules do not match:
    functor (D : DOMAIN') -> sig  end
  is not included in
    functor (D : DOMAIN) -> sig  end
  Modules do not match: DOMAIN is not included in DOMAIN'
  Type declarations do not match: type t is not included in type kind = unit

- Andreas