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
When pattern matching on GADTs, abstract (phantom) types are not considered structurally different from concrete ones #7360
Comments
Comment author: @Octachron As far as I can see, this is a duplicate of #7028, i.e. there is not enough information for the type-checker to prove that the two abstract types cannot be equal in another context. As an illustration of the problem, a variation of the phantom4.ml example
Due to the value
and the type-checker is right to warn about the non-exhaustiveness of the warning. |
Comment author: rlepigre Well, of course two arbitrary abstract types cannot be considered different. My point is, phantom types can always be considered different (e.g. a and b are different in phantom1.ml). In other words, (abstract) phantom types should be distinguished from other abstract types in some way. |
Comment author: @gasche I believe this is not a bug. Once a abstract type declaration has been hideen under a type signature, there is no way to tell anymore whether it is just abstract or also never-defined (it would only be sound to consider non-defined types distinct). It is perfectly correct that phantom4 fails to compile (there is no sound way to accept it that does not break separate compilation of modules), the surprising part is rather than phantom2 works. This issue is relatively well-known among authors of GADTs, and the common pattern is to give an explicit definition to "phantom" types: type a = A type _ t = X : a t | Y : b t I vote to close this ticket as "not a bug", but will wait a bit to let others give their opinion. |
Comment author: rlepigre OK, that's what I do to solve the problem in my code. However I find it rather annoying that we need to rely on such a trick. Especially since we need to expose the constructors A and B for things to work out. I think that the representation of abstract types in modules should contain a flag defined/not defined. And of course, two such modules would only have compatible signatures if the flags coincide (but I would not go as far as giving a syntactic counterpart to this). Wouldn't this be feasible, sound and preserve separate compilation of modules? |
Comment author: @gasche Well, if you don't have a syntactic counterpart to this, then you cannot express (syntactically) the signatures that let that information transpire, so the solution that goes through an intermediate module signature (your phantom4) still won't work. Part of the discussion in #5985 is about these issues, you may find it interesting: |
Comment author: rlepigre I'm not sure I agree. It is probably possible to propagate the information (that a given type is never defined) internally. The syntax is not important here as a user does not need to know if an abstract type has actually been defined or not. This is just a matter of improving the heuristic for ruling out unreachable branches in pattern matching. I'll have a look at the link, thanks Gabriel. |
Comment author: @alainfrisch What does it mean for a type to have never been defined? I don't see how to define such a "flag" in module types without (i) breaking transivity (i.e. a module type is always a subtype of itself); or (ii) breaking the property that two "never defined" types are different in all contexts (and can thus be assumed to be incompatible). |
Comment author: rlepigre Actually I changed my mind about one thing I said earlier : "abstract types cannot be considered different". After talking with Christophe Raffalli about this, we convinced ourselves that two (different) abstract types should always be considered different. Indeed, if your code contains several abstract types t1, t2, ... tn then you can always rewrite your code using t1' = {lt1 = t1}, t2' = {lt2 = t2}, ... tn' = {ltn = tn} (where lt1, lt2, ... ltn are unique record labels). Of course, you can rewrite the code because ti and ti' are isomorphic for all i, but then all the couple (ti', tj') are indeed different (for all i, j such that i is not equal to j). This seems to show that, when pattern matching on GADTs, abstract types (and not only phantom types) can always be considered different. |
Comment author: @yallop You can indeed often (not always) rewrite code to use fresh nominal types such as records to ensure distinctness. But it's not safe for the compiler to assume that arbitrary abstract types are distinct. In the following example, if X.a and X.b are distinct then the pattern matching in f is exhaustive. If they're equal then the pattern matching is not exhaustive. Within the body of F it isn't known whether they're distinct. And they can later be instantiated to be either distinct (G) or equal (H). type (_, _) eq = Refl : ('a, 'a) eq module F(X: sig type a and b end) = module G = F(struct type a = float and b = int end) |
Comment author: rlepigre Here X.a and X.b are not abstract types as they have not been instantiated (they are only the parameters of a functor). I think that what you are saying is that such parameters are not distinguished from abstract types in the implementation. |
Comment author: @yallop X.a and X.b are abstract within the body of F. I think you may be using an unusual definition of "abstract" here. And the same situation can arise even a and b are defined in a top-level module rather than a functor parameter. For example, here's the signature of a top-level module X: module X: Examining a_eq_b in a suitable context reveals to the type-checker that a and b are equal. So it's not safe to assume that they're distinct. |
Comment author: rlepigre OK, I see: GADTs themselves can make abstract types equal. I guess my problem cannot be solved then. And I don't really care as I can always give a dummy definition to my "phantom" types. Thanks for the discussion. |
Original bug ID: 7360
Reporter: rlepigre
Status: resolved (set by @damiendoligez on 2016-09-28T12:18:15Z)
Resolution: won't fix
Priority: normal
Severity: minor
Version: 4.03.0
Category: typing
Duplicate of: #7028
Related to: #5985
Monitored by: @gasche @yallop
Bug description
A GADT which uses abstract types (or phantom types defined in another module) leads to problems with pattern matching exhaustiveness checking. See the examples.
Steps to reproduce
Just call "ocaml" on the example files.
File attachments
The text was updated successfully, but these errors were encountered: