fix bug in project: we were not substituting into the looked up field setHEADmain

1 files changed, 7 insertions, 4 deletions

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(),