diff --git a/src/Core/Domain.hs b/src/Core/Domain.hs
index bb3b28f..d639fa3 100644
--- a/src/Core/Domain.hs
+++ b/src/Core/Domain.hs
@@ -93,9 +93,25 @@ pattern Empty :: Spine
 pattern Empty =
   Spine Seq.Empty Seq.Empty
 
+pattern (:<) :: Elimination -> Spine -> Spine
+pattern elimination :< spine <-
+  (eliminationViewL -> Just (elimination, spine))
+  where
+    elim :< Spine spine args =
+      case elim of
+        App plicity arg ->
+          case spine of
+            Seq.Empty -> Spine Seq.Empty ((plicity, arg) Seq.:<| args)
+            (apps, brs) Seq.:<| spine' ->
+              Spine (((plicity, arg) Seq.:<| apps, brs) Seq.:<| spine') args
+        Case brs ->
+          Spine ((Seq.Empty, brs) Seq.:<| spine) args
+
+{-# COMPLETE Empty, (:<) #-}
+
 pattern (:>) :: Spine -> Elimination -> Spine
 pattern spine :> elimination <-
-  (eliminationView -> Just (spine, elimination))
+  (eliminationViewR -> Just (spine, elimination))
   where
     Spine spine args :> elim =
       case elim of
@@ -113,8 +129,19 @@ pattern Apps args <-
     Apps args =
       Spine Seq.Empty args
 
-eliminationView :: Spine -> Maybe (Spine, Elimination)
-eliminationView (Spine spine apps) =
+eliminationViewL :: Spine -> Maybe (Elimination, Spine)
+eliminationViewL (Spine spine apps) =
+  case spine of
+    Seq.Empty -> case apps of
+      Seq.Empty -> Nothing
+      (plicity, arg) Seq.:<| apps' -> Just (App plicity arg, Spine spine apps')
+    (Seq.Empty, brs) Seq.:<| spine' ->
+      Just (Case brs, Spine spine' apps)
+    ((plicity, arg) Seq.:<| apps', brs) Seq.:<| spine' ->
+      Just (App plicity arg, Spine ((apps', brs) Seq.:<| spine') apps)
+
+eliminationViewR :: Spine -> Maybe (Spine, Elimination)
+eliminationViewR (Spine spine apps) =
   case apps of
     Seq.Empty ->
       case spine of
diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs
index 0358ea4..3bd4222 100644
--- a/src/Elaboration/Context.hs
+++ b/src/Elaboration/Context.hs
@@ -275,13 +275,13 @@ extendBefore context beforeVar binding type_ = do
     )
 
 defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
-defineWellOrdered context head spine value =
+defineWellOrdered context head_ spine value =
   context
     { equations =
         context.equations
-          { equal = HashMap.insertWith (<>) head [(spine, value)] context.equations.equal
+          { equal = HashMap.insertWith (<>) head_ [(spine, value)] context.equations.equal
           }
-    , boundVars = case (head, spine) of
+    , boundVars = case (head_, spine) of
         (Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
         _ -> context.boundVars
     }
@@ -292,9 +292,9 @@ skip context = do
   pure context'
 
 define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
-define context head spine value = do
+define context head_ spine value = do
   deps <- evalStateT (freeVars context value) mempty
-  let context' = defineWellOrdered context head spine value
+  let context' = defineWellOrdered context head_ spine value
       (pre, post) =
         Tsil.partition (`EnumSet.member` deps) $
           IntSeq.toTsil context'.boundVars
@@ -598,8 +598,8 @@ forceHead context value =
           forceHead context value'
         Meta.EagerUnsolved {} ->
           pure value
-    Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
+    Domain.Neutral head_ spine
+      | Just spineValues <- HashMap.lookup head_ context.equations.equal -> do
           let go [] = pure value
               go ((eqSpine, eqValue) : rest)
                 | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
@@ -637,8 +637,8 @@ forceHeadGlue context value =
           pure $ Domain.Glued (Domain.Meta metaIndex) spine $ Domain.Lazy lazyValue
         Meta.EagerUnsolved {} ->
           pure value
-    Domain.Neutral head spine
-      | Just spineValues <- HashMap.lookup head context.equations.equal -> do
+    Domain.Neutral head_ spine
+      | Just spineValues <- HashMap.lookup head_ context.equations.equal -> do
           let go [] = pure value
               go ((eqSpine, eqValue) : rest)
                 | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
@@ -646,7 +646,7 @@ forceHeadGlue context value =
                     if eq
                       then do
                         lazyValue <- lazy $ Evaluation.applySpine eqValue spineSuffix
-                        pure $ Domain.Glued head spine $ Domain.Lazy lazyValue
+                        pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
                       else go rest
               go (_ : rest) = go rest
           go spineValues
diff --git a/src/Elaboration/Depth.hs b/src/Elaboration/Depth.hs
new file mode 100644
index 0000000..6aad9b3
--- /dev/null
+++ b/src/Elaboration/Depth.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE BlockArguments #-}
+
+module Elaboration.Depth where
+
+import qualified Core.Domain as Domain
+import Monad
+import Protolude
+import qualified Query
+import qualified Query.Mapped as Mapped
+import Rock
+
+-- | Try to find out which of two heads might refer to the other so we can
+-- unfold glued values that are defined later first (see "depth" in
+-- https://arxiv.org/pdf/1505.04324.pdf).
+compareHeadDepths :: Domain.Head -> Domain.Head -> M Ordering
+compareHeadDepths head1 head2 =
+  case (head1, head2) of
+    (Domain.Global global1, Domain.Global global2) -> do
+      global1DependsOn2 <- fetch $ Query.TransitiveDependencies global2 $ Mapped.Query global1
+      global2DependsOn1 <- fetch $ Query.TransitiveDependencies global1 $ Mapped.Query global2
+      pure case (global1DependsOn2, global2DependsOn1) of
+        (Just _, Nothing) -> GT
+        (Nothing, Just _) -> LT
+        _ -> EQ
+    (_, Domain.Global _) -> pure LT
+    (Domain.Global _, _) -> pure GT
+    (Domain.Var v1, Domain.Var v2) -> pure $ compare v1 v2
+    _ -> pure EQ
diff --git a/src/Elaboration/Unification/Indices.hs b/src/Elaboration/Equation.hs
similarity index 55%
rename from src/Elaboration/Unification/Indices.hs
rename to src/Elaboration/Equation.hs
index fb4db05..0f7f611 100644
--- a/src/Elaboration/Unification/Indices.hs
+++ b/src/Elaboration/Equation.hs
@@ -6,7 +6,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE NoFieldSelectors #-}
 
-module Elaboration.Unification.Indices where
+module Elaboration.Equation where
 
 import Control.Exception.Lifted
 import qualified Core.Binding as Binding
@@ -21,6 +21,7 @@ import qualified Data.OrderedHashMap as OrderedHashMap
 import qualified Data.Tsil as Tsil
 import Elaboration.Context (Context)
 import qualified Elaboration.Context as Context
+import Elaboration.Depth (compareHeadDepths)
 import qualified Environment
 import Flexibility (Flexibility)
 import qualified Flexibility
@@ -38,32 +39,38 @@ data Error
   | Dunno
   deriving (Eq, Ord, Show, Exception)
 
-data UnificationState v = UnificationState
+data EquationState v = EquationState
   { context :: !(Context v)
   , touchableBefore :: !(Index (Succ v))
   }
 
-type Unify v = StateT (UnificationState v) M
+type Equate v = StateT (EquationState v) M
 
-unify :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v)
-unify context flexibility value1 value2 =
+equate :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v)
+equate context flexibility value1 value2 =
   (.context)
     <$> execStateT
-      (unifyM flexibility value1 value2)
-      UnificationState
+      (equateM flexibility value1 value2)
+      EquationState
         { context = context
         , touchableBefore = Index.Zero
         }
 
-isTouchable :: Var -> Unify v Bool
-isTouchable var = do
+isTouchableVar :: Var -> Equate v Bool
+isTouchableVar var = do
   touchableIndex <- gets (.touchableBefore)
   context <- gets (.context)
   pure case Context.lookupVarIndex var context of
     Just varIndex -> Index.Succ varIndex > touchableIndex
     Nothing -> False
 
-extend :: Name -> Domain.Type -> (Var -> Unify (Succ v) a) -> Unify v a
+isTouchable :: Domain.Head -> Equate v Bool
+isTouchable head_ = case head_ of
+  Domain.Meta _ -> pure False
+  Domain.Var var -> isTouchableVar var
+  Domain.Global _ -> pure True
+
+extend :: Name -> Domain.Type -> (Var -> Equate (Succ v) a) -> Equate v a
 extend name type_ k = do
   st <- get
   (result, st') <- lift do
@@ -83,20 +90,20 @@ unextend context =
         , Context.boundVars = boundVars
         }
     _ ->
-      panic "Unification.Indices.unextend"
+      panic "Equation.unextend"
 
-contextual1 :: (Context v -> a -> M b) -> a -> Unify v b
+contextual1 :: (Context v -> a -> M b) -> a -> Equate v b
 contextual1 f x = do
   c <- gets (.context)
   lift $ f c x
 
-contextual2 :: (Context v -> a -> b -> M c) -> a -> b -> Unify v c
+contextual2 :: (Context v -> a -> b -> M c) -> a -> b -> Equate v c
 contextual2 f x y = do
   c <- gets (.context)
   lift $ f c x y
 
-unifyM :: Flexibility -> Domain.Value -> Domain.Value -> Unify v ()
-unifyM flexibility value1 value2 = do
+equateM :: Flexibility -> Domain.Value -> Domain.Value -> Equate v ()
+equateM flexibility value1 value2 = do
   value1' <- contextual1 Context.forceHeadGlue value1
   value2' <- contextual1 Context.forceHeadGlue value2
   case (value1', value2') of
@@ -104,11 +111,11 @@ unifyM flexibility value1 value2 = do
     (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
       | head1 == head2 -> do
           let flexibility' = max (Domain.headFlexibility head1) flexibility
-          unifySpines flexibility' spine1 spine2
+          equateSpines flexibility' spine1 spine2
     (Domain.Con con1 args1, Domain.Con con2 args2)
       | con1 == con2
       , map fst args1 == map fst args2 ->
-          Tsil.zipWithM_ (unifyM flexibility `on` snd) args1 args2
+          Tsil.zipWithM_ (equateM flexibility `on` snd) args1 args2
       | otherwise ->
           throwIO Nope
     (Domain.Lit lit1, Domain.Lit lit2)
@@ -118,34 +125,40 @@ unifyM flexibility value1 value2 = do
           throwIO Nope
     (Domain.Glued head1 spine1 value1'', Domain.Glued head2 spine2 value2'')
       | head1 == head2 ->
-          unifySpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
-            unifyM flexibility value1'' value2''
+          equateSpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
+            equateM flexibility value1'' value2''
+      | otherwise -> do
+          ordering <- lift $ compareHeadDepths head1 head2
+          case ordering of
+            LT -> equateM flexibility value1' value2''
+            GT -> equateM flexibility value1'' value2'
+            EQ -> equateM flexibility value1'' value2''
     (Domain.Glued _ _ value1'', _) ->
-      unifyM flexibility value1'' value2'
+      equateM flexibility value1'' value2'
     (_, Domain.Glued _ _ value2'') ->
-      unifyM flexibility value1' value2''
+      equateM flexibility value1' value2''
     (Domain.Lam bindings1 type1 plicity1 closure1, Domain.Lam _ type2 plicity2 closure2)
       | plicity1 == plicity2 ->
-          unifyAbstraction (Bindings.toName bindings1) type1 closure1 type2 closure2
+          equateAbstraction (Bindings.toName bindings1) type1 closure1 type2 closure2
     (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Pi _ domain2 plicity2 targetClosure2)
       | plicity1 == plicity2 ->
-          unifyAbstraction (Binding.toName binding1) domain1 targetClosure1 domain2 targetClosure2
+          equateAbstraction (Binding.toName binding1) domain1 targetClosure1 domain2 targetClosure2
     (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Fun domain2 plicity2 target2)
       | plicity1 == plicity2 -> do
-          unifyM flexibility domain2 domain1
+          equateM flexibility domain2 domain1
           extend (Binding.toName binding1) domain1 \var -> do
             target1 <- lift $ Evaluation.evaluateClosure targetClosure1 $ Domain.var var
-            unifyM flexibility target1 target2
+            equateM flexibility target1 target2
     (Domain.Fun domain1 plicity1 target1, Domain.Pi binding2 domain2 plicity2 targetClosure2)
       | plicity1 == plicity2 -> do
-          unifyM flexibility domain2 domain1
+          equateM flexibility domain2 domain1
           extend (Binding.toName binding2) domain2 \var -> do
             target2 <- lift $ Evaluation.evaluateClosure targetClosure2 $ Domain.var var
-            unifyM flexibility target1 target2
+            equateM flexibility target1 target2
     (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
       | plicity1 == plicity2 -> do
-          unifyM flexibility domain2 domain1
-          unifyM flexibility target1 target2
+          equateM flexibility domain2 domain1
+          equateM flexibility target1 target2
 
     -- Eta expand
     (Domain.Lam bindings1 type1 plicity1 closure1, v2) ->
@@ -153,140 +166,63 @@ unifyM flexibility value1 value2 = do
         let varValue = Domain.var var
         body1 <- lift $ Evaluation.evaluateClosure closure1 varValue
         body2 <- lift $ Evaluation.apply v2 plicity1 varValue
-        unifyM flexibility body1 body2
+        equateM flexibility body1 body2
     (v1, Domain.Lam bindings2 type2 plicity2 closure2) ->
       extend (Bindings.toName bindings2) type2 \var -> do
         let varValue = Domain.var var
         body1 <- lift $ Evaluation.apply v1 plicity2 varValue
         body2 <- lift $ Evaluation.evaluateClosure closure2 varValue
-        unifyM flexibility body1 body2
+        equateM flexibility body1 body2
 
     -- Vars
-    (Domain.Neutral (Domain.Var var1) Domain.Empty, _)
+    (Domain.Neutral head1 spine1, _)
       | Flexibility.Rigid <- flexibility ->
-          solve var1 value2'
-    (_, Domain.Neutral (Domain.Var var2) Domain.Empty)
+          solve head1 spine1 value2'
+    (_, Domain.Neutral head2 spine2)
       | Flexibility.Rigid <- flexibility ->
-          solve var2 value1'
+          solve head2 spine2 value1'
     _ ->
       throwIO Dunno
   where
-    unifyAbstraction name type1 closure1 type2 closure2 = do
-      unifyM flexibility type1 type2
+    equateAbstraction name type1 closure1 type2 closure2 = do
+      equateM flexibility type1 type2
 
       extend name type1 \var -> do
         let varValue = Domain.var var
         body1 <- lift $ Evaluation.evaluateClosure closure1 varValue
         body2 <- lift $ Evaluation.evaluateClosure closure2 varValue
-        unifyM flexibility body1 body2
+        equateM flexibility body1 body2
 
-    solve var value = do
-      touchable <- isTouchable var
+    solve head_ spine value = do
+      touchable <- isTouchable head_
       if touchable
         then do
-          occurs var Flexibility.Rigid value
-          context' <- contextual2 Context.define var value
+          occurs head_ Flexibility.Rigid value
+          spine' <- touchableSpine spine
+          context' <- contextual2 Context.define head_ spine' value
           modify \st -> st {context = context'}
         else throwIO Dunno
 
-unifySpines
+equateSpines
   :: Flexibility
   -> Domain.Spine
   -> Domain.Spine
-  -> Unify v ()
-unifySpines flexibility spine1 spine2 =
+  -> Equate v ()
+equateSpines flexibility spine1 spine2 =
   case (spine1, spine2) of
     (Domain.Empty, Domain.Empty) -> pure ()
-    (spine1' Domain.:> elimination1, spine2' Domain.:> elimination2) -> do
-      unifySpines flexibility spine1' spine2'
-      case (elimination1, elimination2) of
-        (Domain.App plicity1 arg1, Domain.App plicity2 arg2)
-          | plicity1 == plicity2 -> unifyM flexibility arg1 arg2
-        (Domain.Case branches1, Domain.Case branches2) ->
-          unifyBranches flexibility branches1 branches2
-        _ ->
-          throwIO Dunno
+    (Domain.App plicity1 arg1 Domain.:< spine1', Domain.App plicity2 arg2 Domain.:< spine2')
+      | plicity1 == plicity2 -> do
+          equateM flexibility arg1 arg2
+          equateSpines flexibility spine1' spine2'
     _ ->
       throwIO Dunno
 
-unifyBranches :: Flexibility -> Domain.Branches -> Domain.Branches -> Unify v ()
-unifyBranches
-  flexibility
-  (Domain.Branches outerEnv1 branches1 defaultBranch1)
-  (Domain.Branches outerEnv2 branches2 defaultBranch2) =
-    case (branches1, branches2) of
-      (Syntax.ConstructorBranches conTypeName1 conBranches1, Syntax.ConstructorBranches conTypeName2 conBranches2)
-        | conTypeName1 == conTypeName2 ->
-            unifyMaps conBranches1 conBranches2
-      (Syntax.LiteralBranches litBranches1, Syntax.LiteralBranches litBranches2) ->
-        unifyMaps (second Telescope.Empty <$> litBranches1) (second Telescope.Empty <$> litBranches2)
-      _ ->
-        throwIO Dunno
-    where
-      unifyMaps brs1 brs2 = do
-        let branches = OrderedHashMap.intersectionWith (,) brs1 brs2
-            extras1 = OrderedHashMap.difference brs1 branches
-            extras2 = OrderedHashMap.difference brs2 branches
-
-        when
-          ( (not (OrderedHashMap.null extras1) && isNothing defaultBranch2)
-              || (not (OrderedHashMap.null extras2) && isNothing defaultBranch1)
-          )
-          $ throwIO Dunno
-
-        defaultBranch1' <- forM defaultBranch1 $ lift . Evaluation.evaluate outerEnv1
-        defaultBranch2' <- forM defaultBranch2 $ lift . Evaluation.evaluate outerEnv2
-
-        forM_ defaultBranch2' \branch2 ->
-          forM_ extras1 \(_, tele1) ->
-            withInstantiatedTele outerEnv1 tele1 \branch1 -> do
-              unifyM flexibility branch1 branch2
-
-        forM_ defaultBranch1' \branch1 ->
-          forM_ extras2 \(_, tele2) ->
-            withInstantiatedTele outerEnv2 tele2 \branch2 ->
-              unifyM flexibility branch1 branch2
-
-        forM_ branches \((_, tele1), (_, tele2)) ->
-          unifyTele outerEnv1 outerEnv2 tele1 tele2
-
-        case (defaultBranch1', defaultBranch2') of
-          (Just branch1, Just branch2) ->
-            unifyM flexibility branch1 branch2
-          _ ->
-            pure ()
-
-      unifyTele
-        :: Domain.Environment v1
-        -> Domain.Environment v2
-        -> Telescope Bindings Syntax.Type Syntax.Term v1
-        -> Telescope Bindings Syntax.Type Syntax.Term v2
-        -> Unify v ()
-      unifyTele env1 env2 tele1 tele2 =
-        case (tele1, tele2) of
-          (Telescope.Extend bindings1 type1 plicity1 tele1', Telescope.Extend _bindings2 type2 plicity2 tele2')
-            | plicity1 == plicity2 -> do
-                type1' <- lift $ Evaluation.evaluate env1 type1
-                type2' <- lift $ Evaluation.evaluate env2 type2
-                unifyM flexibility type1' type2'
-                extend (Bindings.toName bindings1) type1' \var ->
-                  unifyTele
-                    (Environment.extendVar env1 var)
-                    (Environment.extendVar env2 var)
-                    tele1'
-                    tele2'
-          (Telescope.Empty body1, Telescope.Empty body2) -> do
-            body1' <- lift $ Evaluation.evaluate env1 body1
-            body2' <- lift $ Evaluation.evaluate env2 body2
-            unifyM flexibility body1' body2'
-          _ ->
-            panic "unifyTele"
-
 withInstantiatedTele
   :: Domain.Environment v1
   -> Telescope Bindings Syntax.Type Syntax.Term v1
-  -> (forall v'. Domain.Value -> Unify v' k)
-  -> Unify v k
+  -> (forall v'. Domain.Value -> Equate v' k)
+  -> Equate v k
 withInstantiatedTele env tele k =
   case tele of
     Telescope.Empty body -> do
@@ -297,7 +233,7 @@ withInstantiatedTele env tele k =
       extend (Bindings.toName bindings) type' \var ->
         withInstantiatedTele (Environment.extendVar env var) tele' k
 
-occurs :: Var -> Flexibility -> Domain.Value -> Unify v ()
+occurs :: Domain.Head -> Flexibility -> Domain.Value -> Equate v ()
 occurs occ flexibility value = do
   value' <- contextual1 Context.forceHeadGlue value
   case value' of
@@ -310,12 +246,12 @@ occurs occ flexibility value = do
       pure ()
     Domain.Glued (Domain.Var _) _ value'' ->
       occurs occ flexibility value''
-    Domain.Lazy lazyValue -> do
-      value'' <- lift $ force lazyValue
-      occurs occ flexibility value''
     Domain.Glued hd spine value'' ->
       occurs occ Flexibility.Flexible (Domain.Neutral hd spine) `catch` \(_ :: Error) ->
         occurs occ flexibility value''
+    Domain.Lazy lazyValue -> do
+      value'' <- lift $ force lazyValue
+      occurs occ flexibility value''
     Domain.Lam bindings type_ _ closure ->
       occursAbstraction (Bindings.toName bindings) type_ closure
     Domain.Pi binding domain _ targetClosure ->
@@ -331,38 +267,29 @@ occurs occ flexibility value = do
         body <- lift $ Evaluation.evaluateClosure closure varValue
         occurs occ flexibility body
 
-occursHead :: Var -> Flexibility -> Domain.Head -> Unify v ()
-occursHead occ flexibility hd =
-  case hd of
-    Domain.Var var
-      | var == occ ->
-          throwIO case flexibility of
-            Flexibility.Rigid -> Nope
-            Flexibility.Flexible -> Dunno
-      | otherwise -> do
-          touchable <- isTouchable var
+occursHead :: Domain.Head -> Flexibility -> Domain.Head -> Equate v ()
+occursHead occ flexibility hd
+  | hd == occ = throwIO case flexibility of
+      Flexibility.Rigid -> Nope
+      Flexibility.Flexible -> Dunno
+  | otherwise =
+      case hd of
+        Domain.Var var -> do
+          touchable <- isTouchableVar var
           unless touchable $
             throwIO case flexibility of
               Flexibility.Rigid -> Nope
               Flexibility.Flexible -> Dunno
-    Domain.Global _ -> pure ()
-    Domain.Meta _ -> pure ()
+        Domain.Global _ -> pure ()
+        Domain.Meta _ -> pure ()
 
-occursElimination
-  :: Var
-  -> Flexibility
-  -> Domain.Elimination
-  -> Unify v ()
+occursElimination :: Domain.Head -> Flexibility -> Domain.Elimination -> Equate v ()
 occursElimination occ flexibility elimination =
   case elimination of
     Domain.App _plicity arg -> occurs occ flexibility arg
     Domain.Case branches -> occursBranches occ flexibility branches
 
-occursBranches
-  :: Var
-  -> Flexibility
-  -> Domain.Branches
-  -> Unify v ()
+occursBranches :: Domain.Head -> Flexibility -> Domain.Branches -> Equate v ()
 occursBranches occ flexibility (Domain.Branches outerEnv branches defaultBranch) = do
   case branches of
     Syntax.ConstructorBranches _ constructorBranches ->
@@ -377,7 +304,7 @@ occursBranches occ flexibility (Domain.Branches outerEnv branches defaultBranch)
     occursTele
       :: Domain.Environment v1
       -> Telescope Bindings Syntax.Type Syntax.Term v1
-      -> Unify v ()
+      -> Equate v ()
     occursTele env tele =
       case tele of
         Telescope.Extend bindings type_ _plicity tele' -> do
@@ -390,3 +317,89 @@ occursBranches occ flexibility (Domain.Branches outerEnv branches defaultBranch)
         Telescope.Empty body -> do
           body' <- lift $ Evaluation.evaluate env body
           occurs occ flexibility body'
+
+touchableValue :: Index (Succ v) -> Domain.Value -> Equate v Domain.Value
+touchableValue locals value = do
+  value' <- contextual1 Context.forceHeadGlue value
+  case value' of
+    Domain.Neutral hd spine -> do
+      touchableHead locals hd
+      Domain.mapM_ (touchableElimination locals) spine
+    Domain.Con _ args ->
+      mapM_ (touchableValue locals . snd) args
+    Domain.Lit _ ->
+      pure ()
+    Domain.Glued (Domain.Var _) _ value'' ->
+      touchableValue locals value''
+    Domain.Glued hd spine value'' ->
+      touchableValue locals (Domain.Neutral hd spine) `catch` \(_ :: Error) ->
+        touchableValue locals value''
+    Domain.Lazy lazyValue -> do
+      value'' <- lift $ force lazyValue
+      touchableValue locals value''
+    Domain.Lam bindings type_ _ closure ->
+      occursAbstraction (Bindings.toName bindings) type_ closure
+    Domain.Pi binding domain _ targetClosure ->
+      occursAbstraction (Binding.toName binding) domain targetClosure
+    Domain.Fun domain _ target -> do
+      touchableValue locals domain
+      touchableValue locals target
+  where
+    occursAbstraction name type_ closure = do
+      touchableValue locals type_
+      extend name type_ \var -> do
+        let varValue = Domain.var var
+        body <- lift $ Evaluation.evaluateClosure closure varValue
+        touchableValue locals body
+
+touchableHead :: Index (Succ v) -> Domain.Head -> Equate v Domain.Head
+touchableHead locals hd =
+  case hd of
+    Domain.Var var -> do
+      context <- gets (.context)
+      case Context.lookupVarIndex var context of
+        Just varIndex
+          | Index.Succ varIndex <= locals -> pure hd
+          | otherwise -> do
+              touchable <- isTouchableVar var
+              unless touchable $ throwIO Dunno
+        Nothing -> throwIO Dunno
+    Domain.Global _ -> pure hd
+    Domain.Meta _ -> throwIO Dunno
+
+touchableElimination :: Index (Succ v) -> Domain.Elimination -> Equate v Domain.Elimination
+touchableElimination locals elimination =
+  case elimination of
+    Domain.App _plicity arg -> touchableValue locals arg
+    Domain.Case branches -> touchableBranches locals branches
+
+touchableBranches :: Index (Succ v) -> Domain.Branches -> Equate v Domain.Branches
+touchableBranches locals (Domain.Branches outerEnv branches defaultBranch) = do
+  case branches of
+    Syntax.ConstructorBranches _ constructorBranches ->
+      forM_ constructorBranches $ mapM_ $ touchableTele outerEnv
+    Syntax.LiteralBranches literalBranches ->
+      forM_ literalBranches $
+        mapM_ \branch ->
+          touchableTele locals outerEnv $ Telescope.Empty branch
+  forM_ defaultBranch \branch ->
+    touchableTele outerEnv locals $ Telescope.Empty branch
+  where
+    touchableTele
+      :: Index (Succ v)
+      -> Domain.Environment v1
+      -> Telescope Bindings Syntax.Type Syntax.Term v1
+      -> Equate v (Telescope Bindings Syntax.Type Syntax.Term v1)
+    touchableTele locals' env tele =
+      case tele of
+        Telescope.Extend bindings type_ _plicity tele' -> do
+          type' <- lift $ Evaluation.evaluate env type_
+          touchableValue locals type'
+          extend (Bindings.toName bindings) type' \var ->
+            touchableTele
+              (Index.Succ locals')
+              (Environment.extendVar env var)
+              tele'
+        Telescope.Empty body -> do
+          body' <- lift $ Evaluation.evaluate env body
+          touchableValue locals body'
diff --git a/src/Elaboration/Unification.hs b/src/Elaboration/Unification.hs
index 9ea9ed9..a874361 100644
--- a/src/Elaboration/Unification.hs
+++ b/src/Elaboration/Unification.hs
@@ -26,6 +26,7 @@ import qualified Data.Tsil as Tsil
 import {-# SOURCE #-} qualified Elaboration
 import Elaboration.Context (Context)
 import qualified Elaboration.Context as Context
+import Elaboration.Depth (compareHeadDepths)
 import qualified Elaboration.Meta as Meta
 import Environment (Environment (Environment))
 import qualified Environment
@@ -312,24 +313,6 @@ unify context flexibility value1 value2 = do
     can'tUnify =
       throwIO $ Error.TypeMismatch mempty
 
--- | Try to find out which of two heads might refer to the other so we can
--- unfold glued values that are defined later first (see "depth" in
--- https://arxiv.org/pdf/1505.04324.pdf).
-compareHeadDepths :: Domain.Head -> Domain.Head -> M Ordering
-compareHeadDepths head1 head2 =
-  case (head1, head2) of
-    (Domain.Global global1, Domain.Global global2) -> do
-      global1DependsOn2 <- fetch $ Query.TransitiveDependencies global2 $ Mapped.Query global1
-      global2DependsOn1 <- fetch $ Query.TransitiveDependencies global1 $ Mapped.Query global2
-      pure case (global1DependsOn2, global2DependsOn1) of
-        (Just _, Nothing) -> GT
-        (Nothing, Just _) -> LT
-        _ -> EQ
-    (_, Domain.Global _) -> pure LT
-    (Domain.Global _, _) -> pure GT
-    (Domain.Var v1, Domain.Var v2) -> pure $ compare v1 v2
-    _ -> pure EQ
-
 unifySpines :: Context v -> Flexibility -> Domain.Spine -> Domain.Spine -> M ()
 unifySpines context flexibility spine1 spine2 =
   case (spine1, spine2) of
@@ -350,7 +333,8 @@ unifySpines context flexibility spine1 spine2 =
 
 equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool
 equalSpines context spine1 spine2 =
-  Context.try_ context $ unifySpines context Flexibility.Flexible spine1 spine2
+  (True <$ unifySpines context Flexibility.Flexible spine1 spine2)
+    `catch` \(_ :: Error) -> pure False
 
 unifyBranches
   :: Context v