fix failure to add hypotheticals for instances of compound signatures

2 files changed, 11 insertions, 1 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
+}