replace todo! with real errors

1 files changed, 39 insertions, 13 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 30598d3..beb0af6 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -232,7 +232,9 @@ impl CheckerState {
                 let owner = arm_owners[0];
 
                 if !arm_owners.into_iter().all(|o| self.equal(owner, o)) {
-                    todo!("inconsistent case scrutinee set");
+                    return Err(CheckerError::InstanceInconsistentCaseScrutineeSet(
+                        instance.clone(),
+                    ));
                 }
 
                 let Set::Variant(fields) = owner else {
@@ -316,20 +318,39 @@ impl CheckerState {
             } => {
                 if let Some(signature) = signature {
                     if inst_params.is_empty() {
-                        todo!("should be impossible");
+                        return Err(CheckerError::Unimplemented(
+                            "instance for with empty params".to_string(),
+                        ));
                     };
                     let Signature::Ext {
                         params: sig_params,
                         codomain,
                     } = signature
                     else {
-                        todo!("need to raise error");
+                        return Err(CheckerError::WrongSignatureForInstance {
+                            real: Signature::Ext {
+                                params: vec![Param {
+                                    name: "_".to_string(),
+                                    set: Set::Var("_".to_string()),
+                                }],
+                                codomain: Box::new(Signature::Var("_".to_string())),
+                            },
+                            value: instance.clone().into(),
+                            claimed: signature.clone(),
+                        });
                     };
                     if sig_params.is_empty() {
-                        todo!("should be impossible")
+                        return Err(CheckerError::Unimplemented(
+                            "extension signature with empty params".to_string(),
+                        ));
                     }
                     if sig_params.len() != inst_params.len() {
-                        todo!("this is a type error")
+                        return Err(CheckerError::InstanceDoesNotBelong {
+                            instance: instance.clone(),
+                            reason: "instance and signature have differing number of parameters"
+                                .to_string(),
+                            claimed: signature.clone(),
+                        });
                     }
                     let mut ctx = self.clone();
                     let inst_params = zip(inst_params, sig_params)
@@ -347,7 +368,12 @@ impl CheckerState {
                                 let inst_s = ctx.check_set(inst_s)?;
                                 let set_s = ctx.check_set(set_s)?;
                                 if !ctx.equal(&inst_s, &set_s) {
-                                    todo!("type error")
+                                    return Err(CheckerError::InstanceDoesNotBelong{
+                                        instance: instance.clone(),
+                                        claimed: signature.clone(),
+                                        reason: format!("the signature specifies set {} but in this position the instance has set {}",
+                                            set_s, inst_s),
+                                    });
                                 }
                                 ctx.add_element(
                                     inst_n.clone(),
@@ -431,7 +457,7 @@ impl CheckerState {
                             elements: args,
                         });
                     };
-                    let (ctx, checked_args) = self._bind_args(&params, &args)?;
+                    let (ctx, checked_args) = self._bind_args(instance, &params, &args)?;
 
                     if let Some(expected) = signature {
                         let result_sig = if args.len() == params.len() {
@@ -470,7 +496,7 @@ impl CheckerState {
 
                 match subject {
                     Instance::For { params, body } => {
-                        let (ctx, _checked) = self._bind_args(&params, &args)?;
+                        let (ctx, _checked) = self._bind_args(instance, &params, &args)?;
                         if args.len() == params.len() {
                             ctx.check_instance(&body, signature)
                         } else {
@@ -503,15 +529,15 @@ impl CheckerState {
 
     fn _bind_args(
         &self,
+        instance: &Instance,
         params: &[Param],
         args: &[Element],
     ) -> Result<(CheckerState, Vec<Element>), CheckerError> {
         if args.len() > params.len() {
-            todo!(
-                "over-application: {} args to a function of arity {}",
-                args.len(),
-                params.len()
-            );
+            return Err(CheckerError::OverApplication {
+                instance: instance.clone(),
+                applied_to: args.len(),
+            });
         }
         let mut ctx = self.clone();
         let checked = zip(params.iter(), args.iter())