prepare for more work on signatures, in particular this means processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type

1 files changed, 8 insertions, 2 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 4fa723f..4d5f02c 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -12,14 +12,20 @@ impl CheckerState {
                 let deref = self.lookup_signature(&v)?;
                 Ok(deref.clone())
             }
-            Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented(
+            Signature::Ext { .. } => Err(CheckerError::Unimplemented(
                 "extension signatures".to_string(),
             )),
             Signature::Theory(fields) => {
+                let mut ctx = self.clone();
                 let fields = fields
                     .into_iter()
                     .map(|SigField { signature, name }| {
-                        let signature = self.check_signature(signature)?;
+                        let signature = ctx.check_signature(signature)?;
+                        ctx.add_instance(
+                            name.clone(),
+                            InstanceValue::Hypothetical(signature.clone()),
+                            signature.clone(),
+                        )?;
                         Ok(SigField { name, signature })
                     })
                     .collect::<Result<Vec<_>, _>>()?;