wire in instance checking to the main checker

1 files changed, 1 insertions, 28 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index b710ac3..1a6a0bd 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -41,7 +41,7 @@ pub enum CheckerError {
         claimed: Signature,
         real: Signature,
     },
-    #[display("Instance {instance} does belong to set {claimed}: {reason}")]
+    #[display("Instance {instance} is not of signature {claimed}: {reason}")]
     InstanceDoesNotBelong {
         instance: Instance,
         claimed: Signature,
@@ -111,7 +111,6 @@ pub struct CheckerState {
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
     binder_element: usize,
-    binder_instance: usize,
 }
 
 impl fmt::Display for CheckerState {
@@ -424,30 +423,4 @@ impl CheckerState {
         self.binder_element += 1;
         Ok(())
     }
-
-    #[instrument(skip(self), level = "debug", fields(%name, %signature))]
-    pub fn make_instance_binding(
-        &mut self,
-        name: String,
-        signature: Signature,
-    ) -> Result<(), CheckerError> {
-        let canonical = format!("db_i_{}", self.binder_instance);
-        self.add_instance(
-            canonical.clone(),
-            InstanceValue::Hypothetical,
-            signature.clone(),
-        )?;
-        self.add_instance(
-            name.clone(),
-            Instance::Var(canonical.clone()).into(),
-            signature.clone(),
-        )?;
-        // And lo, the special case, our chosen canonical form
-        if signature == Signature::Set {
-            self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?;
-        }
-
-        self.binder_instance += 1;
-        Ok(())
-    }
 }