From 77d637846be1eb0d140612731c80ca7a6cf1bb29 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Thu, 7 May 2026 15:33:30 +0100
Subject: fix failure to add hypotheticals for instances of compound signatures

---
 src/checker_signature.rs | 52 +++++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 47 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 6acd271..55682a9 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -90,11 +90,11 @@ impl CheckerState {
                 let mut new_fields = Vec::new();
                 for Field { carries, name } in fields {
                     let signature = ctx.check_signature(carries)?;
-                    ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?;
-                    // And lo, the special case, our chosen canonical form
-                    if signature == Signature::Set {
-                        ctx.add_set(name.clone(), Set::ClaimedSet(Instance::Var(name.clone())))?;
-                    }
+                    ctx._recursively_add_hypothetical_instance(
+                        name.clone(),
+                        signature.clone(),
+                        None,
+                    )?;
                     new_fields.push(Field {
                         name: name.clone(),
                         carries: signature,
@@ -112,6 +112,48 @@ impl CheckerState {
         }
     }
 
+    // the goal here is to spread the love: if we are adding a hypothetical of
+    // some signature _ : theory { ... } then we must recurse into all of those
+    // fields and add hypotheticals for them---but, we need to build the tree as
+    // we go, giving them the concrete value of their path from the root (our
+    // canonical form).
+    fn _recursively_add_hypothetical_instance(
+        &mut self,
+        name: String,
+        signature: Signature,
+        head: Option<&Instance>,
+    ) -> Result<(), CheckerError> {
+        let value = match head {
+            Some(h) => InstanceValue::Concrete(Instance::Project {
+                instance: Box::new(h.clone()),
+                field: name.clone(),
+            }),
+            None => InstanceValue::Hypothetical,
+        };
+        let self_instance = match head {
+            Some(h) => Instance::Project {
+                instance: Box::new(h.clone()),
+                field: name.clone(),
+            },
+            None => Instance::Var(name.clone()),
+        };
+        // handle the special case canonical form for _ :: Set
+        if signature == Signature::Set {
+            self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()))?;
+        }
+        self.add_instance(name.clone(), value, signature.clone())?;
+        if let Signature::Theory(fields) = signature {
+            for f in fields {
+                self._recursively_add_hypothetical_instance(
+                    f.name,
+                    f.carries,
+                    Some(&self_instance),
+                )?;
+            }
+        }
+        Ok(())
+    }
+
     #[instrument(skip(self), level = "debug", fields(%instance, signature=%signature.map(|s| s.to_string()).unwrap_or_default()) )]
     pub fn check_instance(
         &self,
-- 
cgit v1.3.1