[Caml-list] Typing issue in explicit module

[Caml-list] Typing issue in explicit module

[Paul A. Steckler]

Here's some code that compiles successfully with 4.05.0 ocamlc. The .ml file is:

.ml file:
--
    type t
    let id x = x
    let idid = id id
--
.mli file:
--
  type t
  val id: 'a -> 'a
  val idid : t -> t
--

If I wrap the code in an explicit module, I get a type error:

.ml file:
--
module Foo =
  struct
  <code as before>
  end
--
.mli file:
--
module Foo :
 sig
   <code as before>
 end
--

With this change made, ocamlc complains:

--
Error: The implementation Foo.ml does not match the interface Foo.cmi:
       In module Foo:
       Modules do not match:
         sig type t = Foo.t val id : 'a -> 'a val idid : '_a -> '_a end
       is not included in
         sig type t val id : 'a -> 'a val idid : t -> t end
       In module Foo:
       Values do not match:
         val idid : '_a -> '_a
       is not included in
         val idid : t -> t
--

Adding a type annotation t -> t to the definition of "idid" gets rid
of the error.

With OCaml 4.04.0, no error occurs, and the type annotation is
unnecessary. Is this change expected?

The code I've shown is a simplified version of OCaml code extracted
from a Coq script, reported as a bug in Coq:
https://coq.inria.fr/bugs/show_bug.cgi?id=5705.

-- Paul

Re: [Caml-list] Typing issue in explicit module

[Jacques Garrigue]

This is a known issue to fixing a long standing soundness problem in ocaml 4.04
(I believe you are wrong in saying that it did work in 4.04, it should rather be 4.03 or 4.02).

https://caml.inria.fr/mantis/view.php?id=7313

Basically, non-generalizable type variables in inner modules should be instantiated before
leaving the module, if you want to instantiate them with local types.
This is needed to ensure correct scoping in complex situations.
Your solution is the correct one.

Jacques Garrigue

2017/08/30 4:13, Paul A. Steckler <steck@stecksoft.com>:
> 
> Here's some code that compiles successfully with 4.05.0 ocamlc. The .ml file is:
> 
> .ml file:
> --
>    type t
>    let id x = x
>    let idid = id id
> --
> .mli file:
> --
>  type t
>  val id: 'a -> 'a
>  val idid : t -> t
> --
> 
> If I wrap the code in an explicit module, I get a type error:
> 
> .ml file:
> --
> module Foo =
>  struct
>  <code as before>
>  end
> --
> .mli file:
> --
> module Foo :
> sig
>   <code as before>
> end
> --
> 
> With this change made, ocamlc complains:
> 
> --
> Error: The implementation Foo.ml does not match the interface Foo.cmi:
>       In module Foo:
>       Modules do not match:
>         sig type t = Foo.t val id : 'a -> 'a val idid : '_a -> '_a end
>       is not included in
>         sig type t val id : 'a -> 'a val idid : t -> t end
>       In module Foo:
>       Values do not match:
>         val idid : '_a -> '_a
>       is not included in
>         val idid : t -> t
> --
> 
> Adding a type annotation t -> t to the definition of "idid" gets rid
> of the error.
> 
> With OCaml 4.04.0, no error occurs, and the type annotation is
> unnecessary. Is this change expected?
> 
> The code I've shown is a simplified version of OCaml code extracted
> from a Coq script, reported as a bug in Coq:
> https://coq.inria.fr/bugs/show_bug.cgi?id=5705.
> 
> -- Paul
> 
> -- 
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs