fill in some more todos

1 files changed, 40 insertions, 81 deletions

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 6633dd1..89f4441 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -276,7 +276,23 @@ impl CheckerState {
                         params: inst_params,
                     })
                 } else {
-                    todo!("expand only mode???")
+                    let mut ctx = self.clone();
+                    let inst_params = inst_params
+                        .iter()
+                        .map(|Param { name, set }| {
+                            let set = ctx.check_set(set)?;
+                            let canon = ctx.make_element_binding(name.clone(), set.clone())?;
+                            Ok(Param {
+                                name: canon,
+                                set: set,
+                            })
+                        })
+                        .collect::<Result<Vec<_>, _>>()?;
+                    let body = ctx.check_instance(body, None)?;
+                    Ok(Instance::For {
+                        params: inst_params,
+                        body: Box::new(body),
+                    })
                 }
             }
             Instance::App(inner, element) => {
@@ -326,86 +342,29 @@ impl CheckerState {
                         ))
                     }
                     Instance::For { params, body } => {
-                        // if params.is_empty() {
-                        //     panic!(
-                        //         "It should have been impossible to construct a For with no params, but here we are"
-                        //     );
-                        // }
-                        // if let Some(signature) = signature {
-                        //     let Signature::Ext {
-                        //         params: sig_params,
-                        //         codomain,
-                        //     } = signature
-                        //     else {
-                        //         return Err(CheckerError::WrongSignatureForInstance {
-                        //             value: inner.clone().into(),
-                        //             claimed: signature.clone(),
-                        //             real: Signature::Ext {
-                        //                 params: vec![Param {
-                        //                     name: "...".to_string(),
-                        //                     set: Set::Var("...".to_string()),
-                        //                 }],
-                        //                 codomain: Box::new(Signature::Var("...".to_string())),
-                        //             },
-                        //         });
-                        //     };
-                        //     if params.len() != sig_params.len() {
-                        //         todo!("raise an error about incorrect signature")
-                        //     };
-                        //     let mut ctx = self.clone();
-                        //     let (params, sig_params): (Vec<Param>, Vec<Param>) =
-                        //         zip(params, sig_params)
-                        //             .enumerate()
-                        //             .map(|(idx, (a_p, s_p))| {
-                        //                 let a_set = ctx.check_set(&a_p.set)?;
-                        //                 let p_set = ctx.check_set(&s_p.set)?;
-                        //                 if !ctx.equal(&a_set, &p_set) {
-                        //                     todo!(
-                        //                         "raise an error about the for/Ext being incorrect"
-                        //                     );
-                        //                 }
-                        //                 if idx == 0 {
-                        //                     let element = ctx.check_element(&*element, &p_set)?;
-                        //                     ctx.make_element_definition(
-                        //                         a_p.name.clone(),
-                        //                         element.clone(),
-                        //                         a_set.clone(),
-                        //                     )?;
-                        //                     ctx.make_element_definition(
-                        //                         s_p.name.clone(),
-                        //                         element,
-                        //                         p_set.clone(),
-                        //                     )?;
-                        //                 } else {
-                        //                     let canon_a = ctx.make_element_binding(
-                        //                         a_p.name.clone(),
-                        //                         a_set.clone(),
-                        //                     )?;
-                        //                     ctx.add_element(
-                        //                         s_p.name.clone(),
-                        //                         Element::Var(canon_a).into(),
-                        //                         p_set.clone(),
-                        //                     )?;
-                        //                 }
-                        //                 Ok((
-                        //                     Param {
-                        //                         name: a_p.name.clone(),
-                        //                         set: a_set,
-                        //                     },
-                        //                     Param {
-                        //                         name: s_p.name.clone(),
-                        //                         set: p_set,
-                        //                     },
-                        //                 ))
-                        //             })
-                        //             .collect::<Result<_, _>>()?;
-                        //     // TODO: now we need to build a new For and a new
-                        //     // Ext, and check the latter then check that the
-                        //     // former fits the latter. The base case would be
-                        //     // checking that body's expected signature is
-                        //     // codomain.
-                        // }
-                        todo!("finish this");
+                        if params.is_empty() {
+                            panic!(
+                                "it should have been impossible to construct a for with no parameters, but here we are"
+                            );
+                        }
+                        let mut ctx = self.clone();
+                        let first_set = ctx.check_set(&params[0].set)?;
+                        let element_checked = self.check_element(element, &first_set)?;
+                        ctx.make_element_definition(
+                            params[0].name.clone(),
+                            element_checked,
+                            first_set,
+                        )?;
+
+                        if params.len() == 1 {
+                            ctx.check_instance(body, signature)
+                        } else {
+                            let residual = Instance::For {
+                                params: params[1..].to_vec(),
+                                body: body.clone(),
+                            };
+                            ctx.check_instance(&residual, signature)
+                        }
                     }
                     Instance::Record(_) | Instance::SetCoerce(_) => {
                         Err(CheckerError::NonFunctionalInstance {