fix failure to add hypotheticals for instances of compound signatures

3 files changed, 58 insertions, 6 deletions

diff --git a/examples/equality.makkai b/examples/equality.makkai
index 86b81ae..294dafc 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -54,7 +54,7 @@ let signature NeqParticular = theory {
     Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty>
 }
 
-let instance zeroNeqOne :: NeqParticular = {
+let instance zeroNeqOneAgain :: NeqParticular = {
     .SE = eqTwo,
     .A = <zero. pt>,
     .B = <one. pt>,
diff --git a/examples/tests/test_projection.makkai b/examples/tests/test_projection.makkai
new file mode 100644
index 0000000..2c4ce23
--- /dev/null
+++ b/examples/tests/test_projection.makkai
@@ -0,0 +1,10 @@
+let signature S = theory {
+    A :: Set,
+    Point :: <A>,
+    B :: (x : set-of(A)) -> Set
+}
+
+let signature T = theory {
+    SI :: S,
+    F :: (r: set-of((SI .B) (element-of(SI .Point)))) -> Set
+}
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 6acd271..55682a9 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -90,11 +90,11 @@ impl CheckerState {
                 let mut new_fields = Vec::new();
                 for Field { carries, name } in fields {
                     let signature = ctx.check_signature(carries)?;
-                    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())))?;
-                    }
+                    ctx._recursively_add_hypothetical_instance(
+                        name.clone(),
+                        signature.clone(),
+                        None,
+                    )?;
                     new_fields.push(Field {
                         name: name.clone(),
                         carries: signature,
@@ -112,6 +112,48 @@ impl CheckerState {
         }
     }
 
+    // the goal here is to spread the love: if we are adding a hypothetical of
+    // some signature _ : theory { ... } then we must recurse into all of those
+    // fields and add hypotheticals for them---but, we need to build the tree as
+    // we go, giving them the concrete value of their path from the root (our
+    // canonical form).
+    fn _recursively_add_hypothetical_instance(
+        &mut self,
+        name: String,
+        signature: Signature,
+        head: Option<&Instance>,
+    ) -> Result<(), CheckerError> {
+        let value = match head {
+            Some(h) => InstanceValue::Concrete(Instance::Project {
+                instance: Box::new(h.clone()),
+                field: name.clone(),
+            }),
+            None => InstanceValue::Hypothetical,
+        };
+        let self_instance = match head {
+            Some(h) => Instance::Project {
+                instance: Box::new(h.clone()),
+                field: name.clone(),
+            },
+            None => Instance::Var(name.clone()),
+        };
+        // handle the special case canonical form for _ :: Set
+        if signature == Signature::Set {
+            self.add_set(name.clone(), Set::ClaimedSet(self_instance.clone()))?;
+        }
+        self.add_instance(name.clone(), value, signature.clone())?;
+        if let Signature::Theory(fields) = signature {
+            for f in fields {
+                self._recursively_add_hypothetical_instance(
+                    f.name,
+                    f.carries,
+                    Some(&self_instance),
+                )?;
+            }
+        }
+        Ok(())
+    }
+
     #[instrument(skip(self), level = "debug", fields(%instance, signature=%signature.map(|s| s.to_string()).unwrap_or_default()) )]
     pub fn check_instance(
         &self,