Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typing regression between 4.03 and 4.04 branch with signature coercion. #7313

Open
vicuna opened this issue Aug 2, 2016 · 16 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link

commented Aug 2, 2016

Original bug ID: 7313
Reporter: bobot
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2016-08-04T21:39:54Z)
Resolution: open
Priority: normal
Severity: minor
Target version: later
Category: typing
Has duplicate: #7401
Related to: #3993 #6752 #7152
Monitored by: @gasche @yallop @yakobowski

Bug description

This files with the following signature doesn't compile in 4.4 but compiled before

let mk_fun () = ref (fun () -> assert false)


module R = struct
  module B = struct
    type t_ctx = A
    let f = mk_fun ()
  end
end
module R : sig
  module B : sig
    type t_ctx = A
    val f: (unit -> t_ctx) ref
  end
end

The deep module and the type t_ctx are needed.

It is a reduction of a typing error that occurs from compiling Frama-C with 4.04

Steps to reproduce

boot/ocamlrun ./ocamlc -nostdlib -I stdlib -I byterun/ -o test.cmi test.mli
boot/ocamlrun ./ocamlc -nostdlib -I stdlib -I byterun/ -o test test.ml

Additional information

The error is:

File "../frama-c/test.ml", line 1:
Error: The implementation ../frama-c/test.ml
       does not match the interface ../frama-c/test.cmi:
       In module R:
       Modules do not match:
         sig module B = R.B end
       is not included in
         sig
           module B : sig type t_ctx = A val f : (unit -> t_ctx) ref end
         end
       In module R.B:
       Modules do not match:
         sig type t_ctx = R.B.t_ctx = A val f : (unit -> '_a) ref end
       is not included in
         sig type t_ctx = A val f : (unit -> t_ctx) ref end
       In module R.B:
       Values do not match:
         val f : (unit -> '_a) ref
       is not included in
         val f : (unit -> t_ctx) ref
       File "../frama-c/test.ml", line 9, characters 8-9: Actual declaration
@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 2, 2016

Comment author: @mshinwell

I've seen an error like this on a Jane Street tree with 4.04, again involving a non-generalised type variable. A temporary workaround for me was to add a type annotation in the .ml file (without the offending type variable; write the type from the .mli).

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 2, 2016

Comment author: @gasche

I would try to see if #708 (merge commit 44e0384)

#708

is guilty of this regression. (Maybe a level adjustment problem somewhere in there.)

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 2, 2016

Comment author: bobot

Indeed d894ba1 works and 44e0384 fails

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 2, 2016

Comment author: @garrigue

I seem to remember seeing a similar problem occurring a few weeks ago, before the merge of #708, but after my reverting to strict scoping on #6752, but I cannot find the any trace of it anymore.
Anybody has seen that?
At first I thought it was the same problem.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 4, 2016

Comment author: @garrigue

According to the discussion in 708, the problem indeed comes from the fix of #6752, as I recalled.
The answer is that indeed the behavior is now more restrictive than before, in that we do not allow to instantiate non-generalizable variables with types coming from the same module, except for toplevel ones when a coercion is used. This was required to close a soundness bug.
I would be happy to revert to the old behavior, if somebody could come up with the specification of what was supposed to be allowed.

At this point the workaround is to add type annotations for non-generalized type variables in submodules.
I'll try to have a look on Monday on whether we could at least allow coercions to work for submodules too, since this seems to be the most offending part of the change.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 8, 2016

Comment author: @garrigue

With a better investigation, the problem seems to come from the need to fix #7152.

Concretely, this is related to the following type:

module Dem : sig
  module Data : sig type t = make_dec end
  val key : '_a Fast.t
end

You should instantiate '_a by either Data.t or Dem.Data.t, depending on whether you are looking at the type from inside Dem or outside Dem. Since the variable is shared between the two, actually both are invalid. So the solution to 7152 solved this by forcing the expansion, and instantiating by make_dec, which is correct. But this also means that you cannot instantiate such a non-generalizable type variable by an internal abstract type (except when you are coercing before adding the module definition to the environment, since the locking is only done afterward).

I understand that all this kind of worked until 4.02.3, but my feeling is that this was purely by chance. Something like lazyness allowing one to instantiate with an internal reference before the exporting substitution occurs, so that the internal-external conflict is avoided.

If I revert to the mechanism used before, i.e. creating the id for the module name only after type its body, then everything works fine, except #7152.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 8, 2016

Comment author: @garrigue

Actually, reverting to the previous approach does not solve this PR. Sorry for the confusion.
The real cause is probably a change in evaluation order somewhere, but I'm not sure it's worth tracking it down, because it is bound to be fragile.

Just to give you an idea of how the original approach was fragile, it was sufficient to add the line

  let _ = Dem.key

just after the definition of Dem in #7152 to break it in all versions up to 4.02.
4.03 fixed it, but only by making things more laxist, and had other problems.
The more restrictive approch in 4.04 fixes it once and for all.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 18, 2016

Comment author: bobot

Could someone tag it with target version = 4.04? Thanks in advance.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 18, 2016

Comment author: @garrigue

Actually, tagging it as 4.04 is confusing.
I'm keeping open, as I think the question of how to handle non-generalizable variables in modules is still open.
However, I have no solution for it that doesn't break something else, so there is no plan to fix the regression for 4.04.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 23, 2016

Comment author: bobot

@garrigue Ah okay, I was afraid that was the plan. So I must find a way to automate @mshinwell workaround before 4.04 since it seems we have at least 287 such cases in Frama-C (all the mk_* applications in 1).

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 23, 2016

Comment author: bobot

If fact the number of problematic case was a lot less only 12. And there is another workaround since it was in a submodule I just copy pasted its signature in the .ml file (simpler for future modification of the code).

The workaround applied on test.ml:

let mk_fun () = ref (fun () -> assert false)


module R:
 sig
  module B : sig
    type t_ctx = A
    val f: (unit -> t_ctx) ref
  end
end = struct
  module B = struct
    type t_ctx = A
    let f = mk_fun ()
  end
end

Strangely if I add a module All that contains all the module, the typing error reappears during the coercion of All.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 30, 2016

Comment author: @alainfrisch

This issue is currently marked as "block" and tagre version = 4.04. Does anyone consider there indeed remains something blocking for 4.04? Otherwise, I would suggest changing the target version.

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 30, 2016

Comment author: bobot

At least two OCaml code had the problem (frama-c and janestreet code). Even if we have been able to hack around the problem, I think other library or tools will also have the problem.

Unfortunately the fix seems not clear. If it is not corrected, I think it mandates a comment in the release annoucement (at least in the changelog, better in the message).

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 30, 2016

Comment author: @garrigue

Added a more precise comment in the changelog, for #6752, but citing this PR too.
Commit 156592d in branch 4.04.

@vicuna

This comment has been minimized.

Copy link
Author

commented Nov 4, 2016

Comment author: @gasche

Is #7401 a duplicate of this issue?

#7401

@vicuna

This comment has been minimized.

Copy link
Author

commented Dec 13, 2016

Comment author: @garrigue

Indeed, #7401 is a consequence of the stricter typing of submodules.

Note that we cannot just go back to the statu quo ante:
#7414 is an example of why the previous approach was wrong (a laxist approach to scoping allowed to use functors to break soundness).

I have some idea for allowing examples where the type can be trivially found in the mli, but it is harder than I thought first.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.