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

Segfault with GADT exhaustiveness #7390

Closed
vicuna opened this Issue Oct 19, 2016 · 6 comments

Comments

Projects
None yet
2 participants
@vicuna
Copy link
Collaborator

commented Oct 19, 2016

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:

type empty = Empty and filled = Filled
type ('a,'fout,'fin) opt =
  | N : ('a, 'f, 'f) opt
  | Y : 'a -> ('a, filled, empty) opt

type 'fill either =
  | Either : (string, 'fill, 'f) opt * (int, 'f, empty) opt -> 'fill either

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

let f (* : filled either -> string *) =
  fun (Either (Y a, N)) -> a

'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:

# print_string (f (Either (N, Y 4)));;
Segmentation fault
@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

Comment author: @garrigue

Fixed in 4.04 by commit 958d234.

Always adjust levels before checking exhaustiveness or redundancy.

@vicuna vicuna closed this Oct 19, 2016

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

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:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Nil
File "/home/ci/jenkins-workspace/4.04/stdlib/scanf.ml", line 1:
Error: Some fatal warnings were triggered (1 occurrences)

I don't have the time to investigate this right now.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

Comment author: @garrigue

Right. I'm trying to fix this, but this looks like a bug in scanf.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

Comment author: @garrigue

The warning in scanf.ml is fixed by commit 5fa0eed, but this should be checked by the maintainer of scanf. I don't think this is Pierre Weis anymore, despite the header.

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

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...
That's the scary thing with advanced type systems: people believe so much in them that they end up finding holes that let them write what they want, thinking that this is just the type system that is more clever than them...

@vicuna

This comment has been minimized.

Copy link
Collaborator Author

commented Oct 19, 2016

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.