Definitional eta equality

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