1 files changed, 19 insertions, 21 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 86661c7..2bd011d 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -35,7 +35,7 @@ impl CheckerState {
                 Ok(Set::Variant(fields))
             }
             Set::ClaimedSet(instance) => {
-                let instance = self.check_instance(instance, &Signature::Set)?;
+                let instance = self.check_instance(instance, Some(&Signature::Set))?;
                 Ok(Set::ClaimedSet(instance))
             }
             Set::Var(v) => {
@@ -313,40 +313,38 @@ impl CheckerState {
                         field: field_set, ..
                     } = self.lookup_variant_field(&arm.tag)?;
 
-                    let mut new_context = self.clone();
+                    let mut ctx = self.clone();
                     let binding_name = arm.bound.clone();
                     let binding_set = field_set.clone();
 
-                    let body = if let Some((tag, inner)) = &matching
+                    let case_arm = if let Some((tag, inner)) = &matching
                         && *tag == arm.tag
                     {
-                        new_context.add_element(
-                            binding_name.clone(),
-                            inner.clone().into(),
-                            binding_set,
-                        )?;
-                        let output = new_context.check_element(arm.body.clone().into(), set)?;
+                        let canonical =
+                            ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
+                        let output = ctx.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.clone());
-                        output
+                        CaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body: output,
+                        }
                     } else {
-                        new_context.add_element(
-                            binding_name.clone(),
-                            Value::Hypothetical,
-                            binding_set,
-                        )?;
-                        new_context.check_element(arm.body.clone().into(), set)?
+                        let canonical = ctx.make_element_binding(binding_name, binding_set)?;
+                        let body = ctx.check_element(arm.body.clone().into(), set)?;
+                        CaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body,
+                        }
                     };
 
-                    processed_arms.push(CaseArm {
-                        tag: arm.tag.clone(),
-                        bound: binding_name,
-                        body,
-                    });
+                    processed_arms.push(case_arm);
                 }
                 Ok(computed_output.unwrap_or(Element::Case {
                     scrutinee: Box::new(scrutinee),