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
Comments
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). |
Comment author: @garrigue According to the discussion in 708, the problem indeed comes from the fix of #6752, as I recalled. At this point the workaround is to add type annotations for non-generalized type variables in submodules. |
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. |
Comment author: @garrigue Actually, reverting to the previous approach does not solve this PR. Sorry for the confusion. 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. |
Comment author: bobot Could someone tag it with target version = 4.04? Thanks in advance. |
Comment author: @garrigue Actually, tagging it as 4.04 is confusing. |
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 |
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:
Strangely if I add a module All that contains all the module, the typing error reappears during the coercion of All. |
Comment author: @alainfrisch This issue is currently marked as "block" and target version = 4.04. Does anyone consider there indeed remains something blocking for 4.04? Otherwise, I would suggest changing the target version. |
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). |
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: 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. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Since it seems that everybody has adapted to the new behaviour, it's maybe time to forget about this; this is harder than I though first. |
I'm closing this as we clearly don't intend to change the behaviour in the short-to-medium term. |
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
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
Additional information
The error is:
The text was updated successfully, but these errors were encountered: