address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme

12 files changed, 164 insertions, 47 deletions

diff --git a/README.md b/README.md
index a6cf033..1ff5a86 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,22 @@
 
 A simple type theory.
 
+## Motivation
+
+There's a pleasant story here about categorical semantics in `Alg(Fam(Lex))^op`, but the real impetus for developing and implementing this particular fragment was the exercise: i had never implemented a dependent type theory before, and wanted to know whether i could deduce how to do so by trying. You, the reader, may be the judge of those efforts.
+
+As a consequence, this code is 100% artisanal, hand-crafted, guaranteed-cruft-and-hacks human written (by me).
+
+Credit goes to [David Jaz](https://www.davidjaz.com/) for developing the fragment and its semantics. Credit goes to me for introducing errors.
+
+## Rust implementation
+
+Usage `makkai [--debug] file1.makkai ... fileN.makkai`
+
+See the [grammar](grammar.txt) for details, and the examples in `examples/`.
+
+Note: the checker does not presently support η-equivalence in all cases and so has some known errors, and likely therefore, some unknown errors.
+
 ## Type Theory
 
 ### Judgements
@@ -74,15 +90,6 @@ A construction admitting an instance of any signature, given an element of a var
 - **Intro.** `C ⊢ case m of { v0. x0 => I0 | ... | vn. xn => In } :: S` when `C ⊢ S signature`, `C ⊢ m : variant { v0. : X0 | ... | vn. : Xn }`, and, for each `i`, `C, xi : Xi ⊢ Ii :: S`.
 - **β.** `case vi. m of { ... | vi. xi => Ii | ... }=Ii[m/xi]`.
 
-
-## Rust implementation
-
-Usage `makkai [--debug] file1.makkai ... fileN.makkai`
-
-See the [grammar](grammar.txt) for details, and the examples in `examples/`.
-
-Note: the checker does not presently support η-equivalence in all cases.
-
 # License
 
 Copyright tslil clingman 2026, this programme is free software and is made available under the terms of the GPL v3 or later. See LICENSE for details.
diff --git a/examples/alpha_equiv.makkai b/examples/alpha_equiv.makkai
new file mode 100644
index 0000000..2ae067a
--- /dev/null
+++ b/examples/alpha_equiv.makkai
@@ -0,0 +1,4 @@
+let signature S = (n : Nat) -> Set
+let signature T = (m : Nat) -> Set
+let instance i :: S = for (x : Nat), (Nat :: Set)
+let instance j :: T = i
diff --git a/examples/equality.makkai b/examples/equality.makkai
new file mode 100644
index 0000000..a9b3368
--- /dev/null
+++ b/examples/equality.makkai
@@ -0,0 +1,19 @@
+let set Empty = variant[]
+let set Unit = record {}
+let element pt : Unit = {}
+
+let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
+
+let signature EqS = (x : Three) (y: Three) -> theory { E :: Set }
+let instance eqThree :: EqS = for (x: Three) (y: Three), {
+    .E = case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
+                   | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ]
+                   | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ]
+                   ]
+}
+
+let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) }
+
+let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
+
+let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt }
diff --git a/examples/ext_codomain.makkai b/examples/ext_codomain.makkai
new file mode 100644
index 0000000..da0ddae
--- /dev/null
+++ b/examples/ext_codomain.makkai
@@ -0,0 +1,5 @@
+let signature S = (x : Nat) -> theory { G :: Set }
+
+let instance s :: S = for (x : Nat), { .G = (Nat :: Set) }
+
+let set NatAgain = set-of((s 42) .G)
diff --git a/examples/inline_nested.makkai b/examples/inline_nested.makkai
new file mode 100644
index 0000000..e891349
--- /dev/null
+++ b/examples/inline_nested.makkai
@@ -0,0 +1,9 @@
+let signature Outer = theory {
+    Inner :: theory { F :: Set }
+}
+
+let instance my_outer :: Outer = {
+    .Inner = { .F = (Nat :: Set) }
+}
+
+let set MyF = set-of(my_outer .Inner .F)
diff --git a/examples/nested_for.makkai b/examples/nested_for.makkai
new file mode 100644
index 0000000..b3618cc
--- /dev/null
+++ b/examples/nested_for.makkai
@@ -0,0 +1,3 @@
+let signature F = (n : Nat) -> (m : Nat) -> Set
+let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set)
+let set Result = set-of(f 1 2)
diff --git a/src/ast.rs b/src/ast.rs
index 76b6c9f..e254c65 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -71,7 +71,7 @@ pub enum Signature {
     #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
     Theory(Vec<Field<Signature>>),
 
-    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
+    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(""), codomain)]
     Ext {
         params: Vec<Param>,
         codomain: Box<Signature>,
diff --git a/src/checker.rs b/src/checker.rs
index fdba181..c381ba4 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -16,11 +16,12 @@ impl CheckerState {
         let Programme(decls) = prog;
 
         for decl in decls {
+            self.reset_binders();
             match decl {
                 Decl::Set { name, set } => {
                     self.assert_unbound_set(name)?;
                     let set = self.check_set(set)?;
-                    self.add_set(name.clone(), set.into())
+                    self.add_set(name.clone(), set)
                 }
 
                 Decl::Element { name, element, set } => {
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 98e10ec..a00ea81 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -1,7 +1,7 @@
 use crate::ast::*;
 use crate::checker_state::*;
 
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use tracing::instrument;
 
 impl CheckerState {
@@ -11,6 +11,10 @@ impl CheckerState {
             Set::BuiltIn(_) => Ok(set.clone()),
             Set::Record(fields) => {
                 let mut ctx = self.clone();
+                let field_set = fields.iter().map(|f| &f.name).collect::<HashSet<&String>>();
+                if field_set.len() != fields.len() {
+                    todo!("duplicate fields");
+                }
                 let fields = fields
                     .into_iter()
                     .map(|Field { name, carries }| {
@@ -260,7 +264,6 @@ impl CheckerState {
                 })
             }
             Element::Case { arms, scrutinee } => {
-                // TODO: do we allow mapping out of bottom?
                 if arms.is_empty() {
                     return Err(CheckerError::Unimplemented(
                         "mapping out of bottom types".to_string(),
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index beb0af6..2888568 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -24,8 +24,27 @@ impl CheckerState {
                         Ok(Param { set, name: canon })
                     })
                     .collect::<Result<Vec<_>, _>>()?;
-                let codomain = Box::new(ctx.check_signature(codomain)?);
-                Ok(Signature::Ext { params, codomain })
+                let codomain = ctx.check_signature(codomain)?;
+
+                let result = 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,
+                    }
+                } else {
+                    Signature::Ext {
+                        params,
+                        codomain: Box::new(codomain),
+                    }
+                };
+
+                Ok(result)
             }
             Signature::Theory(fields) => {
                 let mut ctx = self.clone();
@@ -36,10 +55,7 @@ impl CheckerState {
                     ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?;
                     // And lo, the special case, our chosen canonical form
                     if signature == Signature::Set {
-                        ctx.add_set(
-                            name.clone(),
-                            Set::ClaimedSet(Instance::Var(name.clone())).into(),
-                        )?;
+                        ctx.add_set(name.clone(), Set::ClaimedSet(Instance::Var(name.clone())))?;
                     }
                     new_fields.push(Field {
                         name: name.clone(),
@@ -153,7 +169,7 @@ impl CheckerState {
                                 if f_s == Signature::Set {
                                     ctx.add_set(
                                         f_n.clone(),
-                                        Set::ClaimedSet(Instance::Var(f_n.clone())).into(),
+                                        Set::ClaimedSet(Instance::Var(f_n.clone())),
                                     )?;
                                 }
 
@@ -316,12 +332,37 @@ impl CheckerState {
                 params: inst_params,
                 body,
             } => {
+                if inst_params.is_empty() {
+                    return Err(CheckerError::Unimplemented(
+                        "for instance with empty params".to_string(),
+                    ));
+                }
+
+                // deal with left-nesting
+                let mut ctx = self.clone();
+                for Param { name, set } in inst_params {
+                    ctx.make_element_binding(name.clone(), set.clone())?;
+                }
+                let body = ctx.check_instance(body, None)?;
+                let (inst_params, body) = if let Instance::For {
+                    params: inner_params,
+                    body: inner_body,
+                } = body
+                {
+                    let mut merged = inst_params.clone();
+                    merged.extend(inner_params.clone());
+                    (merged, *inner_body)
+                } else {
+                    (inst_params.clone(), body)
+                };
+
                 if let Some(signature) = signature {
                     if inst_params.is_empty() {
                         return Err(CheckerError::Unimplemented(
                             "instance for with empty params".to_string(),
                         ));
                     };
+
                     let Signature::Ext {
                         params: sig_params,
                         codomain,
@@ -339,11 +380,13 @@ impl CheckerState {
                             claimed: signature.clone(),
                         });
                     };
+
                     if sig_params.is_empty() {
                         return Err(CheckerError::Unimplemented(
                             "extension signature with empty params".to_string(),
                         ));
                     }
+
                     if sig_params.len() != inst_params.len() {
                         return Err(CheckerError::InstanceDoesNotBelong {
                             instance: instance.clone(),
@@ -365,7 +408,7 @@ impl CheckerState {
                                     set: set_s,
                                 },
                             )| {
-                                let inst_s = ctx.check_set(inst_s)?;
+                                let inst_s = ctx.check_set(&inst_s)?;
                                 let set_s = ctx.check_set(set_s)?;
                                 if !ctx.equal(&inst_s, &set_s) {
                                     return Err(CheckerError::InstanceDoesNotBelong{
@@ -387,7 +430,7 @@ impl CheckerState {
                             },
                         )
                         .collect::<Result<Vec<_>, _>>()?;
-                    let body = ctx.check_instance(body, Some(&*codomain))?;
+                    let body = ctx.check_instance(&body, Some(&*codomain))?;
                     Ok(Instance::For {
                         body: Box::new(body),
                         params: inst_params,
@@ -405,7 +448,7 @@ impl CheckerState {
                             })
                         })
                         .collect::<Result<Vec<_>, _>>()?;
-                    let body = ctx.check_instance(body, None)?;
+                    let body = ctx.check_instance(&body, None)?;
                     Ok(Instance::For {
                         params: inst_params,
                         body: Box::new(body),
@@ -416,18 +459,11 @@ impl CheckerState {
                 instance: inner,
                 args,
             } => {
-                // 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 subject = self.check_instance(inner, None)?;
-
                 // the whole game here is to make sure that we have no left
                 // nesting, and that we're fully evaluated. If that's true then
-                // we don't need to come up with signatures for partial
-                // application. The parser already enforces this, but the
-                // cunning user may supply ASTs directly so we do this here as
-                // well.
+                // structural equality is much more powerful, and partial
+                // application is simpler.
                 let (subject, args) = match subject {
                     Instance::App {
                         instance: inner_inner,
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 3404a35..45d2dab 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -272,27 +272,27 @@ impl CheckerState {
     }
 
     #[instrument(skip(self), level = "debug", fields(%name, %set))]
-    pub fn add_set(&mut self, name: String, set: SetValue) -> Result<(), CheckerError> {
+    pub fn add_set(&mut self, name: String, set: Set) -> Result<(), CheckerError> {
         match &set {
-            SetValue::Concrete(set @ Set::Record(fields)) => {
+            Set::Record(fields) => {
                 for Field {
                     name: rfn,
                     carries: field_set,
                 } in fields
                 {
-                    self.add_record_field(rfn, field_set, set)?;
+                    self.add_record_field(rfn, field_set, &set)?;
                 }
             }
-            SetValue::Concrete(set @ Set::Variant(fields)) => {
+            Set::Variant(fields) => {
                 for Field {
                     name: vfn,
                     carries: field_set,
                 } in fields
                 {
-                    self.add_variant_field(vfn, field_set, set)?;
+                    self.add_variant_field(vfn, field_set, &set)?;
                 }
             }
-            _ => (),
+            Set::Var(_) | Set::BuiltIn(_) | Set::ClaimedSet(_) => (),
         };
         self.wf_sets.insert(name, set.into());
         Ok(())
@@ -394,14 +394,16 @@ impl CheckerState {
                     carries: field_sig,
                 } in fields
                 {
-                    // TODO: are we supposed to recurse?
-                    // let name = self.make_unique_name();
-                    // self.add_signature(&name, field_sig.clone(), rebind)?;
+                    let inner_name = self.make_unique_name();
+                    self.add_signature(&inner_name, field_sig.clone(), rebind)?;
                     self.add_signature_field(field_name, field_sig, &signature, rebind)?;
                 }
             }
-            // TODO: is there more?
-            _ => (),
+            Signature::Ext { codomain, .. } => {
+                let inner_name = self.make_unique_name();
+                self.add_signature(&inner_name, (**codomain).clone(), rebind)?;
+            }
+            Signature::Set | Signature::Var(_) => (),
         };
 
         self.wf_signatures.insert(name.clone(), signature);
@@ -487,4 +489,8 @@ impl CheckerState {
         let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
         _reserved_name(n)
     }
+
+    pub fn reset_binders(&mut self) {
+        self.binder_element.store(0, Ordering::Relaxed);
+    }
 }
diff --git a/src/parser.rs b/src/parser.rs
index 4e41644..31956bd 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -154,11 +154,23 @@ parser! {
         = _ n:upper_ident() _ "::" _ s:signature() _
         { Field { name: n, carries: s } }
 
+        rule sig_ext() -> Signature
+        = ps:param_list() _ "->" _ cod:signature()
+        {
+            match cod {
+                Signature::Ext { params: inner, codomain } => {
+                    let mut all = ps;
+                    all.extend(inner);
+                    Signature::Ext { params: all, codomain }
+                }
+                other => Signature::Ext { params: ps, codomain: Box::new(other) },
+            }
+        }
+
         rule signature() -> Signature
         = kw_Set()    { Signature::Set }
         / kw_theory() _ "{" _ fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
-        / ps:param_list() _ "->" _ cod:signature()
-        { Signature::Ext { params: ps, codomain: Box::new(cod) } }
+        / s:sig_ext() { s }
         / v:sig_var()                 { Signature::Var(v) }
         / "(" _ s:signature() _ ")"   { s }
 
@@ -243,9 +255,21 @@ parser! {
             }
         }
 
-        rule instance() -> Instance
+        rule inst_for() -> Instance
         = kw_for() _ ps:param_list() _ "," _ body:instance()
-        { Instance::For { params: ps, body: Box::new(body) } }
+        {
+            match body {
+                Instance::For { params: inner, body } => {
+                    let mut all = ps;
+                    all.extend(inner);
+                    Instance::For { params: all, body }
+                }
+                other => Instance::For { params: ps, body: Box::new(other) },
+            }
+        }
+
+        rule instance() -> Instance
+        = i:inst_for() { i }
         / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(inst_case_arm() ** "|") _ "]"
         { Instance::Case { scrutinee: Box::new(scrut), arms } }
         / app_inst()