[Caml-list] typechecking in 4.05+beta2

[Caml-list] typechecking in 4.05+beta2

[Virgile Prevosto]

Dear list,

while playing with the new beta, I stumbled upon the following issue.
The program below is now rejected by the compiler, while this was not
the case with 4.04.

--- test.mli:
module M(E: sig type t end): sig
type t
val u: t -> t -> t
end

--- test.ml:
module M(E: sig type t end) = struct
type t = (E.t, unit) Hashtbl.t
let u = Hashtbl.fold (fun x () h -> Hashtbl.add h x (); h)
end

---
ocamlc test.mli
ocamlc test.ml
File "test.ml", line 1:
Error: The implementation test.ml does not match the interface test.cmi:
       ...
       At position module M(E) : <here>
       Modules do not match:
         sig
           type t = (E.t, unit) Hashtbl.t
           val u :
             ('_a, unit) Hashtbl.t ->
             ('_a, unit) Hashtbl.t -> ('_a, unit) Hashtbl.t
         end
       is not included in
         sig type t val u : t -> t -> t end
       At position module M(E) : <here>
       Values do not match:
         val u :
           ('_a, unit) Hashtbl.t ->
           ('_a, unit) Hashtbl.t -> ('_a, unit) Hashtbl.t
       is not included in
         val u : t -> t -> t
       File "test.ml", line 3, characters 4-5: Actual declaration

It is quite easy to fix, but I was wondering whether this restriction
in type unification when checking the conformance of .ml and .mli was
intended, and if yes, what is the reason behind it?
Note that this is of course a reduction of the initial code, and all
ingredients seems to be needed.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile

Re: [Caml-list] typechecking in 4.05+beta2

[Virgile Prevosto]

Dear list,

2017-02-22 19:54 GMT+01:00 Virgile Prevosto <virgile.prevosto@m4x.org>:
> while playing with the new beta, I stumbled upon the following issue.
> The program below is now rejected by the compiler, while this was not
> the case with 4.04.
> [snip]

I've bisected the issue and it is apparently caused by commit
2bd22967b that fixes mantis issue 7414, which is about weak type
variables and first-class modules. I don't know the type-checker well
enough to understand whether it is possible to accept my example while
rejecting the one from MPR#7414.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile

Re: [Caml-list] typechecking in 4.05+beta2

[Gabriel Scherer]

Thanks for the bisection work. The related code change reproduces, at
the level of functors, a change in handling of non-generalized
inference variables that was done at the module level in 4.04, and for
which there were a couple similar known regressions. I believe that
the conclusion would be the same here : it is unfortunate that your
code breaks, but we don't expect the new behavior of 4.05 (which plugs
a small soundness hole in the type system) to change to become more
permissive again.

( I posted in essence the same comment on the relevant pull request
discussion: https://github.com/ocaml/ocaml/pull/929#issuecomment-282283191
)

On Fri, Feb 24, 2017 at 3:47 AM, Virgile Prevosto
<virgile.prevosto@m4x.org> wrote:
> Dear list,
>
> 2017-02-22 19:54 GMT+01:00 Virgile Prevosto <virgile.prevosto@m4x.org>:
>> while playing with the new beta, I stumbled upon the following issue.
>> The program below is now rejected by the compiler, while this was not
>> the case with 4.04.
>> [snip]
>
> I've bisected the issue and it is apparently caused by commit
> 2bd22967b that fixes mantis issue 7414, which is about weak type
> variables and first-class modules. I don't know the type-checker well
> enough to understand whether it is possible to accept my example while
> rejecting the one from MPR#7414.
>
> Best regards,
> --
> E tutto per oggi, a la prossima volta
> Virgile
>
> --
> 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

Re: [Caml-list] typechecking in 4.05+beta2

[Virgile Prevosto]

2017-02-24 17:14 GMT+01:00 Gabriel Scherer <gabriel.scherer@gmail.com>:
> Thanks for the bisection work. The related code change reproduces, at
> the level of functors, a change in handling of non-generalized
> inference variables that was done at the module level in 4.04, and for
> which there were a couple similar known regressions. I believe that
> the conclusion would be the same here : it is unfortunate that your
> code breaks, but we don't expect the new behavior of 4.05 (which plugs
> a small soundness hole in the type system) to change to become more
> permissive again.
>
> ( I posted in essence the same comment on the relevant pull request
> discussion: https://github.com/ocaml/ocaml/pull/929#issuecomment-282283191
> )
>

Thanks for your answer. I saw your comment on github that confirmed my
fears ;-). Anyway, the fix is indeed only a couple of eta-expansions
or type annotations and we can live with that.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile