rework checking logic to revolve around "stuck" computations, the meaning of Hypothetical is now reserved for formal bindings

2 files changed, 93 insertions, 109 deletions

diff --git a/src/checker.rs b/src/checker.rs
index 05ebca2..976b9fb 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -1,5 +1,5 @@
 use crate::ast::*;
-use crate::checker_state::{CheckerError, CheckerState, ElementValue};
+use crate::checker_state::{CheckerError, CheckerState};
 
 use tracing::{debug, instrument};
 
@@ -26,12 +26,7 @@ impl CheckerState {
                 Decl::Element { name, element, set } => {
                     let set = self.check_set(set.clone())?;
                     let element = self.check_element(element.clone().into(), &set)?;
-                    if matches!(element, ElementValue::Hypothetical(_)) {
-                        panic!(
-                            "invariant violation: from concrete values at the top level we returned a hypothetical value"
-                        );
-                    }
-                    self.add_element(name.clone(), element, set)
+                    self.add_element(name.clone(), element.into(), set)
                 }
                 Decl::Signature { name, signature } => {
                     let signature = self.check_signature(signature.clone())?;
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 7ff6e4a..729ce08 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -48,13 +48,13 @@ impl CheckerState {
 
     fn _check_literal_set_helper(
         &self,
-        value: ElementValue,
+        value: Element,
         claimed: &Set,
         should_be: Set,
     ) -> Result<(), CheckerError> {
         if !self.equal(claimed, &should_be) {
             Err(CheckerError::WrongSetForElement {
-                value: value.clone(),
+                value: value.clone().into(),
                 claimed: claimed.clone(),
                 real: should_be,
             })
@@ -63,30 +63,11 @@ impl CheckerState {
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%value, %set))]
-    pub fn check_element(
-        &self,
-        value: ElementValue,
-        set: &Set,
-    ) -> Result<ElementValue, CheckerError> {
-        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 (*)
-            Value::Hypothetical(ref h_set) => {
-                if !self.equal(set, &h_set) {
-                    Err(CheckerError::WrongSetForElement {
-                        value: value.clone(),
-                        claimed: set.clone(),
-                        real: h_set.clone(),
-                    })
-                } else {
-                    Ok(value)
-                }
-            }
-            Value::Concrete(ref element @ Element::Literal(ref lit)) => {
-                let value = value.clone();
+    #[instrument(skip(self), level = "debug", fields(%element, %set))]
+    pub fn check_element(&self, element: Element, set: &Set) -> Result<Element, CheckerError> {
+        match element {
+            Element::Literal(ref lit) => {
+                let value = element.clone();
                 // we may infer the type from the element
                 match lit {
                     Literal::Int(_) => {
@@ -107,22 +88,30 @@ impl CheckerState {
                 }
                 Ok(element.clone().into())
             }
-            Value::Concrete(Element::Var(ref v)) => {
+            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.equal(set, &lookup.container) {
                     return Err(CheckerError::WrongSetForElement {
-                        value: value.clone(),
+                        value: element.clone().into(),
                         claimed: set.clone(),
                         real: lookup.container.clone(),
                     });
                 }
-                Ok(lookup.value.clone())
+                // If we found a formal binding, we have no value to report.
+                // This is the ONLY source of Var as a return value for
+                // check_element, so in other branches we condition our logic
+                // for formal bindings on finding Var after recursing.
+                if let ElementValue::Concrete(ref deref) = lookup.value {
+                    Ok(deref.clone())
+                } else {
+                    Ok(Element::Var(v.clone()))
+                }
             }
-            Value::Concrete(ref concrete @ Element::Record(ref assignations)) => {
+            Element::Record(ref assignations) => {
                 let rej = |reason| CheckerError::ElementDoesNotBelong {
-                    element: concrete.clone(),
+                    element: element.clone(),
                     claimed: set.clone(),
                     reason,
                 };
@@ -162,24 +151,17 @@ impl CheckerState {
                 let sub_els = zip(element_felements, set_fsets)
                     .map(|(e_f, e_s)| self.check_element(e_f.clone().into(), &e_s))
                     .collect::<Result<Vec<_>, _>>()?;
-                // rebuild, hypotheticals are contagious
+                // rebuild
                 let assignations = zip(element_fnames, sub_els)
-                    .map(|(name, element)| match element {
-                        Value::Concrete(element) => Some(ElemAssign { name, element }),
-                        Value::Hypothetical(_) => None,
-                    })
+                    .map(|(name, element)| ElemAssign { name, element })
                     .collect();
                 // resign?
-                Ok(if let Some(assignations) = assignations {
-                    Element::Record(assignations).into()
-                } else {
-                    Value::Hypothetical(set.clone())
-                })
+                Ok(Element::Record(assignations))
             }
-            Value::Concrete(Element::Project {
+            Element::Project {
                 element: ref inner,
                 ref field,
-            }) => {
+            } => {
                 // globally unique projections mean we know what the sets going
                 // in and out must be
                 let Field {
@@ -190,41 +172,45 @@ impl CheckerState {
                 // enforce the correct typing of the claimed result
                 if !self.equal(set, field_set) {
                     return Err(CheckerError::WrongSetForElement {
-                        value,
+                        value: element.clone().into(),
                         claimed: set.clone(),
                         real: field_set.clone(),
                     });
                 }
 
                 // enforce the correct typing of the element
-                let inner = self.check_element((*inner.clone()).into(), owner_set)?;
+                let inner = self.check_element(*inner.clone(), owner_set)?;
+
+                // Unfortunately we still have to do something nasty here to
+                // obtain the data
                 match inner {
-                    Value::Concrete(inner) => {
-                        // 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"
-                            );
-                        };
+                    // We're stuck on something that bottoms out in a binding
+                    // blocking computation, nothing to be done here
+                    Element::Var(_) | Element::Project { .. } | Element::Case { .. } => {
+                        Ok(Element::Project {
+                            element: Box::new(inner),
+                            field: field.clone(),
+                        })
+                    }
+                    Element::Record(assignations) => {
                         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.into())
+                            .element;
+                        Ok(sub_element)
                     }
-                    // correct by (*)
-                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
+                    _ => panic!(
+                        "invariant violation: check_element returned neither a record or stuck computation for record set"
+                    ),
                 }
             }
-            Value::Concrete(Element::Inject {
+            Element::Inject {
                 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
                 // roles are here interchanged
@@ -236,31 +222,24 @@ impl CheckerState {
                 // enforce the correct typing of the claimed result
                 if !self.equal(set, owner_set) {
                     return Err(CheckerError::WrongSetForElement {
-                        value,
+                        value: element.clone().into(),
                         claimed: set.clone(),
                         real: owner_set.clone(),
                     });
                 }
 
                 // enforce the correct typing of the element
-                let element = self.check_element((*inner.clone()).into(), field_set)?;
-
-                match element {
-                    Value::Concrete(element) => Ok(Element::Inject {
-                        element: Box::new(element),
-                        field: field.clone(),
-                    }
-                    .into()),
-                    // correct by (*)
-                    Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
-                }
+                let element = self.check_element(*inner.clone(), field_set)?;
+                Ok(Element::Inject {
+                    element: Box::new(element),
+                    field: field.clone(),
+                })
             }
-            Value::Concrete(
-                ref element @ Element::Case {
-                    ref arms,
-                    ref scrutinee,
-                },
-            ) => {
+
+            Element::Case {
+                ref arms,
+                ref scrutinee,
+            } => {
                 // TODO: do we allow mapping out of bottom?
                 if arms.is_empty() {
                     return Err(CheckerError::Unimplemented(
@@ -276,7 +255,7 @@ impl CheckerState {
                     .map(|ca| self.lookup_variant_field(&ca.tag).map(|sf| &sf.owner))
                     .collect::<Result<Vec<_>, _>>()?;
                 let owner = arm_owners[0]; // safe because of the above decision about bottom
-                if !arm_owners.iter().all(|o| self.equal(owner, o)) {
+                if !arm_owners.into_iter().all(|o| self.equal(owner, o)) {
                     return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone()));
                 }
 
@@ -305,62 +284,72 @@ impl CheckerState {
                 // scrutinee must be of the same set that all the arms are
                 // implying, in particular this implies that the following holds
                 // `inner : self.lookup_variant_field(field).field_set`
-                let scrutinee = self.check_element((*scrutinee.clone()).into(), owner)?;
+                let scrutinee = self.check_element(*scrutinee.clone(), owner)?;
 
                 // which variant are we, if any
+
                 let matching: Option<(String, Element)> = match scrutinee {
-                    Value::Hypothetical(_) => None,
-                    Value::Concrete(Element::Inject {
-                        field,
-                        element: inner,
-                    }) => Some((field, *inner)),
-                    _ => {
-                        panic!(
-                            "invariant violation: we believe element is of a variant set but it's not an injection"
-                        );
-                    }
+                    Element::Inject {
+                        ref field,
+                        element: ref inner,
+                    } => Some((field.clone(), *inner.clone())),
+                    // These are all the cases which could become stuck on a
+                    // formal binding
+                    Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None,
+                    Element::Literal(_) | Element::Record(_) => panic!(
+                        "invariant violation: scrutinee is a non-variant value at variant set"
+                    ),
                 };
 
                 // for each arm, recurse with a concrete value (if we have one)
                 // otherwise fall back to hypothetical elements; in the former
                 // case record the end result
                 let mut computed_output = None;
+                let mut processed_arms = Vec::new();
                 for arm in arms {
                     let Field {
                         field: field_set, ..
                     } = self.lookup_variant_field(&arm.tag)?;
 
-                    // TODO: if we were worried about overhead we'd have a separate
-                    // locals stack, though truly if we were worried about overhead
-                    // we'd not have NNN instances of clone elsewhere in the
-                    // codebase and we wouldn't be eagerly evaluating all
-                    // expressions fully.
-
                     let mut new_context = self.clone();
                     let binding_name = arm.bound.clone();
                     let binding_set = field_set.clone();
 
-                    if let Some((tag, inner)) = &matching
+                    let body = if let Some((tag, inner)) = &matching
                         && *tag == arm.tag
                     {
-                        new_context.add_element(binding_name, inner.clone().into(), binding_set)?;
+                        new_context.add_element(
+                            binding_name.clone(),
+                            inner.clone().into(),
+                            binding_set,
+                        )?;
                         let output = new_context.check_element(arm.body.clone().into(), set)?;
                         if matches!(computed_output, Some(_)) {
                             panic!(
                                 "invariant violation: we somehow matched multiple arms in case analysis"
                             )
                         }
-                        computed_output = Some(output);
+                        computed_output = Some(output.clone());
+                        output
                     } else {
                         new_context.add_element(
-                            binding_name,
+                            binding_name.clone(),
                             Value::Hypothetical(field_set.clone()),
                             binding_set,
                         )?;
-                        new_context.check_element(arm.body.clone().into(), set)?;
+                        new_context.check_element(arm.body.clone().into(), set)?
                     };
+
+                    processed_arms.push(CaseArm {
+                        tag: arm.tag.clone(),
+                        bound: binding_name,
+                        body,
+                    });
                 }
-                Ok(computed_output.unwrap_or(Value::Hypothetical(set.clone())))
+                Ok(computed_output.unwrap_or(Element::Case {
+                    scrutinee: Box::new(scrutinee),
+                    arms: processed_arms,
+                }))
             }
         }
     }