fixing ...

3 files changed, 32 insertions, 5 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 1a89631..83d97a1 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -103,13 +103,15 @@ impl CheckerState {
             }
             Element::Var(v) => {
                 let lookup = self.lookup_element(&v)?;
+                let container = self.check_set(&lookup.container)?; // TODO: necessary why?
+
                 // 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) {
+                if !self.equal(set, &container) {
                     return Err(CheckerError::WrongSetForElement {
                         value: element.clone().into(),
                         claimed: set.clone(),
-                        real: lookup.container.clone(),
+                        real: container,
                     });
                 }
                 // If we found a formal binding, we have no value to report.
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index ab54fd1..9d0bffe 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -107,7 +107,7 @@ impl CheckerState {
         }
     }
 
-    #[instrument(skip(self), level = "debug", fields(%instance, ?signature))]
+    #[instrument(skip(self), level = "debug", fields(%instance, signature=%signature.map(|s| s.to_string()).unwrap_or_default()) )]
     pub fn check_instance(
         &self,
         instance: &Instance,
@@ -140,10 +140,24 @@ impl CheckerState {
                             claimed: signature.clone(),
                         });
                     };
+                    println!("{self}");
                     let element = self.check_element(element, set)?;
                     Ok(Instance::ElementCoerce(element))
                 } else {
                     // todo!("how do we handle check_element without a set?");
+                    println!("THISISATTODO");
+                    // quick hack:
+                    let element = if let Element::Var(v) = element {
+                        let lookup = self.lookup_element(&v)?;
+                        if let ElementValue::Concrete(ref x) = lookup.value {
+                            x.clone()
+                        } else {
+                            element.clone()
+                        }
+                    } else {
+                        element.clone()
+                    };
+
                     Ok(Instance::ElementCoerce(element.clone()))
                 }
             }
@@ -491,6 +505,7 @@ impl CheckerState {
                             claimed: signature.clone(),
                         });
                     }
+
                     let mut ctx = self.clone();
                     let inst_params = zip(inst_params, sig_params)
                         .map(
@@ -519,6 +534,12 @@ impl CheckerState {
                                     Element::Var(set_n.clone()).into(),
                                     set_s.clone(),
                                 )?;
+                                // TODO should this be unconditional?
+                                ctx.add_element(
+                                    set_n.clone(),
+                                    ElementValue::Hypothetical,
+                                    set_s.clone()
+                                )?;
                                 Ok(Param {
                                     name: set_n.clone(),
                                     set: set_s,
diff --git a/src/checker_state.rs b/src/checker_state.rs
index a88c6b0..77abbdd 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -464,8 +464,12 @@ fn _reserved_name(n: usize, alter: bool) -> String {
 
 impl CheckerState {
     fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
-        let n = self.binder_element.fetch_add(1, Ordering::Relaxed);
-        let canonical = _reserved_name(n, false);
+        let canonical = if name.starts_with("#") {
+            name.clone()
+        } else {
+            let n = self.binder_element.fetch_add(1, Ordering::Relaxed);
+            _reserved_name(n, false)
+        };
         self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
         Ok(canonical)
     }