enforce arm match uniqueness again

1 files changed, 8 insertions, 0 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 5410dfe..db47c14 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -307,6 +307,9 @@ impl CheckerState {
                     }
                 };
 
+                // for each arm, recurse with a concrete value (if we have one)
+                // otherwise fall back to hypothetical elements; in the former
+                // case record the end result
                 let mut computed_output = None;
                 for arm in arms {
                     let SetField { field_set, .. } = self.lookup_variant_field(&arm.tag)?;
@@ -326,6 +329,11 @@ impl CheckerState {
                     {
                         new_context.add_element(binding_name, inner.clone().into(), binding_set)?;
                         let output = new_context.check_element(arm.body.clone().into(), set)?;
+                        if matches!(computed_output, Some(_)) {
+                            panic!(
+                                "invariant violation: we somehow matched multiple arms in case analysis"
+                            )
+                        }
                         computed_output = Some(output);
                     } else {
                         new_context.add_element(