switch to references in many places for check_*, complete logic of Var case for App

3 files changed, 62 insertions, 48 deletions

diff --git a/src/checker.rs b/src/checker.rs
index f3c5205..adb5012 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -20,19 +20,19 @@ impl CheckerState {
             match decl {
                 Decl::Set { name, set } => {
                     self.assert_unbound_set(name)?;
-                    let set = self.check_set(set.clone())?;
+                    let set = self.check_set(set)?;
                     self.add_set(name.clone(), set.into())
                 }
 
                 Decl::Element { name, element, set } => {
                     self.assert_unbound_element(name)?;
-                    let set = self.check_set(set.clone())?;
-                    let element = self.check_element(element.clone().into(), &set)?;
+                    let set = self.check_set(set)?;
+                    let element = self.check_element(element.into(), &set)?;
                     self.add_element(name.clone(), element.into(), set)
                 }
                 Decl::Signature { name, signature } => {
                     self.assert_unbound_signature(name)?;
-                    let signature = self.check_signature(signature.clone())?;
+                    let signature = self.check_signature(signature)?;
                     self.add_signature(name, signature, false)
                 }
                 Decl::Instance {
@@ -41,8 +41,8 @@ impl CheckerState {
                     signature,
                 } => {
                     self.assert_unbound_instance(name)?;
-                    let signature = self.check_signature(signature.clone())?;
-                    let instance = self.check_instance(instance.clone(), (&signature).into())?;
+                    let signature = self.check_signature(signature)?;
+                    let instance = self.check_instance(instance, (&signature).into())?;
                     self.add_instance(name.clone(), instance.into(), signature)
                 }
             }?;
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2bd011d..10f9b28 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -6,7 +6,7 @@ use tracing::instrument;
 
 impl CheckerState {
     #[instrument(skip(self), level = "debug", fields(%set))]
-    pub fn check_set(&self, set: Set) -> Result<Set, CheckerError> {
+    pub fn check_set(&self, set: &Set) -> Result<Set, CheckerError> {
         match set {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
@@ -16,7 +16,10 @@ impl CheckerState {
                     .map(|RecordField { name, set }| {
                         let set = ctx.check_set(set)?;
                         ctx.make_element_binding(name.clone(), set.clone())?;
-                        Ok(RecordField { name, set })
+                        Ok(RecordField {
+                            name: name.clone(),
+                            set,
+                        })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
                 Ok(Set::Record(fields))
@@ -41,7 +44,7 @@ impl CheckerState {
             Set::Var(v) => {
                 let deref = self.lookup_set(&v)?;
                 match deref {
-                    SetValue::Hypothetical => Ok(Set::Var(v)),
+                    SetValue::Hypothetical => Ok(Set::Var(v.clone())),
                     SetValue::Concrete(deref) => Ok(deref.clone()),
                 }
             }
@@ -66,9 +69,9 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%element, %set))]
-    pub fn check_element(&self, element: Element, set: &Set) -> Result<Element, CheckerError> {
+    pub fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckerError> {
         match element {
-            Element::Literal(ref lit) => {
+            Element::Literal(lit) => {
                 let value = element.clone();
                 // we may infer the type from the element
                 match lit {
@@ -90,7 +93,7 @@ impl CheckerState {
                 }
                 Ok(element.clone().into())
             }
-            Element::Var(ref v) => {
+            Element::Var(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!
@@ -111,7 +114,7 @@ impl CheckerState {
                     Ok(Element::Var(v.clone()))
                 }
             }
-            Element::Record(ref assignations) => {
+            Element::Record(assignations) => {
                 let rej = |reason| CheckerError::ElementDoesNotBelong {
                     element: element.clone(),
                     claimed: set.clone(),
@@ -151,7 +154,7 @@ impl CheckerState {
 
                 // recurse, sets have already been completely expanded
                 let sub_els = zip(element_felements, set_fsets)
-                    .map(|(e_f, e_s)| self.check_element(e_f.clone().into(), &e_s))
+                    .map(|(e_f, e_s)| self.check_element(e_f.into(), &e_s))
                     .collect::<Result<Vec<_>, _>>()?;
                 // rebuild
                 let assignations = zip(element_fnames, sub_els)
@@ -161,8 +164,8 @@ impl CheckerState {
                 Ok(Element::Record(assignations))
             }
             Element::Project {
-                element: ref inner,
-                ref field,
+                element: inner,
+                field,
             } => {
                 // globally unique projections mean we know what the sets going
                 // in and out must be
@@ -181,7 +184,7 @@ impl CheckerState {
                 }
 
                 // enforce the correct typing of the element
-                let inner = self.check_element(*inner.clone(), owner_set)?;
+                let inner = self.check_element(inner, owner_set)?;
 
                 // Unfortunately we still have to do something nasty here to
                 // obtain the data
@@ -210,8 +213,8 @@ impl CheckerState {
                 }
             }
             Element::Inject {
-                element: ref inner,
-                ref field,
+                element: inner,
+                field,
             } => {
                 // globally unique injections mean that we know what the sets
                 // going in and out must be, but compared to projections their
@@ -231,17 +234,14 @@ impl CheckerState {
                 }
 
                 // enforce the correct typing of the element
-                let element = self.check_element(*inner.clone(), field_set)?;
+                let element = self.check_element(inner, field_set)?;
                 Ok(Element::Inject {
                     element: Box::new(element),
                     field: field.clone(),
                 })
             }
 
-            Element::Case {
-                ref arms,
-                ref scrutinee,
-            } => {
+            Element::Case { arms, scrutinee } => {
                 // TODO: do we allow mapping out of bottom?
                 if arms.is_empty() {
                     return Err(CheckerError::Unimplemented(
@@ -286,7 +286,7 @@ 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(), owner)?;
+                let scrutinee = self.check_element(scrutinee, owner)?;
 
                 // which variant are we, if any
 
@@ -322,7 +322,7 @@ impl CheckerState {
                     {
                         let canonical =
                             ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
-                        let output = ctx.check_element(arm.body.clone().into(), set)?;
+                        let output = ctx.check_element((&arm.body).into(), set)?;
                         if matches!(computed_output, Some(_)) {
                             panic!(
                                 "invariant violation: we somehow matched multiple arms in case analysis"
@@ -336,7 +336,7 @@ impl CheckerState {
                         }
                     } else {
                         let canonical = ctx.make_element_binding(binding_name, binding_set)?;
-                        let body = ctx.check_element(arm.body.clone().into(), set)?;
+                        let body = ctx.check_element((&arm.body).into(), set)?;
                         CaseArm {
                             tag: arm.tag.clone(),
                             bound: canonical,
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index b979f54..8e99d3c 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -6,7 +6,7 @@ use tracing::instrument;
 
 impl CheckerState {
     #[instrument(skip(self), level = "debug", fields(%signature))]
-    pub fn check_signature(&self, signature: Signature) -> Result<Signature, CheckerError> {
+    pub fn check_signature(&self, signature: &Signature) -> Result<Signature, CheckerError> {
         match signature {
             Signature::Set => Ok(Signature::Set),
             Signature::Var(v) => {
@@ -16,14 +16,14 @@ impl CheckerState {
             Signature::Ext { params, codomain } => {
                 let mut ctx = self.clone();
                 let params = params
-                    .into_iter()
+                    .iter()
                     .map(|p| {
-                        let set = ctx.check_set(p.set.clone())?;
+                        let set = ctx.check_set(&p.set)?;
                         let canon = ctx.make_element_binding(p.name.clone(), set.clone())?;
                         Ok(Param { set, name: canon })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
-                let codomain = Box::new(ctx.check_signature(*codomain)?);
+                let codomain = Box::new(ctx.check_signature(codomain)?);
                 Ok(Signature::Ext { params, codomain })
             }
             Signature::Theory(fields) => {
@@ -40,7 +40,10 @@ impl CheckerState {
                             Set::ClaimedSet(Instance::Var(name.clone())).into(),
                         )?;
                     }
-                    new_fields.push(SigField { name, signature });
+                    new_fields.push(SigField {
+                        name: name.clone(),
+                        signature,
+                    });
                     // We must iteratively add the entire signature so that
                     // field lookup does something, as we rely on that for type
                     // checking. We could hack together a signature i suppose,
@@ -57,11 +60,11 @@ impl CheckerState {
     #[instrument(skip(self), level = "debug", fields(%instance, ?signature))]
     pub fn check_instance(
         &self,
-        instance: Instance,
+        instance: &Instance,
         signature: Option<&Signature>,
     ) -> Result<Instance, CheckerError> {
         match instance {
-            Instance::SetCoerce(ref set) => {
+            Instance::SetCoerce(set) => {
                 if let Some(signature) = signature
                     && *signature != Signature::Set
                 {
@@ -71,14 +74,14 @@ impl CheckerState {
                         claimed: signature.clone(),
                     });
                 };
-                let set = Box::new(self.check_set(*set.clone())?);
+                let set = Box::new(self.check_set(set)?);
                 if let Set::ClaimedSet(inner) = *set {
                     Ok(inner)
                 } else {
                     Ok(Instance::SetCoerce(set))
                 }
             }
-            Instance::Var(ref v) => {
+            Instance::Var(v) => {
                 // Exactly the same discipline as for Element::Var, see there
                 // for some sparse comments
                 let lookup = self.lookup_instance(&v)?;
@@ -97,7 +100,7 @@ impl CheckerState {
                     Ok(Instance::Var(v.clone()))
                 }
             }
-            Instance::Record(ref assignations) => {
+            Instance::Record(assignations) => {
                 // once again, mutatis mutandis from elements
                 let (instance_fnames, instance_finstances): (Vec<String>, Vec<&Instance>) =
                     assignations
@@ -146,17 +149,14 @@ impl CheckerState {
                 }
 
                 let sub_els = zip(instance_finstances, signature_fsigs)
-                    .map(|(e_f, e_s)| self.check_instance(e_f.clone(), (&e_s).into()))
+                    .map(|(e_f, e_s)| self.check_instance(e_f, (&e_s).into()))
                     .collect::<Result<Vec<_>, _>>()?;
                 let assignations = zip(instance_fnames, sub_els)
                     .map(|(name, instance)| InstAssign { name, instance })
                     .collect();
                 Ok(Instance::Record(assignations))
             }
-            Instance::Project {
-                ref instance,
-                ref field,
-            } => {
+            Instance::Project { instance, field } => {
                 let Field {
                     field: field_signature,
                     owner: owner_signature,
@@ -172,7 +172,7 @@ impl CheckerState {
                     });
                 }
 
-                let inner = self.check_instance(*instance.clone(), owner_signature.into())?;
+                let inner = self.check_instance(instance, owner_signature.into())?;
 
                 match inner {
                     Instance::Var(_) | Instance::Project { .. } => Ok(Instance::Project {
@@ -198,7 +198,7 @@ impl CheckerState {
                 todo!("instance for")
             }
             Instance::App(inner, element) => {
-                let inner = self.check_instance(*inner, None)?;
+                let inner = self.check_instance(inner, None)?;
                 match &inner {
                     Instance::Var(v) => {
                         let field = self.lookup_signature_field(&v)?;
@@ -219,9 +219,23 @@ impl CheckerState {
                                 real: field.owner.clone(),
                             });
                         };
-                        // TODO: we need to assert (somewhere else) that ext has >=1 params
-                        // TODO: in the special case that params.len() == 1 we need to do something with codomain
-                        let element = self.check_element(*element, &params[0].set)?;
+                        if params.is_empty() {
+                            panic!(
+                                "It should have been impossible to construct an Ext with no params, but here we are"
+                            );
+                        }
+                        if params.len() == 1
+                            && let Some(signature) = signature
+                        {
+                            if !self.equal(&**codomain, signature) {
+                                return Err(CheckerError::WrongSignatureForInstance {
+                                    value: instance.clone().into(),
+                                    claimed: signature.clone(),
+                                    real: *codomain.clone(),
+                                });
+                            }
+                        }
+                        let element = self.check_element(element, &params[0].set)?;
                         Ok(Instance::App(
                             Box::new(Instance::Var(v.clone())),
                             Box::new(element),
@@ -233,7 +247,7 @@ impl CheckerState {
                     Instance::Record(_) | Instance::SetCoerce(_) => {
                         Err(CheckerError::NonFunctionalInstance {
                             instance: inner,
-                            element: *element,
+                            element: *element.clone(),
                         })
                     }
                     Instance::Project { .. } | Instance::App(_, _) => panic!(