From a73c34fc2e6b2dbe3ba8f4466851b03d29c016d4 Mon Sep 17 00:00:00 2001 From: tslil 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 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/checker_set.rs') 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(), -- cgit v1.3.1