From ece72d34809af0060d62e1841b1a76478db5a44a Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Wed, 29 Apr 2026 20:47:53 +0100
Subject: wip on App For

---
 src/checker_signature.rs | 99 ++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 78 insertions(+), 21 deletions(-)

(limited to 'src/checker_signature.rs')

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 7b07105..e86ff9e 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -198,6 +198,10 @@ impl CheckerState {
                 todo!("instance for")
             }
             Instance::App(inner, element) => {
+                // this is the only time that we ever call check_instance with
+                // signature = None, and in this mode all we want is to put
+                // inner into a canonical form pushing stuck terms to the leaves
+                // and simplifying everything else.
                 let inner = self.check_instance(inner, None)?;
                 match &inner {
                     Instance::Var(v) => {
@@ -245,28 +249,81 @@ impl CheckerState {
                                 "It should have been impossible to construct a For with no params, but here we are"
                             );
                         }
-                        let mut ctx = self.clone();
-                        for (idx, param) in params.iter().enumerate() {
-                            let Param {
-                                name: param_name,
-                                set: param_set,
-                            } = param.clone();
-                            if idx == 0 {
-                                let element = self.check_element(&*element, &param_set)?;
-                                ctx.make_element_definition(param_name, element, param_set)?;
-                            } else {
-                                ctx.make_element_binding(param_name, param_set)?;
-                            }
-                        }
-                        let instance = ctx.check_instance(body, signature)?;
-                        if params.len() == 1 {
-                            Ok(instance)
-                        } else {
-                            Ok(Instance::For {
-                                params: params[1..].iter().map(|p| p.clone()).collect(),
-                                body: Box::new(instance),
-                            })
+                        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");
                     }
                     Instance::Record(_) | Instance::SetCoerce(_) => {
                         Err(CheckerError::NonFunctionalInstance {
-- 
cgit v1.3.1