1 files changed, 32 insertions, 5 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index a00ea81..1a89631 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -230,7 +230,7 @@ impl CheckerState {
                             .element;
                         Ok(sub_element)
                     }
-                    _ => panic!(
+                    Element::Inject { .. } | Element::Literal(_) => panic!(
                         "invariant violation: check_element returned neither a record or stuck computation for record set"
                     ),
                 }
@@ -312,7 +312,6 @@ impl CheckerState {
                 let scrutinee = self.check_element(scrutinee, owner)?;
 
                 // which variant are we, if any
-
                 let matching: Option<(String, Element)> = match scrutinee {
                     Element::Inject {
                         ref field,
@@ -326,6 +325,18 @@ impl CheckerState {
                     ),
                 };
 
+                // are we allowed to posit the equality of elements scrutinee =
+                // (arm.tag). (arm.bound) when looking at necessarily
+                // non-matching arms?
+                let posit_equality_with = match &scrutinee {
+                    Element::Var(v) => Some(v.clone()),
+                    Element::Inject { .. }
+                    | Element::Project { .. }
+                    | Element::Case { .. }
+                    | Element::Literal(_)
+                    | Element::Record(_) => None,
+                };
+
                 // 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
@@ -333,7 +344,8 @@ impl CheckerState {
                 let mut processed_arms = Vec::new();
                 for arm in arms {
                     let OwnedField {
-                        field: field_set, ..
+                        field: field_set,
+                        owner,
                     } = self.lookup_variant_field(&arm.tag)?;
 
                     let mut ctx = self.clone();
@@ -345,7 +357,9 @@ impl CheckerState {
                     {
                         let canonical =
                             ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
-                        let output = ctx.check_element((&arm.body).into(), set)?;
+                        let this_set = ctx.check_set(set)?;
+
+                        let output = ctx.check_element((&arm.body).into(), &this_set)?;
                         if matches!(computed_output, Some(_)) {
                             panic!(
                                 "invariant violation: we somehow matched multiple arms in case analysis"
@@ -359,7 +373,20 @@ impl CheckerState {
                         }
                     } else {
                         let canonical = ctx.make_element_binding(binding_name, binding_set)?;
-                        let body = ctx.check_element((&arm.body).into(), set)?;
+
+                        if let Some(ref scrutinee_var) = posit_equality_with {
+                            ctx.make_element_definition(
+                                scrutinee_var.clone(),
+                                Element::Inject {
+                                    field: arm.tag.clone(),
+                                    element: Box::new(Element::Var(canonical.clone())),
+                                },
+                                owner.clone(),
+                            )?;
+                        };
+                        let this_set = ctx.check_set(set)?;
+                        let body = ctx.check_element((&arm.body).into(), &this_set)?;
+
                         CaseArm {
                             tag: arm.tag.clone(),
                             bound: canonical,