Original bug ID: 7336
Reporter: @sliquister
Status: acknowledged (set by @xavierleroy on 2017-02-18T17:24:17Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.03.0
Target version: 4.07.0+dev/beta2/rc1/rc2
Category: typing
Child of: #7338
Monitored by: @gasche

Bug description

I got the following (legitimate) type error today:

$ ocamlopt -short-paths a.ml
File "a.ml", line 27, characters 11-12:
Error: Signature mismatch:
       ...
       Values do not match:
         val fold :
           ('a, 'b) hashtbl ->
           init:'c -> f:(key:'a -> data:'b -> 'c -> 'c) -> 'c
       is not included in
         val fold :
           ('a, 'b) t1 ->
           init:'c -> f:(key:Key.t -> data:'b -> 'c -> 'c) -> 'c
       File "a.ml", line 4, characters 2-85: Expected declaration
       File "a.ml", line 4, characters 2-85: Actual declaration

while building something I reduced to [1]. The details of the code or the error are not very important, the point is I was not able to figure out what the problem is until someone helped me, because the types printed are what I expect. It turns out the bug was in the definition of t1.

I think the type error reporting is not as good at the module level. I don't think I'm ever confused like that by errors that don't involve modules. Contrast with an error involving the same types, but when there is no module in sight:

$ ocamlopt -short-paths a.ml
File "a.ml", line 26, characters 32-33:
Error: This expression has type
         (a, b) t1 -> init:c -> f:(key:key -> data:b -> c -> c) -> c
       but an expression was expected of type
         (a, b) hashtbl -> init:c -> f:(key:a -> data:b -> c -> c) -> c
       Type (a, b) t1 = (key, a) hashtbl is not compatible with type
         (a, b) hashtbl
       Type key is not compatible with type a

I'd like the typer to give this kind of error at the module level too. If this error had been given, I would have probably found the problem right away.

(Here, it probably didn't help that we are forced to create useless types, t1 and key1, to use destructive substitutions, because now they show up in type errors. I'm trying to lift that restriction.)

[1]

module type S = sig
  type ('a, 'b) t
  type 'a key
  val fold :
    ('a, 'b) t -> init:'c -> f:(key:'a key -> data:'b -> 'c -> 'c) -> 'c
end

module M : S with type 'a key = 'a = struct
  type ('a, 'b) t
  type 'a key = 'a
  let fold = assert false
end

type ('a, 'b) t = ('a, 'b) M.t
module Make(Key : sig type t end) = struct
  type key = Key.t
  type ('a, 'b) hashtbl = ('a, 'b) t
  type 'a t = (key, 'a) hashtbl
  type ('a, 'b) t1 = (key, 'a) hashtbl
  type 'a key1 = key

  (* roughly equivalent type error at the value level:
    type a type b type c
    let x : (a, b) hashtbl -> init:c -> f:(key:a M.key -> data:b -> c -> c) -> c = assert false
    let y : (a, b) t1 -> init:c -> f:(key:Key.t -> data:b -> c -> c) -> c = assert false
    let _ = if true then x else y
  *)
  include (M : S
           with type ('a, 'b) t := ('a, 'b) t1
           with type 'a key := 'a key1)
end