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

Missing exhaustivity check for extensible variant #7330

Closed
vicuna opened this issue Aug 20, 2016 · 4 comments
Closed

Missing exhaustivity check for extensible variant #7330

vicuna opened this issue Aug 20, 2016 · 4 comments
Assignees

Comments

@vicuna
Copy link

vicuna commented Aug 20, 2016

Original bug ID: 7330
Reporter: Elarnon
Assigned to: @garrigue
Status: resolved (set by @garrigue on 2016-08-22T01:03:37Z)
Resolution: fixed
Priority: normal
Severity: crash
Version: 4.03.0
Fixed in version: 4.04.0 +dev / +beta1 / +beta2
Category: typing
Monitored by: @gasche @yallop

Bug description

When compiling non-exhaustive pattern-matching (i.e. without a catch-all clause) on extensible variant types in 4.03.0:

(a) No warning is emitted at compile time. 4.02.3 properly emits a Warning 8.

(b) Ill-typed code is executed at runtime. 4.02.3 properly raises a Match_failure exception.

This behavior was reproduced using opam's 4.03.0 (i.e. no flambda) version on OSX, Debian testing and Archlinux machines, see attached file for code that compiles without warning in 4.03.0 but segfaults when executed. It is still present in opam's 4.04.0+beta1.

File attachments

@vicuna
Copy link
Author

vicuna commented Aug 21, 2016

Comment author: @gasche

git bisect tells me that the issue was introduced in the gadt-warnings branch:

commit c88f3d0
Author: Jacques Garrigue
Date: Tue May 19 22:52:21 2015 +0000

Improved exhaustiveness warnings for GADTs, with non-deterministic in type_pat

git-svn-id: http://caml.inria.fr/svn/ocaml/branches/gadt-warnings@16133 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02

c88f3d0

@vicuna
Copy link
Author

vicuna commented Aug 22, 2016

Comment author: @garrigue

Fixed in 4.04 branch by commit b4b21d6.

Extra extension constructors were represented by an untypable pattern.
Fixed by switching to a variable, but this requires hacks for nice warnings.

@vicuna vicuna closed this as completed Aug 22, 2016
@vicuna
Copy link
Author

vicuna commented Oct 7, 2016

Comment author: @alainfrisch

I've cherry-picked this from 4.04 to trunk (commit 4950410).

@vicuna
Copy link
Author

vicuna commented Nov 3, 2016

Comment author: @edwintorok

I've just run into this segfault, when having a non-exhaustive match on an exception (4.02.3 and 4.04.0+trunk correctly print the warning and raise Match_failure, 4.03.0 segfaults), I think this is because exceptions are like open variants internally.

Here are two testcases, please consider adding them to your testsuite as well:

(* ocamlopt excrash.ml -o excrash && ./excrash *)
exception Custom of string list
type ('a,'b) result = Ok of unit | Error of 'b
let failme () = Error (Failure "test")

let handle = function
| Ok () -> 0
| Error (Custom lst) -> List.length lst

let () = failme () |> handle |> string_of_int |> print_endline

(* ocamlopt varcrash.ml -o varcrash && ./varcrash *)
type t = ..

type t += Custom of string list
type t += A of string

type ('a,'b) result = Ok of 'a | Error of 'b
let failme () = Error (A "test")

let handle = function
| Ok () -> 0
| Error (Custom lst) -> List.length lst

let () = failme () |> handle |> string_of_int |> print_endline

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

2 participants