separability and with-constraints: fix for bug #9607#9609
separability and with-constraints: fix for bug #9607#9609gasche merged 4 commits intoocaml:trunkfrom
Conversation
…Stephen Dolan Currently the test fails while it should work.
|
The change looks good to me, but it seems like there's an unrelated change to the testsuite that snuck in. I was wondering whether this bug could occur anywhere else. My intuition is that whenever |
|
I was already wondering how to get a static check that we are recomputing this in all the right place, but thanks for the other occurrence. I need to think about it more. |
|
@stedolan the code you are pointing out seems to be there to deal with private row types. Apparently those are handled by a "shadow" type declaration for the row variable, which is fully abstract (and private), followed by a "real" definition for the private type itself, using the shadow row identifier as its row variable. In particular, there is no reason for the private row variable to have a non-default separability (it is purely abstract at this point). The separability choice there is sound (of course, by default we make the conservative choice of preventing unboxing) but I also have the impression that we could not do better in this case. I think that the reason why there is a non-trivial variance computed is that you need the variance of the row variable to be compatible with the variance of the rest of the type. (I don't understand the details of the variance computation on pairs of booleans, though.) |
|
Thanks for the explanation! |
|
(the build seems to pass even though a reference file was deleted, so it seems it wasn't needed. leftover from a conversion to expect tests?) |
|
Sorry for not answering earlier. The reference file was dead code (it's mentioned in the commit message that removes it), I suppose from a previous version of the code that did not use expect-style tests (which need no reference file). Ideally I would still like to make the code more robust so that people adding new kind of variance-like data do not make the same mistake we did, but I think this could and should go in a separate PR. In particular, the current PR will go to 4.11, while a robustification one needs not. |
ae65c52 to
9b1bfc3
Compare
|
I tried several approaches to being careful about whether properties are defined or not (based on creating type parameters for them that would be |
|
I merged, and cherry-picked in 4.11 ( 35039ea ). |
|
Rebasing on top of that patch, we now get an uncaught exception. I'm not able to provide a repro case yet but I can share the backtrace with you in case it's of any use. |
|
It took me a bit of time to figure it out (but most of the time was spent trying to write a correct emacs-lisp regexp to parse the new backtrace format to easily jump around the trace), but I suspect that the reason is that the source uses a type construction from a compilation unit whose The trace is a bit hard to read due to the fact that your compiler variant uses The place where the exception is raised looks like this in | (Tconstr(path,tys,_), m ) ->
let msig = (Env.find_type path env).type_separability in
...but earlier in the stale part of trace we can find a place in | Tconstr(p, _args, _abbrev) ->
begin try
let type_decl = Env.find_type p env in
type_decl.type_immediate
with Not_found -> Type_immediacy.Unknown
(* This can happen due to e.g. missing -I options,
causing some .cmi files to be unavailable.
Maybe we should emit a warning. *)
endHere is my current hypothesis for what is happening: you have an I would have preferred if the "immediacy" function had emitted a warning indeed, because this would have been helpful to locate the problem. I will have to add the same workaround/hack in |
|
I don't know how to write a testcase for this potential failure. My attempt, taking inspiration from |
|
@hhugo could you try redoing the build with the following workaround ? |
|
gasche@2a142de does fix the uncaught exception but it seems I still hit an occurrence of #9607. I'll try to get you a repro case. |
|
Thanks! |
|
The following use to compile and no longer does. I'm not sure how much it's related to #9607 module Private_variant = struct
type 'a t = A : 'e -> 'e t
end
module type Public = sig
module Event : sig
type 'e t = 'e Private_variant.t
end
type t = T : 'e Event.t -> t [@@unboxed]
end
module type Component = sig
include Public
module type Public = Public
with type 'e Event.t = 'e Event.t
and type t = t
endHere is the error I get with your latest patch |
|
Thanks! This is great, because it also gives a repro case for the |
|
@hhugo could you open a new issue with this repro case? I believe that there is an interesting bug lying somewhere around it (possibly also affecting immediacy and variance), and it would be nice to have a new PR number to refer to it and potential fixes. |
|
A slightly simpler repro case: module type Sig = sig
type 'a ind = 'a * int
type t = T : 'e ind -> t [@@unboxed]
end
module type Problem = sig
include Sig
module type ReboundSig = Sig
with type 'a ind = 'a ind
and type t = t
end |
|
I opened a draft PR with a preliminary fix in #9623. |
This PR fixes #9607, reported by @stedolan (thanks!). The issue is a bit silly: in typedecl, "properties" must be computed in two places (
transl_type_decl, but alsotransl_with_constraintthat handles with-constraints), and we didn't know about the second one.@stedolan would you by chance be willing to review the fix?