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.

Sign up for GitHub

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

Jump to bottom

Treat empty variants as GADTs for exhaustiveness check #9309

Closed
wants to merge 5 commits into from
Closed

Treat empty variants as GADTs for exhaustiveness check #9309

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9e86263
Add a test showing that the exhaustiveness check doesn't work with th…
smuenzel-js Feb 17, 2020
5d41ade
Treat empty variants as GADTs for exhaustiveness check
smuenzel-js Feb 17, 2020
dcb5896
Update comments related to empty type
trefis Feb 17, 2020
c60af1a
Add simpler test for empty type pattern match
Octachron Feb 17, 2020
b469d2a
use unsuitable branch terminology
smuenzel-js Feb 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
4 changes: 4 additions & 0 deletions Changes
View file
Open in desktop
Expand Up @@ -210,6 +210,10 @@ Working version

### Bug fixes:

- #9309: Treat the empty variant as a GADT in or-patterns, so that the
exhaustiveness check will examine all cases in the or pattern.
(Stefan Muenzel, report by Robert Head, review by ????)

- #7683, #1499: Fixes one case where the evaluation order in native-code
may not match the one in bytecode.
(Nicolás Ojeda Bär, report by Pierre Chambart, review by Gabriel Scherer)
Expand Down
34 changes: 34 additions & 0 deletions testsuite/tests/typing-misc/empty_variant.ml
View file
Open in desktop
Expand Up @@ -29,3 +29,37 @@ let f : t option -> int = function None -> 3
[%%expect{|
val f : t option -> int = <fun>
|}]


type nothing = |
type ('a, 'b, 'c) t = | A of 'a | B of 'b | C of 'c
module Runner : sig
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Concerning the test, a simpler

type nothing = |
type 'b t = A | B of 'b | C
let g (x:nothing t) = match x with A -> ()

triggers this issue. Did you have a specific reason in mind for the current test?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a simplified version of the error that we observed in our code base -- that's how I derived it. No preference on whether we should use the simpler one or not.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think keep at least adding the simpler error case is useful, since it makes it clearer what is the intend of the test.

val ac : f:((unit, _, unit) t -> unit) -> unit
end = struct
let ac ~f =
f (A ());
f (C ());
;;
end

let f () =
Runner.ac
~f:(fun (abc : (_,nothing,_) t) ->
let value =
match abc with
| A _ -> 1
in
Printf.printf "%i\n" value
)
[%%expect{|
type nothing = |
type ('a, 'b, 'c) t = A of 'a | B of 'b | C of 'c
module Runner : sig val ac : f:((unit, 'a, unit) t -> unit) -> unit end
Lines 16-17, characters 8-18:
16 | ........match abc with
17 | | A _ -> 1
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
C ()
val f : unit -> unit = <fun>
|}]
4 changes: 3 additions & 1 deletion typing/typecore.ml
View file
Open in desktop
Expand Up @@ -1282,7 +1282,9 @@ and type_pat_aux
| Counter_example ({explosion_fuel; _} as info) ->
let open Parmatch in
begin match ppat_of_type !env expected_ty with
| PT_empty -> raise (Error (loc, !env, Empty_pattern))
| PT_empty ->
if must_backtrack_on_gadt then raise Need_backtrack;
raise (Error (loc, !env, Empty_pattern))
| PT_any -> k' Tpat_any
| PT_pattern (explosion, sp, constrs, labels) ->
let explosion_fuel =
Expand Down