report _which_ element does not belong to the correct set, at the bottom of the tree anyway

2 files changed, 37 insertions, 22 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index db47c14..93ba4b3 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -43,9 +43,15 @@ impl CheckerState {
         }
     }
 
-    fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckerError> {
+    fn _check_literal_set_helper(
+        &self,
+        value: ElementValue,
+        claimed: &Set,
+        should_be: Set,
+    ) -> Result<(), CheckerError> {
         if !self.set_equal(claimed, &should_be) {
             Err(CheckerError::WrongSetForElement {
+                value: value.clone(),
                 claimed: claimed.clone(),
                 real: should_be,
             })
@@ -54,54 +60,57 @@ impl CheckerState {
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%element, %set))]
+    #[instrument(skip(self), level = "debug", fields(%value, %set))]
     pub fn check_element(
         &self,
-        element: ElementValue,
+        value: ElementValue,
         set: &Set,
     ) -> Result<ElementValue, CheckerError> {
-        match element {
+        match value {
             // This arm ensures that if we ever in the position of obtaining a
             // hypothetical from a call to check_element, in the context of
             // check_element, we can safely ignore its payload. I'll point this
             // out later as (*)
-            ElementValue::Hypothetical(h_set) => {
+            ElementValue::Hypothetical(ref h_set) => {
                 if !self.set_equal(set, &h_set) {
                     Err(CheckerError::WrongSetForElement {
+                        value: value.clone(),
                         claimed: set.clone(),
-                        real: h_set,
+                        real: h_set.clone(),
                     })
                 } else {
-                    Ok(ElementValue::Hypothetical(h_set))
+                    Ok(value)
                 }
             }
             ElementValue::Concrete(ref element @ Element::Literal(ref lit)) => {
+                let value = value.clone();
                 // we may infer the type from the element
                 match lit {
                     Literal::Int(_) => {
-                        self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Int))?;
+                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Int))?;
                     }
                     Literal::Nat(_) => {
-                        self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Nat))?;
+                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Nat))?;
                     }
                     Literal::Str(_) => {
-                        self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Str))?;
+                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Str))?;
                     }
                     Literal::Bool(_) => {
-                        self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Bool))?;
+                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Bool))?;
                     }
                     Literal::Float(_) => {
-                        self._check_literal_set_helper(set, Set::BuiltIn(BuiltIn::Float))?;
+                        self._check_literal_set_helper(value, set, Set::BuiltIn(BuiltIn::Float))?;
                     }
                 }
                 Ok(element.clone().into())
             }
-            ElementValue::Concrete(Element::Var(v)) => {
+            ElementValue::Concrete(Element::Var(ref v)) => {
                 let lookup = self.lookup_element(&v)?;
                 // we have previously done the work to discover the type of
                 // this element, so what we're claiming now must match!
                 if !self.set_equal(set, &lookup.set) {
                     return Err(CheckerError::WrongSetForElement {
+                        value: value.clone(),
                         claimed: set.clone(),
                         real: lookup.set.clone(),
                     });
@@ -165,8 +174,8 @@ impl CheckerState {
                 })
             }
             ElementValue::Concrete(Element::Project {
-                element: inner,
-                field,
+                element: ref inner,
+                ref field,
             }) => {
                 // globally unique projections mean we know what the sets going
                 // in and out must be
@@ -178,13 +187,14 @@ impl CheckerState {
                 // enforce the correct typing of the claimed result
                 if !self.set_equal(set, field_set) {
                     return Err(CheckerError::WrongSetForElement {
+                        value,
                         claimed: set.clone(),
                         real: field_set.clone(),
                     });
                 }
 
                 // enforce the correct typing of the element
-                let inner = self.check_element((*inner).into(), owner_set)?;
+                let inner = self.check_element((*inner.clone()).into(), owner_set)?;
                 match inner {
                     ElementValue::Concrete(inner) => {
                         // Unfortunately we still have to do something nasty here to obtain the data
@@ -195,7 +205,7 @@ impl CheckerState {
                         };
                         let sub_element = assignations
                             .into_iter()
-                            .find(|a| a.name == field)
+                            .find(|a| a.name == *field)
                             .expect(
                                 "invariant violation: record missing field that was type-checked",
                             )
@@ -209,8 +219,8 @@ impl CheckerState {
                 }
             }
             ElementValue::Concrete(Element::Inject {
-                element: inner,
-                field,
+                element: ref inner,
+                ref field,
             }) => {
                 // globally unique injections mean that we know what the sets
                 // going in and out must be, but compared to projections their
@@ -223,13 +233,14 @@ impl CheckerState {
                 // enforce the correct typing of the claimed result
                 if !self.set_equal(set, owner_set) {
                     return Err(CheckerError::WrongSetForElement {
+                        value,
                         claimed: set.clone(),
                         real: owner_set.clone(),
                     });
                 }
 
                 // enforce the correct typing of the element
-                let element = self.check_element((*inner).into(), field_set)?;
+                let element = self.check_element((*inner.clone()).into(), field_set)?;
 
                 match element {
                     ElementValue::Concrete(element) => Ok(Element::Inject {
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 19a7c51..86f229e 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -13,8 +13,12 @@ pub enum CheckerError {
     Rebinding(String),
     #[display("The following functionality is unimplemented: {_0}")]
     Unimplemented(String),
-    #[display("Element claimed to belong to {claimed} but actually belongs to {real}")]
-    WrongSetForElement { claimed: Set, real: Set },
+    #[display("Element {value} claimed to belong to {claimed} but actually belongs to {real}")]
+    WrongSetForElement {
+        value: ElementValue,
+        claimed: Set,
+        real: Set,
+    },
     #[display("Element {element} does belong to set {claimed}: {reason}")]
     ElementDoesNotBelong {
         element: Element,