From b819f56aed5291dabbad7d35eddc10aa36525346 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Thu, 25 Feb 2021 13:55:13 -0300
Subject: [PATCH] Definitional eta equality

---
 src/Elab/Eval.hs | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index 1dfcc2a..c03c4de 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -97,15 +97,27 @@ unify topa topb = join $ go <$> forceIO topa <*> forceIO topb where
       traverse_ (uncurry unifySpine) (zip a a')
     | otherwise = fail
 
-  go (VLam p (Closure _ k)) (VLam p' (Closure _ k')) | p == p' = do
+  go (VLam p (Closure _ k)) vl = do
     t <- VVar . Bound <$> newName
-    unify (k t) (k' t)
+    unify (k t) (vApp p vl t)
+
+  go vl (VLam p (Closure _ k)) = do
+    t <- VVar . Bound <$> newName
+    unify (vApp p vl t) (k t)
+
+  go (VPair a b) vl = unify a (vProj1 vl) *> unify b (vProj2 vl)
+  go vl (VPair a b) = unify (vProj1 vl) a *> unify (vProj2 vl) b
 
   go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
     t <- VVar . Bound <$> newName
     unify d d'
     unify (k t) (k' t)
 
+  go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
+    t <- VVar . Bound <$> newName
+    unify d d'
+    unify (k t) (k' t)
+
   go _ _ = fail
 
   fail = liftIO . throwIO $ NotEqual topa topb