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 with GADT exhaustiveness #7390
Comments
Comment author: @gasche The Continuous integration reports that this change breaks the build on a warning configured as an error: File "/home/ci/jenkins-workspace/4.04/stdlib/scanf.ml", line 1371, characters 4-123:
|
Comment author: @garrigue Right. I'm trying to fix this, but this looks like a bug in scanf. |
Comment author: @garrigue Note that the type annotation on make_scanf looked like it was explicitly designed to trigger the bug, by leaving an implicit type variable... |
Comment author: @gasche On the other hand, the previous implementation of Scanf had no strict type checking and also had bug. I think we're better off with partially-buggy GADTs than wishful phantom types. |
Original bug ID: 7390
Reporter: @stedolan
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-10-19T14:08:45Z)
Resolution: fixed
Priority: normal
Severity: minor
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Child of: #5998
Monitored by: @yallop
Bug description
Here's a slightly odd implementation of a sum type:
The intent is that a 'filled either' has values 'Either (Y a, N)' and 'Either (N, Y b)'. However, OCaml accepts the following as exhaustive (both 4.03.0 and 4.02.1):
'f' is inferred to have the commented-out type, but curiously OCaml gives an exhaustivity warning if the annotation is uncommented. If accepted as exhaustive, such a type for 'f' is unsound:
The text was updated successfully, but these errors were encountered: