0005914: Functor breaks with an equivalent argument signature

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0005914

OCaml

OCaml typing

public

2013-02-01 23:13

2013-04-16 12:03

Reporter

mottl

Assigned To

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

new

Resolution

open

Platform

OS Version

Product Version

4.00.1

Target Version

Fixed in Version

Summary

0005914: Functor breaks with an equivalent argument signature

Description

Valid signatures that merely differ in the order of their entries should usually be considered equivalent. But here is an example where flipping the order of two function entries in an argument signature can break a functor. It seems this is related in some bizarre way to unification of recursive types, but the behavior is just downright weird. Here is the error message when running "ocaml" on file "bug.ml" below:

File "bug.ml", line 39, characters 21-22:
Error: Signature mismatch:
       ...
       Values do not match:
         val bar : unit -> ('a M.a M.wrap as 'a)
       is not included in
         val bar : unit -> t
       File "bug.ml", line 32, characters 2-21: Expected declaration
       File "bug.ml", line 18, characters 6-9: Actual declaration

The signatures "Good" and "Bad" are clearly equivalent modulo the order of the two function entries (foo and bar). Nevertheless, the application of Func_good succeeds whereas Func_bad fails. Note that removing the signature constraint ": S" from module M will make the example pass the typechecker again, too.

----------
module type S = sig
  type 't a = [ `A ]

  type 't wrap = 't constraint 't = [> 't wrap a ]
  val foo : 't wrap -> 't wrap -> unit
end

(* module M = struct *)
module M : S = struct
  type 't a = [ `A ]
  type 't wrap = 't constraint 't = [> 't wrap a ]
  let foo x y = ()
end

module T = struct
  type t = t M.a M.wrap
  include M
  let bar : unit -> ('a M.a M.wrap as 'a) = fun () -> `A
end

include T

module type Good = sig
  type t
  val bar : unit -> t
  val foo : t -> t -> unit
end

module type Bad = sig
  type t
  val foo : t -> t -> unit
  val bar : unit -> t
end

module Func_good (Arg : Good) = struct end
module Func_bad (Arg : Bad) = struct end

module X = Func_good (T)
module Y = Func_bad (T)
----------

Issue History
Date Modified	Username	Field	Change
2013-02-01 23:13	mottl	New Issue
2013-04-16 12:03	gasche	Severity	major => minor

Relationships

Notes
There are no notes attached to this issue.