From 617f3931de77bd795a97331e7146eb10266af7e9 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Thu, 30 Apr 2026 10:52:07 +0100
Subject: lost track of what's going on

---
 src/checker_set.rs | 68 +++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 44 insertions(+), 24 deletions(-)

(limited to 'src/checker_set.rs')

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 10f9b28..c3d1b3a 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -1,6 +1,7 @@
 use crate::ast::*;
 use crate::checker_state::*;
 
+use std::collections::HashMap;
 use std::iter::zip;
 use tracing::instrument;
 
@@ -39,7 +40,11 @@ impl CheckerState {
             }
             Set::ClaimedSet(instance) => {
                 let instance = self.check_instance(instance, Some(&Signature::Set))?;
-                Ok(Set::ClaimedSet(instance))
+                if let Instance::SetCoerce(set) = instance {
+                    Ok(*set)
+                } else {
+                    Ok(Set::ClaimedSet(instance))
+                }
             }
             Set::Var(v) => {
                 let deref = self.lookup_set(&v)?;
@@ -128,40 +133,55 @@ impl CheckerState {
                     Err(rej("element is a record instance".to_string()))
                 }?;
 
-                let (set_fnames, set_fsets): (Vec<String>, Vec<Set>) = fields
-                    .iter()
-                    .map(|RecordField { name, set }| (name.clone(), set.clone()))
-                    .unzip();
-                let mut set_fnames_sorted = set_fnames.clone();
+                let mut set_fnames_sorted: Vec<String> =
+                    fields.iter().map(|x| x.name.clone()).collect();
                 set_fnames_sorted.sort();
 
-                let (element_fnames, element_felements): (Vec<String>, Vec<&Element>) =
-                    assignations
-                        .iter()
-                        .map(|ElemAssign { name, element }| (name.clone(), element))
-                        .unzip();
-
-                let mut element_fnames_sorted = element_fnames.clone();
+                let mut element_fnames_sorted: Vec<String> =
+                    assignations.iter().map(|x| x.name.clone()).collect();
                 element_fnames_sorted.sort();
 
+                // make sure that we are correctly filling the record
                 if set_fnames_sorted != element_fnames_sorted {
                     return Err(rej(format!(
                         "expected [{}] but found [{}]",
-                        set_fnames.join(", "),
-                        element_fnames.join(", "),
+                        set_fnames_sorted.join(", "),
+                        element_fnames_sorted.join(", "),
                     )));
                 }
 
-                // recurse, sets have already been completely expanded
-                let sub_els = zip(element_felements, set_fsets)
-                    .map(|(e_f, e_s)| self.check_element(e_f.into(), &e_s))
+                let assignations = assignations
+                    .into_iter()
+                    .map(|x| (&x.name, &x.element))
+                    .collect::<HashMap<_, _>>();
+
+                let mut ctx = self.clone();
+                // the basic pattern here is that we use ctx.check_* to perform
+                // substitutions for us, as we steadily march through the users
+                // definitions
+                let sub_elements = fields
+                    .iter()
+                    .map(
+                        |RecordField {
+                             name: f_n,
+                             set: f_s,
+                         }| {
+                            let f_e = assignations
+                                .get(f_n)
+                                .expect("we have already checked that all fields are present");
+
+                            let f_s = ctx.check_set(f_s)?;
+                            let f_e = ctx.check_element(f_e, &f_s)?;
+                            ctx.add_element(f_n.clone(), f_e.clone().into(), f_s)?;
+
+                            Ok(ElemAssign {
+                                name: f_n.clone(),
+                                element: f_e,
+                            })
+                        },
+                    )
                     .collect::<Result<Vec<_>, _>>()?;
-                // rebuild
-                let assignations = zip(element_fnames, sub_els)
-                    .map(|(name, element)| ElemAssign { name, element })
-                    .collect();
-                // resign?
-                Ok(Element::Record(assignations))
+                Ok(Element::Record(sub_elements))
             }
             Element::Project {
                 element: inner,
-- 
cgit v1.3.1