replace todo! with real errors

3 files changed, 61 insertions, 15 deletions

diff --git a/src/checker_set.rs b/src/checker_set.rs
index 626f74d..98e10ec 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -276,7 +276,9 @@ impl CheckerState {
                     .collect::<Result<Vec<_>, _>>()?;
                 let owner = arm_owners[0]; // safe because of the above decision about bottom
                 if !arm_owners.into_iter().all(|o| self.equal(owner, o)) {
-                    return Err(CheckerError::IncosistentCaseScrutineeSet(element.clone()));
+                    return Err(CheckerError::ElementInconsistentCaseScrutineeSet(
+                        element.clone(),
+                    ));
                 }
 
                 // all cases are handled
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())
diff --git a/src/checker_state.rs b/src/checker_state.rs
index a8473ff..3404a35 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -12,24 +12,33 @@ use std::sync::atomic::{AtomicUsize, Ordering};
 pub enum CheckerError {
     #[display("Unbound: {_0}")]
     Unbound(String),
+
     #[display("Rebinding: {_0}")]
     Rebinding(String),
+
     #[display("The following functionality is unimplemented: {_0}")]
     Unimplemented(String),
+
     #[display("Element {value} claimed to belong to {claimed} but actually belongs to {real}")]
     WrongSetForElement {
         value: ElementValue,
         claimed: Set,
         real: Set,
     },
+
     #[display("Element {element} does belong to set {claimed}: {reason}")]
     ElementDoesNotBelong {
         element: Element,
         claimed: Set,
         reason: String,
     },
+
+    #[display("Case analysis {_0} does not have consistent set for scrutinee")]
+    ElementInconsistentCaseScrutineeSet(Element),
+
     #[display("Case analysis {_0} does not have consistent set for scrutinee")]
-    IncosistentCaseScrutineeSet(Element),
+    InstanceInconsistentCaseScrutineeSet(Instance),
+
     #[display("Incomplete case analysis: covered [{}] but required [{}]",
         found.join(", "),
         required.join(", ")
@@ -38,23 +47,32 @@ pub enum CheckerError {
         found: Vec<String>,
         required: Vec<String>,
     },
+
     #[display("Instance {value} claimed to belong to {claimed} but actually belongs to {real}")]
     WrongSignatureForInstance {
         value: InstanceValue,
         claimed: Signature,
         real: Signature,
     },
+
     #[display("Instance {instance} is not of signature {claimed}: {reason}")]
     InstanceDoesNotBelong {
         instance: Instance,
         claimed: Signature,
         reason: String,
     },
+
     #[display("Non-functional instance {instance} found in application to elements {}", elements.iter().map(|e| e.to_string()).collect::<Vec<_>>().join(" "))]
     NonFunctionalInstance {
         instance: Instance,
         elements: Vec<Element>,
     },
+
+    #[display("Instance {instance} applied to too many arguments: {applied_to}")]
+    OverApplication {
+        instance: Instance,
+        applied_to: usize,
+    },
 }
 
 // -----------------------------------------------------------------------------