From 27ed463f264a701e336eddc86452fa41f28dd111 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Tue, 5 May 2026 14:55:42 +0100
Subject: fix ext nesting, don't register junky intermediate signatures

---
 src/checker_signature.rs | 53 ++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 42 insertions(+), 11 deletions(-)

(limited to 'src/checker_signature.rs')

diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 2888568..0145e82 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -15,36 +15,67 @@ impl CheckerState {
                 Ok(deref.clone())
             }
             Signature::Ext { params, codomain } => {
+                if params.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "extension signature with empty params".to_string(),
+                    ));
+                }
                 let mut ctx = self.clone();
+
+                // a little juggling here to ensure that we merge names without
+                // collision, the pattern is: bind to something unique, recurse,
+                // fix the names which involves in particular messing about with
+                // counters
                 let params = params
                     .iter()
                     .map(|p| {
                         let set = ctx.check_set(&p.set)?;
-                        let canon = ctx.make_element_binding(p.name.clone(), set.clone())?;
+                        let canon = ctx.make_unique_name();
+                        ctx.add_element(
+                            p.name.clone(),
+                            Element::Var(canon.clone()).into(),
+                            set.clone(),
+                        )?;
+                        ctx.add_element(canon.clone(), ElementValue::Hypothetical, set.clone())?;
                         Ok(Param { set, name: canon })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
+
+                // use tactic "trust_me"
+                let snapshot = ctx.get_binder_counter();
                 let codomain = ctx.check_signature(codomain)?;
+                ctx.set_binder_counter(snapshot);
 
-                let result = if let Signature::Ext {
+                let (params, codomain) = if let Signature::Ext {
                     params: inner,
                     codomain: deep,
                 } = codomain
                 {
                     let mut merged = params.clone();
                     merged.extend(inner.iter().cloned());
-                    Signature::Ext {
-                        params: merged,
-                        codomain: deep,
-                    }
+                    (merged, *deep)
                 } else {
-                    Signature::Ext {
-                        params,
-                        codomain: Box::new(codomain),
-                    }
+                    (params, codomain)
                 };
 
-                Ok(result)
+                // normalise
+                let mut ctx = self.clone();
+                let params = params
+                    .into_iter()
+                    .map(|Param { name, set }| {
+                        let canonical = ctx.make_element_binding(name, set.clone())?;
+                        Ok(Param {
+                            name: canonical,
+                            set,
+                        })
+                    })
+                    .collect::<Result<Vec<_>, _>>()?;
+                let codomain = ctx.check_signature(&codomain)?;
+
+                Ok(Signature::Ext {
+                    params,
+                    codomain: Box::new(codomain),
+                })
             }
             Signature::Theory(fields) => {
                 let mut ctx = self.clone();
-- 
cgit v1.3.1