From 90e451893671ceebaa37fcb634b5d7a3f153ba70 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 4 May 2026 17:52:04 +0100
Subject: almost done

---
 src/checker_signature.rs | 37 ++++++++++++++++++++++++-------------
 1 file changed, 24 insertions(+), 13 deletions(-)

(limited to 'src/checker_signature.rs')

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 42a581f..30598d3 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -420,18 +420,9 @@ impl CheckerState {
                     other => (other, args.clone()),
                 };
 
-                let subject_sig: Option<Signature> = match &subject {
-                    Instance::Var(v) => Some(self.lookup_instance(v)?.container.clone()),
-                    Instance::Project { field, .. } => {
-                        Some(self.lookup_signature_field(field)?.field.clone())
-                    }
-                    // TODO: i think we need to handle case here
-                    Instance::App { .. }
-                    | Instance::Record(_)
-                    | Instance::SetCoerce(_)
-                    | Instance::For { .. }
-                    | Instance::Case { .. } => None,
-                };
+                // nevertheless we need the tiniest amount of bidirectionality
+                // here to deal with case, project, and var recursively
+                let subject_sig: Option<Signature> = self.stuck_subject_signature(&subject)?;
 
                 if let Some(subject_sig) = subject_sig {
                     let Signature::Ext { params, codomain } = subject_sig else {
@@ -497,7 +488,7 @@ impl CheckerState {
                         })
                     }
                     Instance::Case { .. } => {
-                        todo!("App applied to a Case instance?");
+                        unreachable!("_stuck_subject_signature should have dealt with this")
                     }
                     Instance::Var(_) | Instance::Project { .. } => {
                         unreachable!("handled in the stuck-head branch above")
@@ -533,4 +524,24 @@ impl CheckerState {
             .collect::<Result<Vec<_>, _>>()?;
         Ok((ctx, checked))
     }
+
+    fn stuck_subject_signature(&self, inst: &Instance) -> Result<Option<Signature>, CheckerError> {
+        match inst {
+            Instance::Var(v) => Ok(Some(self.lookup_instance(v)?.container.clone())),
+            Instance::Project { field, .. } => {
+                Ok(Some(self.lookup_signature_field(field)?.field.clone()))
+            }
+            // All arms of a stuck Case share a signature by the case
+            // elimination typing rule, and we've already expanded the body, so
+            // we can pick any arm.
+            Instance::Case { arms, .. } => self
+                .stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body),
+
+            Instance::For { .. } | Instance::Record(_) | Instance::SetCoerce(_) => Ok(None),
+
+            Instance::App { .. } => unreachable!(
+                "invariant violation: _stuck_head_signature called on a left-nested App"
+            ),
+        }
+    }
 }
-- 
cgit v1.3.1