Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007336OCamltypingpublic2016-08-29 23:182018-04-24 17:32
Reportersliquister 
Assigned To 
PrioritynormalSeverityfeatureReproducibilityhave not tried
StatusacknowledgedResolutionopen 
PlatformOSOS Version
Product Version4.03.0 
Target Version4.07.0+dev/beta2/rc1/rc2Fixed in Version 
Summary0007336: Type errors at the module level are puzzling
DescriptionI 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
TagsNo tags attached.
Attached Files

- Relationships
child of 0007338confirmed meta-issue on confusing type error messages 

-  Notes
(0016241)
sliquister (reporter)
2016-08-30 04:34

I think the problem is Includemod calls Includecore.value_descriptions, which calls Ctype.more_general, which drops the Unify exception and returns a boolean instead.
(0019048)
trefis (manager)
2018-04-24 17:32

Follow-up: since GPR#792 was merged (in 4.06) I believe the example can be reduced to:

------
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 nonrec 'a t = (Key.t, 'a) t

  (* 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 t
           with type 'a key := Key.t)
end
------

Which gives the following error messages (when running without -short-paths):

File "./a.ml", line 25, characters 11-12:
Error: Signature mismatch:
       ...
       Values do not match:
         val fold :
           ('a, 'b) t ->
           init:'c -> f:(key:'a key -> data:'b -> 'c -> 'c) -> 'c
       is not included in
         val fold :
           'a t -> 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

When trying it with GPR#1737 the last two lines become:

       File "./a.ml", line 25, characters 15-93: Expected declaration
       File "./a.ml", line 4, characters 2-85: Actual declaration

While this is very slightly better, it's indeed still fairly confusing.
I agree with sliquister previous message: reusing the trace we get from [moregen] instead of discarding it would probably help matters a lot.

- Issue History
Date Modified Username Field Change
2016-08-29 23:18 sliquister New Issue
2016-08-30 04:34 sliquister Note Added: 0016241
2016-08-30 08:31 gasche Relationship added child of 0007338
2016-09-07 16:51 shinwell Target Version => 4.05.0 +dev/beta1/beta2/beta3/rc1
2017-02-18 18:24 xleroy Severity minor => text
2017-02-18 18:24 xleroy Status new => acknowledged
2017-02-18 18:24 xleroy Target Version 4.05.0 +dev/beta1/beta2/beta3/rc1 => 4.06.0 +dev/beta1/beta2/rc1
2017-02-23 16:45 doligez Category OCaml typing => typing
2017-03-07 13:57 shinwell Severity text => feature
2017-10-11 12:41 frisch Target Version 4.06.0 +dev/beta1/beta2/rc1 => 4.07.0+dev/beta2/rc1/rc2
2018-04-24 17:32 trefis Note Added: 0019048


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker