diff --git a/src/Elaboration/Equation.hs b/src/Elaboration/Equation.hs
index 1285f1e..ebc3017 100644
--- a/src/Elaboration/Equation.hs
+++ b/src/Elaboration/Equation.hs
@@ -49,64 +49,67 @@ contextual1 f x = do
   lift $ f c x
 
 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
-    -- Same heads
-    (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
-      | head1 == head2 -> do
-          let flexibility' = max (Domain.headFlexibility head1) flexibility
-          equateSpines flexibility' spine1 spine2
-    (Domain.Con con1 args1, Domain.Con con2 args2)
-      | con1 == con2
-      , map fst args1 == map fst args2 ->
-          Tsil.zipWithM_ (equateM flexibility `on` snd) args1 args2
-      | otherwise ->
-          throwIO Nope
-    (Domain.Lit lit1, Domain.Lit lit2)
-      | lit1 == lit2 ->
-          pure ()
-      | otherwise ->
-          throwIO Nope
-    (Domain.Glued head1 spine1 value1'', Domain.Glued head2 spine2 value2'')
-      | head1 == head2 ->
-          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'', _) ->
-      equateM flexibility value1'' value2'
-    (_, Domain.Glued _ _ value2'') ->
-      equateM flexibility value1' value2''
-    (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
-      | plicity1 == plicity2 -> do
-          equateM flexibility domain2 domain1
-          equateM flexibility target1 target2
+equateM flexibility unforcedValue1 unforcedValue2 = go unforcedValue1 unforcedValue2
+  where
+    go value1 value2 = do
+      value1' <- contextual1 Context.forceHeadGlue value1
+      value2' <- contextual1 Context.forceHeadGlue value2
+      case (value1', value2') of
+        -- Glue
+        (Domain.Glued head1 spine1 value1'', Domain.Glued head2 spine2 value2'')
+          | head1 == head2 ->
+              equateSpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
+                go value1'' value2''
+          | otherwise -> do
+              ordering <- lift $ compareHeadDepths head1 head2
+              case ordering of
+                LT -> go value1' value2''
+                GT -> go value1'' value2'
+                EQ -> go value1'' value2''
+        (Domain.Glued _ _ value1'', _) ->
+          go value1'' value2'
+        (_, Domain.Glued _ _ value2'') ->
+          go value1' value2''
+        -- Same heads
+        (Domain.Neutral head1 spine1, Domain.Neutral head2 spine2)
+          | head1 == head2 -> do
+              let flexibility' = max (Domain.headFlexibility head1) flexibility
+              equateSpines flexibility' spine1 spine2
+        (Domain.Con con1 args1, Domain.Con con2 args2)
+          | con1 == con2
+          , map fst args1 == map fst args2 ->
+              Tsil.zipWithM_ (equateM flexibility `on` snd) args1 args2
+          | otherwise ->
+              throwIO Nope
+        (Domain.Lit lit1, Domain.Lit lit2)
+          | lit1 == lit2 ->
+              pure ()
+          | otherwise ->
+              throwIO Nope
+        (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
+          | plicity1 == plicity2 -> do
+              equateM flexibility domain2 domain1
+              equateM flexibility target1 target2
 
-    -- Neutrals
-    (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
-      | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
-      , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility
-      , (fst <$> args1) == (fst <$> args2) -> do
-          -- TODO: check both directions?
-          ordering <- lift $ compareHeadDepths head1 head2
-          case ordering of
-            LT -> solve head2 args2 value1'
-            GT -> solve head1 args1 value2'
-            EQ -> solve head2 args2 value1'
-    (Domain.Neutral head1 (Domain.Apps args1), _)
-      | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
-          solve head1 args1 value2
-    (_, Domain.Neutral head2 (Domain.Apps args2))
-      | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
-          solve head2 args2 value1
-    _ ->
-      throwIO Dunno
+        -- Neutrals
+        (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
+          | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility
+          , Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility
+          , (fst <$> args1) == (fst <$> args2) -> do
+              -- TODO: check both directions?
+              ordering <- lift $ compareHeadDepths head1 head2
+              case ordering of
+                LT -> solve head2 args2 unforcedValue1
+                GT -> solve head1 args1 unforcedValue2
+                EQ -> solve head2 args2 unforcedValue1
+        (Domain.Neutral head1 (Domain.Apps args1), _)
+          | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
+              solve head1 args1 unforcedValue2
+        (_, Domain.Neutral head2 (Domain.Apps args2))
+          | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
+              solve head2 args2 unforcedValue1
+        _ ->
+          throwIO Dunno
 
 solve :: Domain.Head -> Domain.Args -> Domain.Value -> Equate v ()
 solve head_ args value = do
diff --git a/src/Elaboration/Unification.hs b/src/Elaboration/Unification.hs
index d6e3557..ad5c5a5 100644
--- a/src/Elaboration/Unification.hs
+++ b/src/Elaboration/Unification.hs
@@ -68,175 +68,177 @@ tryUnifyD context value1 value2 = do
       else const $ Builtin.Unknown value2
 
 unify :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M ()
-unify context flexibility value1 value2 = do
-  value1' <- Context.forceHeadGlue context value1
-  value2' <- Context.forceHeadGlue context value2
-  -- putText "unifying"
-  -- Context.dumpValue context value1'
-  -- Context.dumpValue context value2'
-  catchAndAdd case (value1', value2') of
-    -- Both metas
-    (Domain.Neutral (Domain.Meta metaIndex1) (Domain.Apps args1), Domain.Neutral (Domain.Meta metaIndex2) (Domain.Apps args2))
-      | Flexibility.Rigid <- flexibility -> do
-          args1' <- mapM (mapM $ Context.forceHead context) args1
-          args2' <- mapM (mapM $ Context.forceHead context) args2
-          if metaIndex1 == metaIndex2 && map fst args1 == map fst args2
-            then do
-              -- Intersection: If the same metavar is applied to two different lists of unknown
-              -- variables its solution must not mention any variables at
-              -- positions where the lists differ.
-              let keep =
-                    mzipWith (shouldKeepMetaArgument `on` snd) args1' args2'
-              if and keep
-                then sequence_ $ Seq.zipWith (unify context flexibility `on` snd) args1 args2
-                else pruneMeta context metaIndex1 keep
-            else do
-              let maybeUniqueVars1 = do
-                    vars1 <- mapM (mapM Domain.singleVarView) args1'
-                    guard $ unique $ snd <$> vars1
-                    pure vars1
-
-                  maybeUniqueVars2 = do
-                    vars2 <- mapM (mapM Domain.singleVarView) args2'
-                    guard $ unique $ snd <$> vars2
-                    pure vars2
-
-              case (maybeUniqueVars1, maybeUniqueVars2) of
-                (Just vars1, Just vars2)
-                  | length vars1 > length vars2 ->
-                      solve context metaIndex1 vars1 value2
-                  | otherwise ->
-                      solve context metaIndex2 vars2 value1
-                (Just vars1, _) ->
-                  solve context metaIndex1 vars1 value2
-                (_, Just vars2) ->
-                  solve context metaIndex2 vars2 value1
+unify context flexibility unforcedValue1 unforcedValue2 = catchAndAdd $ go unforcedValue1 unforcedValue2
+  where
+    go value1 value2 = do
+      value1' <- Context.forceHeadGlue context value1
+      value2' <- Context.forceHeadGlue context value2
+      -- putText "unifying"
+      -- Context.dumpValue context value1'
+      -- Context.dumpValue context value2'
+      case (value1', value2') of
+        -- Glued values
+        (Domain.Glued head1 (Domain.Apps args1) value1'', Domain.Glued head2 (Domain.Apps args2) value2'')
+          | head1 == head2
+          , (fst <$> args1) == (fst <$> args2) ->
+              sequence_ (Seq.zipWith (unify context Flexibility.Flexible `on` snd) args1 args2) `catch` \(_ :: Error.Elaboration) ->
+                unify context flexibility value1'' value2''
+          | otherwise -> do
+              ordering <- compareHeadDepths head1 head2
+              case ordering of
+                LT -> go value1' value2''
+                GT -> go value1'' value2'
+                EQ -> go value1'' value2''
+        (Domain.Glued _ _ value1'', _) ->
+          go value1'' value2'
+        (_, Domain.Glued _ _ value2'') ->
+          go value1' value2''
+        -- Both metas
+        (Domain.Neutral (Domain.Meta metaIndex1) (Domain.Apps args1), Domain.Neutral (Domain.Meta metaIndex2) (Domain.Apps args2))
+          | Flexibility.Rigid <- flexibility -> do
+              args1' <- mapM (mapM $ Context.forceHead context) args1
+              args2' <- mapM (mapM $ Context.forceHead context) args2
+              if metaIndex1 == metaIndex2 && map fst args1 == map fst args2
+                then do
+                  -- Intersection: If the same metavar is applied to two different lists of unknown
+                  -- variables its solution must not mention any variables at
+                  -- positions where the lists differ.
+                  let keep =
+                        mzipWith (shouldKeepMetaArgument `on` snd) args1' args2'
+                  if and keep
+                    then sequence_ $ Seq.zipWith (unify context flexibility `on` snd) args1 args2
+                    else pruneMeta context metaIndex1 keep
+                else do
+                  let maybeUniqueVars1 = do
+                        vars1 <- mapM (mapM Domain.singleVarView) args1'
+                        guard $ unique $ snd <$> vars1
+                        pure vars1
+
+                      maybeUniqueVars2 = do
+                        vars2 <- mapM (mapM Domain.singleVarView) args2'
+                        guard $ unique $ snd <$> vars2
+                        pure vars2
+
+                  case (maybeUniqueVars1, maybeUniqueVars2) of
+                    (Just vars1, Just vars2)
+                      | length vars1 > length vars2 ->
+                          solve context metaIndex1 vars1 unforcedValue2
+                      | otherwise ->
+                          solve context metaIndex2 vars2 unforcedValue1
+                    (Just vars1, _) ->
+                      solve context metaIndex1 vars1 unforcedValue2
+                    (_, Just vars2) ->
+                      solve context metaIndex2 vars2 unforcedValue1
+                    _ ->
+                      can'tUnify
+
+        -- Same heads
+        (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
+          | head1 == head2
+          , (fst <$> args1) == (fst <$> args2) -> do
+              let flexibility' =
+                    max (Domain.headFlexibility head1) flexibility
+              sequence_ $ Seq.zipWith (unify context flexibility' `on` snd) args1 args2
+        (Domain.Con con1 args1, Domain.Con con2 args2)
+          | con1 == con2
+          , map fst args1 == map fst args2 ->
+              Tsil.zipWithM_ (unify context flexibility `on` snd) args1 args2
+          | otherwise ->
+              can'tUnify
+        (Domain.Lit lit1, Domain.Lit lit2)
+          | lit1 == lit2 ->
+              pure ()
+          | otherwise ->
+              can'tUnify
+        (Domain.Lam bindings1 type1 plicity1 closure1, Domain.Lam _ type2 plicity2 closure2)
+          | plicity1 == plicity2 ->
+              unifyAbstraction (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
+        (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Fun domain2 plicity2 target2)
+          | plicity1 == plicity2 -> do
+              unify context flexibility domain2 domain1
+              (context', var) <- Context.extend context (Binding.toName binding1) domain1
+              target1 <- Evaluation.evaluateClosure targetClosure1 $ Domain.var var
+              unify context' flexibility target1 target2
+        (Domain.Fun domain1 plicity1 target1, Domain.Pi binding2 domain2 plicity2 targetClosure2)
+          | plicity1 == plicity2 -> do
+              unify context flexibility domain2 domain1
+              (context', var) <- Context.extend context (Binding.toName binding2) domain2
+              target2 <- Evaluation.evaluateClosure targetClosure2 $ Domain.var var
+              unify context' flexibility target1 target2
+        (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
+          | plicity1 == plicity2 -> do
+              unify context flexibility domain2 domain1
+              unify context flexibility target1 target2
+
+        -- Eta expand
+        (Domain.Lam bindings1 type1 plicity1 closure1, v2) -> do
+          (context', var) <- Context.extend context (Bindings.toName bindings1) type1
+          let varValue =
+                Domain.var var
+
+          body1 <- Evaluation.evaluateClosure closure1 varValue
+          body2 <- Evaluation.apply v2 plicity1 varValue
+
+          unify context' flexibility body1 body2
+        (v1, Domain.Lam bindings2 type2 plicity2 closure2) -> do
+          (context', var) <- Context.extend context (Bindings.toName bindings2) type2
+          let varValue =
+                Domain.var var
+
+          body1 <- Evaluation.apply v1 plicity2 varValue
+          body2 <- Evaluation.evaluateClosure closure2 varValue
+
+          unify context' flexibility body1 body2
+
+        -- Metas
+        (Domain.Neutral (Domain.Meta metaIndex1) (Domain.Apps args1), _)
+          | Flexibility.Rigid <- flexibility -> do
+              args1' <- mapM (mapM $ Context.forceHead context) args1
+              case traverse (traverse Domain.singleVarView) args1' of
+                Just vars1
+                  | unique $ snd <$> vars1 ->
+                      solve context metaIndex1 vars1 unforcedValue2
+                _ ->
+                  can'tUnify
+        (_, Domain.Neutral (Domain.Meta metaIndex2) (Domain.Apps args2))
+          | Flexibility.Rigid <- flexibility -> do
+              args2' <- mapM (mapM $ Context.forceHead context) args2
+              case traverse (traverse Domain.singleVarView) args2' of
+                Just vars2
+                  | unique $ snd <$> vars2 ->
+                      solve context metaIndex2 vars2 unforcedValue1
                 _ ->
                   can'tUnify
 
-    -- Same heads
-    (Domain.Neutral head1 (Domain.Apps args1), Domain.Neutral head2 (Domain.Apps args2))
-      | head1 == head2
-      , (fst <$> args1) == (fst <$> args2) -> do
-          let flexibility' =
-                max (Domain.headFlexibility head1) flexibility
-          sequence_ $ Seq.zipWith (unify context flexibility' `on` snd) args1 args2
-    (Domain.Con con1 args1, Domain.Con con2 args2)
-      | con1 == con2
-      , map fst args1 == map fst args2 ->
-          Tsil.zipWithM_ (unify context flexibility `on` snd) args1 args2
-      | otherwise ->
-          can'tUnify
-    (Domain.Lit lit1, Domain.Lit lit2)
-      | lit1 == lit2 ->
+        -- Case inversion
+        (Domain.Neutral (Domain.Meta meta) (spine@(Domain.Apps args) Domain.:> Domain.Case branches), _)
+          | Flexibility.Rigid <- flexibility -> do
+              matches <- potentiallyMatchingBranches context value2' branches
+              invertCase meta spine args matches
+        (_, Domain.Neutral (Domain.Meta meta) (spine@(Domain.Apps args) Domain.:> Domain.Case branches))
+          | Flexibility.Rigid <- flexibility -> do
+              matches <- potentiallyMatchingBranches context value1' branches
+              invertCase meta spine args matches
+        (Domain.Neutral head1 spine1@(Domain.Spine args1 ((branches1, _) Seq.:<| _)), Domain.Neutral head2 spine2)
+          | head1 == head2 ->
+              unifySpines context Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error.Elaboration) ->
+                withBranches context head1 args1 branches1 $ \context' -> unify context' flexibility value1' value2
+        (Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _)), _) ->
+          withBranches context head args branches $ \context' -> unify context' flexibility value1' value2
+        (_, Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _))) ->
+          withBranches context head args branches $ \context' -> unify context' flexibility value1 value2'
+        -- Failure terms mean that there has been an earlier error that's already
+        -- been reported, so let's not trigger more errors from them.
+        (Domain.Neutral (Domain.Global Builtin.UnknownName) _, _) ->
           pure ()
-      | otherwise ->
+        (_, Domain.Neutral (Domain.Global Builtin.UnknownName) _) ->
+          pure ()
+        _ ->
           can'tUnify
-    (Domain.Lam bindings1 type1 plicity1 closure1, Domain.Lam _ type2 plicity2 closure2)
-      | plicity1 == plicity2 ->
-          unifyAbstraction (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
-    (Domain.Pi binding1 domain1 plicity1 targetClosure1, Domain.Fun domain2 plicity2 target2)
-      | plicity1 == plicity2 -> do
-          unify context flexibility domain2 domain1
-          (context', var) <- Context.extend context (Binding.toName binding1) domain1
-          target1 <- Evaluation.evaluateClosure targetClosure1 $ Domain.var var
-          unify context' flexibility target1 target2
-    (Domain.Fun domain1 plicity1 target1, Domain.Pi binding2 domain2 plicity2 targetClosure2)
-      | plicity1 == plicity2 -> do
-          unify context flexibility domain2 domain1
-          (context', var) <- Context.extend context (Binding.toName binding2) domain2
-          target2 <- Evaluation.evaluateClosure targetClosure2 $ Domain.var var
-          unify context' flexibility target1 target2
-    (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
-      | plicity1 == plicity2 -> do
-          unify context flexibility domain2 domain1
-          unify context flexibility target1 target2
-
-    -- Eta expand
-    (Domain.Lam bindings1 type1 plicity1 closure1, v2) -> do
-      (context', var) <- Context.extend context (Bindings.toName bindings1) type1
-      let varValue =
-            Domain.var var
-
-      body1 <- Evaluation.evaluateClosure closure1 varValue
-      body2 <- Evaluation.apply v2 plicity1 varValue
 
-      unify context' flexibility body1 body2
-    (v1, Domain.Lam bindings2 type2 plicity2 closure2) -> do
-      (context', var) <- Context.extend context (Bindings.toName bindings2) type2
-      let varValue =
-            Domain.var var
-
-      body1 <- Evaluation.apply v1 plicity2 varValue
-      body2 <- Evaluation.evaluateClosure closure2 varValue
-
-      unify context' flexibility body1 body2
-
-    -- Glued values
-    (Domain.Glued head1 (Domain.Apps args1) value1'', Domain.Glued head2 (Domain.Apps args2) value2'')
-      | head1 == head2
-      , (fst <$> args1) == (fst <$> args2) ->
-          sequence_ (Seq.zipWith (unify context Flexibility.Flexible `on` snd) args1 args2) `catch` \(_ :: Error.Elaboration) ->
-            unify context flexibility value1'' value2''
-      | otherwise -> do
-          ordering <- compareHeadDepths head1 head2
-          case ordering of
-            LT -> unify context flexibility value1' value2''
-            GT -> unify context flexibility value1'' value2'
-            EQ -> unify context flexibility value1'' value2''
-    (Domain.Glued _ _ value1'', _) ->
-      unify context flexibility value1'' value2'
-    (_, Domain.Glued _ _ value2'') ->
-      unify context flexibility value1' value2''
-    -- Metas
-    (Domain.Neutral (Domain.Meta metaIndex1) (Domain.Apps args1), v2)
-      | Flexibility.Rigid <- flexibility -> do
-          args1' <- mapM (mapM $ Context.forceHead context) args1
-          case traverse (traverse Domain.singleVarView) args1' of
-            Just vars1
-              | unique $ snd <$> vars1 ->
-                  solve context metaIndex1 vars1 v2
-            _ ->
-              can'tUnify
-    (v1, Domain.Neutral (Domain.Meta metaIndex2) (Domain.Apps args2))
-      | Flexibility.Rigid <- flexibility -> do
-          args2' <- mapM (mapM $ Context.forceHead context) args2
-          case traverse (traverse Domain.singleVarView) args2' of
-            Just vars2
-              | unique $ snd <$> vars2 ->
-                  solve context metaIndex2 vars2 v1
-            _ ->
-              can'tUnify
-
-    -- Case inversion
-    (Domain.Neutral (Domain.Meta meta) (spine@(Domain.Apps args) Domain.:> Domain.Case branches), _)
-      | Flexibility.Rigid <- flexibility -> do
-          matches <- potentiallyMatchingBranches context value2' branches
-          invertCase meta spine args matches
-    (_, Domain.Neutral (Domain.Meta meta) (spine@(Domain.Apps args) Domain.:> Domain.Case branches))
-      | Flexibility.Rigid <- flexibility -> do
-          matches <- potentiallyMatchingBranches context value1' branches
-          invertCase meta spine args matches
-    (Domain.Neutral head1 spine1@(Domain.Spine args1 ((branches1, _) Seq.:<| _)), Domain.Neutral head2 spine2)
-      | head1 == head2 ->
-          unifySpines context Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error.Elaboration) ->
-            withBranches context head1 args1 branches1 $ \context' -> unify context' flexibility value1' value2
-    (Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _)), _) ->
-      withBranches context head args branches $ \context' -> unify context' flexibility value1' value2
-    (_, Domain.Neutral head (Domain.Spine args ((branches, _) Seq.:<| _))) ->
-      withBranches context head args branches $ \context' -> unify context' flexibility value1 value2'
-    -- Failure terms mean that there has been an earlier error that's already
-    -- been reported, so let's not trigger more errors from them.
-    (Domain.Neutral (Domain.Global Builtin.UnknownName) _, _) ->
-      pure ()
-    (_, Domain.Neutral (Domain.Global Builtin.UnknownName) _) ->
-      pure ()
-    _ ->
-      can'tUnify
-  where
     unifyAbstraction name type1 closure1 type2 closure2 = do
       unify context flexibility type1 type2
 
@@ -254,10 +256,10 @@ unify context flexibility value1 value2 = do
           metaType <- instantiatedMetaType context meta args
           appliedConstr <- fullyApplyToMetas context constr metaType
           unify context flexibility (Domain.Neutral (Domain.Meta meta) spine) appliedConstr
-          unify context flexibility value1 value2
+          go unforcedValue1 unforcedValue2
         [Just (Right lit)] -> do
           unify context flexibility (Domain.Neutral (Domain.Meta meta) spine) $ Domain.Lit lit
-          unify context flexibility value1 value2
+          go unforcedValue1 unforcedValue2
         _ ->
           can'tUnify
 
@@ -267,8 +269,8 @@ unify context flexibility value1 value2 = do
           m `catch` \err ->
             case err of
               Error.TypeMismatch stack -> do
-                term1 <- Elaboration.readback context value1
-                term2 <- Elaboration.readback context value2
+                term1 <- Elaboration.readback context unforcedValue1
+                term2 <- Elaboration.readback context unforcedValue2
                 pterm1 <- Context.toPrettyableTerm context term1
                 pterm2 <- Context.toPrettyableTerm context term2
                 throwIO $
@@ -278,8 +280,8 @@ unify context flexibility value1 value2 = do
                               , pterm2
                               )
               Error.OccursCheck stack -> do
-                term1 <- Elaboration.readback context value1
-                term2 <- Elaboration.readback context value2
+                term1 <- Elaboration.readback context unforcedValue1
+                term2 <- Elaboration.readback context unforcedValue2
                 pterm1 <- Context.toPrettyableTerm context term1
                 pterm2 <- Context.toPrettyableTerm context term2
                 throwIO $