1 files changed, 95 insertions, 2 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 89f4441..17154dd 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,3 +1,5 @@
+// Time-stamp: <2026-04-30 17h19 BST (9561bc0c)>
+
 use crate::ast::*;
 use crate::checker_state::*;
 use std::collections::HashMap;
@@ -101,7 +103,6 @@ impl CheckerState {
                     Ok(Instance::Var(v.clone()))
                 }
             }
-
             Instance::Record(assignations) => {
                 if let Some(signature) = signature {
                     let rej = |reason| CheckerError::InstanceDoesNotBelong {
@@ -219,6 +220,98 @@ impl CheckerState {
                     ),
                 }
             }
+            Instance::Case { scrutinee, arms } => {
+                if arms.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "mapping out of bottom types".to_string(),
+                    ));
+                }
+
+                let arm_owners = arms
+                    .iter()
+                    .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner))
+                    .collect::<Result<Vec<_>, _>>()?;
+                let owner = arm_owners[0];
+
+                if !arm_owners.into_iter().all(|o| self.equal(owner, o)) {
+                    todo!("inconsistent case scrutinee set");
+                }
+
+                let Set::Variant(fields) = owner else {
+                    panic!(
+                        "invariant violation: looking up the owner of a variant field resulted in a non-variant set",
+                    )
+                };
+                let mut required_field_names_sorted: Vec<String> =
+                    fields.iter().map(|vf| vf.name.clone()).collect();
+                required_field_names_sorted.sort();
+                let mut covered_field_names_sorted: Vec<String> =
+                    arms.iter().map(|ca| ca.tag.clone()).collect();
+                covered_field_names_sorted.sort();
+                if required_field_names_sorted != covered_field_names_sorted {
+                    return Err(CheckerError::IncompleteCaseAnalysis {
+                        found: covered_field_names_sorted,
+                        required: required_field_names_sorted,
+                    });
+                }
+                let scrutinee = self.check_element(scrutinee, owner)?;
+
+                let matching: Option<(String, Element)> = match scrutinee {
+                    Element::Inject {
+                        ref field,
+                        element: ref inner,
+                    } => Some((field.clone(), *inner.clone())),
+                    Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None,
+                    Element::Literal(_) | Element::Record(_) => panic!(
+                        "invariant violation: scrutinee is a non-variant value at variant set"
+                    ),
+                };
+
+                let mut computed_output = None;
+                let mut processed_arms = Vec::new();
+                for arm in arms {
+                    let Field {
+                        field: field_set, ..
+                    } = self.lookup_variant_field(&arm.tag)?;
+
+                    let mut ctx = self.clone();
+                    let binding_name = arm.bound.clone();
+                    let binding_set = field_set.clone();
+
+                    let case_arm = if let Some((tag, inner)) = &matching
+                        && *tag == arm.tag
+                    {
+                        let canonical =
+                            ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
+                        let output = ctx.check_instance((&arm.body).into(), signature)?;
+                        if matches!(computed_output, Some(_)) {
+                            panic!(
+                                "invariant violation: we somehow matched multiple arms in case analysis"
+                            )
+                        }
+                        computed_output = Some(output.clone());
+                        InstCaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body: output,
+                        }
+                    } else {
+                        let canonical = ctx.make_element_binding(binding_name, binding_set)?;
+                        let body = ctx.check_instance((&arm.body).into(), signature)?;
+                        InstCaseArm {
+                            tag: arm.tag.clone(),
+                            bound: canonical,
+                            body,
+                        }
+                    };
+
+                    processed_arms.push(case_arm);
+                }
+                Ok(computed_output.unwrap_or(Instance::Case {
+                    scrutinee: Box::new(scrutinee),
+                    arms: processed_arms,
+                }))
+            }
             Instance::For {
                 params: inst_params,
                 body,
@@ -372,7 +465,7 @@ impl CheckerState {
                             element: *element.clone(),
                         })
                     }
-                    Instance::Project { .. } | Instance::App(_, _) => {
+                    Instance::Project { .. } | Instance::App(_, _) | Instance::Case { .. } => {
                         // it would appear that we are stuck here, so our only
                         // choice is to continue to be so
                         Ok(Instance::App(Box::new(inner), element.clone()))