summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-02-26 16:08:32 +0000
committerAlasdair Armstrong2018-02-26 16:11:30 +0000
commite91a8c8659d08178dfec45a06529ade208ded186 (patch)
tree9d7191b96eef2cec20cf907912f50da1ff4f877f
parentee123e2876c4fa5ae000256caeb7eb810e8c05f8 (diff)
Fix missing case in pattern completeness check
Fixes #4
-rw-r--r--src/pattern_completeness.ml3
-rw-r--r--test/typecheck/pass/pat_completeness.sail11
2 files changed, 12 insertions, 2 deletions
diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml
index ebb402e5..94623e6f 100644
--- a/src/pattern_completeness.ml
+++ b/src/pattern_completeness.ml
@@ -232,8 +232,7 @@ let rec join ctx gpat1 gpat2 =
| None, None -> None
| Some args1, None -> Some args1
| None, Some args2 -> Some args2
- | Some args1, Some args2 ->
- assert false
+ | Some args1, Some args2 -> Some (join ctx args1 args2)
in
let ctors = Bindings.merge ctor_merge ctors1 ctors2 in
if Bindings.for_all (fun _ gpat -> is_wild gpat) ctors then
diff --git a/test/typecheck/pass/pat_completeness.sail b/test/typecheck/pass/pat_completeness.sail
new file mode 100644
index 00000000..fd4a7757
--- /dev/null
+++ b/test/typecheck/pass/pat_completeness.sail
@@ -0,0 +1,11 @@
+union option ('a : Type) = {None, Some : 'a}
+
+union ast = {Foo : unit}
+
+let x : option(ast) = Some(Foo)
+
+let y : unit = match(x) {
+ Some(Foo) => (),
+ Some(a) => (),
+ None => ()
+} \ No newline at end of file