finish the implementation, we don't have motives so this is how it will have to stay

1 files changed, 25 insertions, 42 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 9d0bffe..1ce8bc8 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -1,6 +1,6 @@
 use crate::ast::*;
 use crate::checker_state::*;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::iter::zip;
 
 use tracing::instrument;
@@ -80,6 +80,11 @@ impl CheckerState {
                 })
             }
             Signature::Theory(fields) => {
+                let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
+                if field_set.len() != fields.len() {
+                    return Err(CheckerError::DuplicateFieldsSignature(signature.clone()));
+                }
+
                 let mut ctx = self.clone();
                 let temp_name = ctx.make_unique_name();
                 let mut new_fields = Vec::new();
@@ -132,7 +137,7 @@ impl CheckerState {
                 }
             }
             Instance::ElementCoerce(element) => {
-                if let Some(signature) = signature {
+                let set = if let Some(signature) = signature {
                     let Signature::FromSet(set) = signature else {
                         return Err(CheckerError::WrongSignatureForInstance {
                             value: instance.clone().into(),
@@ -140,26 +145,13 @@ impl CheckerState {
                             claimed: signature.clone(),
                         });
                     };
-                    println!("{self}");
-                    let element = self.check_element(element, set)?;
-                    Ok(Instance::ElementCoerce(element))
+                    Some(set)
                 } else {
-                    // todo!("how do we handle check_element without a set?");
-                    println!("THISISATTODO");
-                    // quick hack:
-                    let element = if let Element::Var(v) = element {
-                        let lookup = self.lookup_element(&v)?;
-                        if let ElementValue::Concrete(ref x) = lookup.value {
-                            x.clone()
-                        } else {
-                            element.clone()
-                        }
-                    } else {
-                        element.clone()
-                    };
+                    None
+                };
 
-                    Ok(Instance::ElementCoerce(element.clone()))
-                }
+                let element = self.check_element(element, set)?;
+                Ok(Instance::ElementCoerce(element))
             }
             Instance::Var(v) => {
                 // Exactly the same discipline as for Element::Var, see there
@@ -337,7 +329,7 @@ impl CheckerState {
                         required: required_field_names_sorted,
                     });
                 }
-                let scrutinee = self.check_element(scrutinee, owner)?;
+                let scrutinee = self.check_element(scrutinee, Some(owner))?;
 
                 let matching: Option<(String, Element)> = match scrutinee {
                     Element::Inject {
@@ -376,12 +368,8 @@ impl CheckerState {
                     {
                         let canonical =
                             ctx.make_element_definition(binding_name, inner.clone(), binding_set)?;
-                        let this_signature = if let Some(signature) = signature {
-                            let signature = ctx.check_signature(signature)?;
-                            Some(signature)
-                        } else {
-                            None
-                        };
+                        let this_signature =
+                            signature.map(|s| ctx.check_signature(s)).transpose()?;
 
                         let output =
                             ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
@@ -409,13 +397,8 @@ impl CheckerState {
                                 owner.clone(),
                             )?;
                         };
-                        let this_signature = if let Some(signature) = signature {
-                            let signature = ctx.check_signature(signature)?;
-                            Some(signature)
-                        } else {
-                            None
-                        };
-
+                        let this_signature =
+                            signature.map(|s| ctx.check_signature(s)).transpose()?;
                         let body =
                             ctx.check_instance((&arm.body).into(), this_signature.as_ref())?;
                         CaseArm {
@@ -683,7 +666,7 @@ impl CheckerState {
         let checked = zip(params.iter(), args.iter())
             .map(|(p, a)| {
                 let p_set = ctx.check_set(&p.set)?;
-                let a = ctx.check_element(a, &p_set)?;
+                let a = ctx.check_element(a, Some(&p_set))?;
                 ctx.add_element(p.name.clone(), a.clone().into(), p_set)?;
                 Ok(a)
             })
@@ -697,13 +680,13 @@ impl CheckerState {
             Instance::Project { field, .. } => {
                 Ok(Some(self.lookup_signature_field(field)?.field.clone()))
             }
-            // All arms of a stuck Case share a signature by the case
-            // elimination typing rule, and we've already expanded the body, so
-            // we can pick any arm.
-
-            // TODO! this is wrong!
-            Instance::Case { arms, .. } => self
-                ._stuck_subject_signature(&arms.first().expect("we don't allow bottom type").body),
+            // until we properly support motives there's nothing we can really do here
+            Instance::Case { .. } => {
+                let msg = format!(
+                    "this type checker has no motives yet, and was called upon to infer the signature of {inst}, which leads with a `case`, and so has no option but to fail"
+                );
+                Err(CheckerError::Unimplemented(msg))
+            }
             Instance::ElementCoerce(_)
             | Instance::For { .. }
             | Instance::Record(_)