1 files changed, 88 insertions, 28 deletions

diff --git a/src/checker.rs b/src/checker.rs
index d45a5a4..2c6c5d0 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -32,10 +32,10 @@ pub enum CheckError {
 }
 
 #[derive(Display)]
-#[display("{value} @ {belongs_to}")]
+#[display("{field_set} @ {owner_set}")]
 struct SetField {
-    value: Set,
-    belongs_to: Set,
+    field_set: Set,
+    owner_set: Set,
 }
 
 #[derive(Display)]
@@ -109,52 +109,48 @@ impl CheckState {
         set_ref: &SetField,
         belongs_to: &Set,
     ) -> Result<(), CheckError> {
-        let SetField {
-            value: _,
-            belongs_to: owner,
-        } = set_ref;
-        if !self.set_equal(owner, belongs_to) {
+        if !self.set_equal(&set_ref.owner_set, belongs_to) {
             Err(CheckError::Rebinding(name.clone()))
         } else {
             Ok(())
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))]
+    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
     fn add_record_field(
         &mut self,
         name: &String,
-        set: &Set,
-        belongs_to: &Set,
+        field_set: &Set,
+        owner_set: &Set,
     ) -> Result<(), CheckError> {
         if let Some(set_ref) = self.record_fields.get(name) {
-            self.assert_correct_owner(name, set_ref, belongs_to)?;
+            self.assert_correct_owner(name, set_ref, owner_set)?;
         };
         self.record_fields.insert(
             name.clone(),
             SetField {
-                value: set.clone(),
-                belongs_to: belongs_to.clone(),
+                field_set: field_set.clone(),
+                owner_set: owner_set.clone(),
             },
         );
         Ok(())
     }
 
-    #[instrument(skip(self), level = "debug", fields(%name, %set, %belongs_to))]
+    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
     fn add_variant_field(
         &mut self,
         name: &String,
-        set: &Set,
-        belongs_to: &Set,
+        field_set: &Set,
+        owner_set: &Set,
     ) -> Result<(), CheckError> {
         if let Some(set_ref) = self.variant_fields.get(name) {
-            self.assert_correct_owner(name, set_ref, belongs_to)?;
+            self.assert_correct_owner(name, set_ref, owner_set)?;
         };
         self.variant_fields.insert(
             name.clone(),
             SetField {
-                value: set.clone(),
-                belongs_to: belongs_to.clone(),
+                field_set: field_set.clone(),
+                owner_set: owner_set.clone(),
             },
         );
         Ok(())
@@ -167,19 +163,19 @@ impl CheckState {
             Set::Record(fields) => {
                 for RecordField {
                     name: rfn,
-                    set: rset,
+                    set: field_set,
                 } in fields
                 {
-                    self.add_record_field(rfn, rset, &set)?;
+                    self.add_record_field(rfn, field_set, &set)?;
                 }
             }
             Set::Variant(fields) => {
                 for VariantField {
                     name: vfn,
-                    set: vset,
+                    set: field_set,
                 } in fields
                 {
-                    self.add_variant_field(vfn, vset, &set)?;
+                    self.add_variant_field(vfn, field_set, &set)?;
                 }
             }
             _ => (),
@@ -377,11 +373,75 @@ impl CheckState {
                 // resign?
                 Ok(Element::Record(assignations))
             }
-            Element::Project { .. } => {
-                Err(CheckError::Unimplemented("element project".to_string()))
+            Element::Project {
+                element: inner,
+                field,
+            } => {
+                // globally unique projections mean we know what the sets going
+                // in and out must be
+                let Some(SetField {
+                    field_set,
+                    owner_set,
+                }) = self.record_fields.get(field)
+                else {
+                    return Err(CheckError::Unbound(field.clone()));
+                };
+
+                // enforce the correct typing of the claimed result
+                if !self.set_equal(set, field_set) {
+                    return Err(CheckError::WrongSetForElement(
+                        set.clone(),
+                        field_set.clone(),
+                    ));
+                }
+
+                // enforce the correct typing of the element
+                let inner = self.check_element(inner, owner_set)?;
+
+                // Unfortunately we still have to do something nasty here to obtain the data
+                let Element::Record(assignations) = inner else {
+                    panic!("invariant violation: check_element returned non-record for record set");
+                };
+                let sub_element = assignations
+                    .into_iter()
+                    .find(|a| a.name == *field)
+                    .expect("invariant violation: record missing field that was type-checked")
+                    .element
+                    .clone();
+
+                Ok(sub_element)
+            }
+            Element::Inject {
+                element: inner,
+                field,
+            } => {
+                // globally unique injections mean that we know what the sets
+                // going in and out must be, but compared to projections their
+                // roles are here interchanged
+                let Some(SetField {
+                    field_set,
+                    owner_set,
+                }) = self.variant_fields.get(field)
+                else {
+                    return Err(CheckError::Unbound(field.clone()));
+                };
+
+                // enforce the correct typing of the claimed result
+                if !self.set_equal(set, owner_set) {
+                    return Err(CheckError::WrongSetForElement(
+                        set.clone(),
+                        owner_set.clone(),
+                    ));
+                }
+
+                // enforce the correct typing of the element
+                let element = self.check_element(inner, field_set)?;
+
+                Ok(Element::Inject {
+                    element: Box::new(element),
+                    field: field.clone(),
+                })
             }
-            Element::Inject { .. } => Err(CheckError::Unimplemented("element inject".to_string())),
-            Element::App(_, _) => Err(CheckError::Unimplemented("element app".to_string())),
             Element::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())),
         }
     }