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

When pattern matching on GADTs, abstract (phantom) types are not considered structurally different from concrete ones #7360

Closed
vicuna opened this issue Sep 16, 2016 · 12 comments

Comments

@vicuna
Copy link

vicuna commented Sep 16, 2016

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

@vicuna
Copy link
Author

vicuna commented Sep 17, 2016

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
could be

module M :sig type a type b 
  type 'a e= A : a e | B : b e
  val trick: a e 
end =
  struct
    type a type b=a
    type 'a e= A : a e | B : b e
    let trick = B
  end

include M

Due to the value trick, the following function is clearly not total

let f : a e -> a e = function
  | A -> A

and the type-checker is right to warn about the non-exhaustiveness of the warning.

@vicuna
Copy link
Author

vicuna commented Sep 17, 2016

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.

@vicuna
Copy link
Author

vicuna commented Sep 17, 2016

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 b = B

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.

@vicuna
Copy link
Author

vicuna commented Sep 18, 2016

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?

@vicuna
Copy link
Author

vicuna commented Sep 18, 2016

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:
#5985

@vicuna
Copy link
Author

vicuna commented Sep 18, 2016

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.

@vicuna
Copy link
Author

vicuna commented Sep 19, 2016

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).

@vicuna
Copy link
Author

vicuna commented Sep 20, 2016

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.

@vicuna
Copy link
Author

vicuna commented Sep 20, 2016

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) =
struct
let f : (X.a, X.b) eq option -> unit
= fun None -> ()
end

module G = F(struct type a = float and b = int end)
module H = F(struct type a = int and b = int end)

@vicuna
Copy link
Author

vicuna commented Sep 20, 2016

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.

@vicuna
Copy link
Author

vicuna commented Sep 20, 2016

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:
type a
type b
val a_eq_b : (a, b) eq
end

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.

@vicuna
Copy link
Author

vicuna commented Sep 20, 2016

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant