From a73c34fc2e6b2dbe3ba8f4466851b03d29c016d4 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Fri, 8 May 2026 10:36:46 +0100
Subject: fix bug in project: we were not substituting into the looked up field
 set

---
 src/checker_set.rs       | 11 +++++++----
 src/checker_signature.rs | 11 +++++++----
 src/checker_state.rs     |  1 -
 3 files changed, 14 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/checker_set.rs b/src/checker_set.rs
index f0966f6..536a7ec 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -20,7 +20,7 @@ impl CheckerState {
                 let mut new_fields = Vec::new();
                 for Field { name, carries } in fields {
                     let set = ctx.check_set(carries)?;
-                    ctx._recursively_add_hypothetical_element(name.clone(), set.clone(), None)?;
+                    ctx.recursively_add_hypothetical_element(name.clone(), set.clone(), None)?;
                     new_fields.push(Field {
                         name: name.clone(),
                         carries: set,
@@ -76,7 +76,8 @@ impl CheckerState {
     // 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_element(
+    #[instrument(skip(self), level = "debug", fields(%name, %set, head=%head.map(|s| s.to_string()).unwrap_or_default()) )]
+    fn recursively_add_hypothetical_element(
         &mut self,
         name: String,
         set: Set,
@@ -99,7 +100,7 @@ impl CheckerState {
         self.add_element(name.clone(), value, set.clone())?;
         if let Set::Record(fields) = set {
             for f in fields {
-                self._recursively_add_hypothetical_element(f.name, f.carries, Some(&self_element))?;
+                self.recursively_add_hypothetical_element(f.name, f.carries, Some(&self_element))?;
             }
         }
         Ok(())
@@ -308,9 +309,11 @@ impl CheckerState {
                     owner: owner_set,
                 } = self.lookup_record_field(&field)?;
 
+                let field_set = self.check_set(field_set)?;
+
                 // enforce the correct typing of the claimed result
                 if let Some(set) = set
-                    && !self.equal(set, field_set)
+                    && !self.equal(set, &field_set)
                 {
                     return Err(CheckerError::WrongSetForElement {
                         value: element.clone().into(),
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 39a35b4..cc5560d 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -90,7 +90,7 @@ impl CheckerState {
                 let mut new_fields = Vec::new();
                 for Field { carries, name } in fields {
                     let signature = ctx.check_signature(carries)?;
-                    ctx._recursively_add_hypothetical_instance(
+                    ctx.recursively_add_hypothetical_instance(
                         name.clone(),
                         signature.clone(),
                         None,
@@ -106,7 +106,8 @@ impl CheckerState {
         }
     }
 
-    fn _recursively_add_hypothetical_instance(
+    #[instrument(skip(self), level = "debug", fields(%name, %signature, head=%head.map(|s| s.to_string()).unwrap_or_default()) )]
+    fn recursively_add_hypothetical_instance(
         &mut self,
         name: String,
         signature: Signature,
@@ -133,7 +134,7 @@ impl CheckerState {
         self.add_instance(name.clone(), value, signature.clone())?;
         if let Signature::Theory(fields) = signature {
             for f in fields {
-                self._recursively_add_hypothetical_instance(
+                self.recursively_add_hypothetical_instance(
                     f.name,
                     f.carries,
                     Some(&self_instance),
@@ -289,8 +290,10 @@ impl CheckerState {
                     owner: owner_signature,
                 } = self.lookup_signature_field(&field)?;
 
+                let field_signature = self.check_signature(field_signature)?;
+
                 if let Some(signature) = signature
-                    && !self.equal(signature, field_signature)
+                    && !self.equal(signature, &field_signature)
                 {
                     return Err(CheckerError::WrongSignatureForInstance {
                         value: (*instance.clone()).into(),
diff --git a/src/checker_state.rs b/src/checker_state.rs
index c12a2d7..3628432 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -503,7 +503,6 @@ impl CheckerState {
         Ok(canonical)
     }
 
-    #[instrument(skip(self))]
     pub fn make_unique_name(&mut self) -> String {
         let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
         _reserved_name(n, true)
-- 
cgit v1.3.1