KCH
KCH

Reputation: 2844

Type sharing in OCaml - typechecker error

When compiling this program:

module type Inc =
    sig
        type t
        val inc : t -> t
    end

module type Dec = 
    sig
        type t
        val dec : t -> t
    end

module Merger (I : Inc) (D : Dec with type t = I.t) =
    struct
        let merge x = x |> I.inc |> D.dec
    end

module IntInc : Inc = 
    struct
        type t = int
        let inc x = x + 10
    end

module IntDec : Dec = 
    struct 
        type t = int
        let dec x = x - 8
    end

module Combiner = Merger (IntInc) (IntDec)

I get the following error:

File "simple.ml", line 30, characters 35-41:
Error: Signature mismatch:
       Modules do not match:
         sig type t = IntDec.t val dec : t -> t end
       is not included in
         sig type t = IntInc.t val dec : t -> t end
       Type declarations do not match:
         type t = IntDec.t
       is not included in
         type t = IntInc.t
       File "simple.ml", line 13, characters 38-50: Expected declaration
       File "simple.ml", line 9, characters 13-14: Actual declaration

I thought that D : Dec with type t = I.t constraint will ensure that D.t = I.t. Why it is not so?

What is more interesting, when I remove module Combiner = Merger (IntInc) (IntDec) line it compiles without errors.

My question is : What am I doing wrong?

Upvotes: 3

Views: 589

Answers (1)

sepp2k
sepp2k

Reputation: 370092

Your definition of Merger with the constraint is perfectly correct, which is why that part compiles without error.

As you said, the only part that doesn't compile is module Combiner = Merger (IntInc) (IntDec). This is because, as far as OCaml knows, the constraint IntInt.t = IntDec.t is not met. The reason for that is that OCaml does not know that IntInt.t and IntDec.t are int. All it knows is that IntInt : Inc and IntDec : Dec - everything else is a private detail of the module.

To fix this problem you can change the module's headers to IntInt : (Inc with type t = int) and IntDec : (Dec with type t = int), making the type t a part of the modules' public interface rather than a private detail, allowing OCaml to use that information when resolving the constraint of the Merger functor.

Upvotes: 6

Related Questions