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
Segfault from conjunctive constraints #7269
Comments
Comment author: @garrigue Fixed in trunk by commit c7ea9e8. Indeed, this is a delayed unification, so it should be handled the same way as GADT parameters. Note that this is related to GADTs, because otherwise there is no way to export a conjunctive constraint without exporting the enclosing row variable, and such subtyping is not allowed under a row variable. |
Comment author: @stedolan Nice, this fixes the subtyping issue. Now that you point it out, I see that conjunctive constraints are very much like GADT parameters. However, the exhaustivity checker is still too eager to reject conjunctive constraints as unsatisfiable. This program doesn't use subtyping, but still segfaults (on 4.03):
For this example, GADTs aren't strictly necessary. Here's the same program, with the existential row encoded using a polymorphic record field instead:
|
Comment author: @garrigue You're right. |
Comment author: @garrigue Really? fixed in trunk by commit 240fde1. While handling conjunctive types as GADT constraints could be interesting, this would require more work. So for now just make the redundancy check less complete, by having it ignore conflicts in conjunctive types. Hacky but reasonable. Technical note: the common part between gadts and universal record fields is that they use so-called "fixed variant types", which have the property of forcing conjunctive fields appearing in types they are unified to. |
Original bug ID: 7269
Reporter: @stedolan
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2017-09-24T15:32:56Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @gasche @yallop @hcarty
Bug description
The following program segfaults in 4.03.0 (but not previous versions):
The issue is that (
Conj of [
A|B] & [
B]) is judged impossible, since [A|
B] and [B] do not unify, and therefore the pattern matching that f does is considered exhaustive. However, I can in fact construct a (
Conj of [A|
B] & [B]), because covariance yields one from a
Conj [`B].I am unsure exactly what & represents. On one hand, it seems like an intersection or subtyping meet (which should be covariant in both arguments), and on the other it seems like a delayed unification (which should not).
The example uses GADTs, but I don't think they're essential. GADTs are the easiest way to keep a row variable around (the row is existentially quantified), which is necessary to exhibit the bug. I suspect it would also come up with modules and private row types.
The text was updated successfully, but these errors were encountered: