diff --git a/src/Elaboration.hs b/src/Elaboration.hs
index 02868a2..812a005 100644
--- a/src/Elaboration.hs
+++ b/src/Elaboration.hs
@@ -620,15 +620,14 @@ elaborateWith context spannedTerm@(Surface.Term span term) mode canPostpone = do
       target' <- check context target Builtin.Type
       result context mode (Syntax.Spanned span $ Syntax.Fun domain' Explicit target') Builtin.Type
     (Surface.Case scrutinee branches, _) -> do
-      skipContext <- Context.skip context
-      (scrutinee', scrutineeType) <- inferAndInsertMetas skipContext UntilExplicit scrutinee $ pure Nothing
+      (scrutinee', scrutineeType) <- inferAndInsertMetas context UntilExplicit scrutinee $ pure Nothing
       case mode of
         Infer _ -> do
           expectedType <- Context.newMetaType context
-          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType Postponement.CanPostpone
+          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType
           pure $ Inferred (Syntax.Spanned span term') expectedType
         Check expectedType -> do
-          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType Postponement.CanPostpone
+          term' <- Matching.checkCase context scrutinee' scrutineeType branches expectedType
           pure $ Checked $ Syntax.Spanned span term'
     (Surface.App function@(Surface.Term functionSpan _) argument@(Surface.Term argumentSpan _), _) -> do
       (function', functionType) <- inferAndInsertMetas context UntilExplicit function $ getModeExpectedTypeName context mode
@@ -758,11 +757,9 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d
               . Syntax.Let bindings Index.Zero boundTerm
               <$> lets''
         Just (previousSpan, var) -> do
-          case Context.lookupVarValue var context of
-            Just _ -> do
-              Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan
-              elaborateLets context declaredNames undefinedVars definedVars lets' body mode
-            Nothing -> do
+          value <- Context.forceHead context (Domain.Neutral (Domain.Var var) Domain.Empty)
+          case value of
+            (Domain.Neutral (Domain.Var sameVar) Domain.Empty) | var == sameVar -> do
               let type_ =
                     Context.lookupVarType var context
               boundTerm <- Clauses.check context clauses' type_
@@ -780,12 +777,15 @@ elaborateLets context declaredNames undefinedVars definedVars lets body mode = d
                 pure $ defines context values
               lets'' <- elaborateLets redefinedContext declaredNames undefinedVars' definedVars' lets' body mode
               pure $ Syntax.Let bindings index boundTerm <$> lets''
+            _ -> do
+              Context.report (Context.spanned span context) $ Error.DuplicateLetName surfaceName previousSpan
+              elaborateLets context declaredNames undefinedVars definedVars lets' body mode
   where
     defines :: Context v -> Tsil (Var, Domain.Value) -> Context v
     defines =
       foldr' \(var, value) context' ->
         if isJust $ Context.lookupVarIndex var context'
-          then Context.defineWellOrdered context' var value
+          then Context.defineWellOrdered context' (Domain.Var var) Domain.Empty value
           else context'
 
 forceExpectedTypeHead :: Context v -> Mode result -> M (Mode result)
diff --git a/src/Elaboration/Context.hs b/src/Elaboration/Context.hs
index fdef800..890ab95 100644
--- a/src/Elaboration/Context.hs
+++ b/src/Elaboration/Context.hs
@@ -9,7 +9,10 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE NoFieldSelectors #-}
 
-module Elaboration.Context where
+module Elaboration.Context (
+  module Elaboration.Context,
+  module Elaboration.Context.Type,
+) where
 
 import qualified Builtin
 import Control.Exception.Lifted
@@ -27,28 +30,24 @@ import Data.EnumMap (EnumMap)
 import qualified Data.EnumMap as EnumMap
 import Data.EnumSet (EnumSet)
 import qualified Data.EnumSet as EnumSet
-import Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import Data.HashSet (HashSet)
 import Data.IORef.Lifted
-import Data.IntSeq (IntSeq)
 import qualified Data.IntSeq as IntSeq
-import qualified Data.Kind
 import qualified Data.Sequence as Seq
 import qualified Data.Set as Set
-import Data.Tsil (Tsil)
 import qualified Data.Tsil as Tsil
+import Elaboration.Context.Type
 import qualified Elaboration.Meta as Meta
 import qualified Elaboration.Postponed as Postponed
+import {-# SOURCE #-} Elaboration.Unification as Unification
 import Environment (Environment (Environment))
 import qualified Environment
-import Error (Error)
 import qualified Error
 import qualified Error.Hydrated as Error
 import qualified Error.Parsing as Error
 import Index
 import qualified Index.Map
-import qualified Index.Map as Index
 import Literal (Literal)
 import qualified Meta
 import Monad
@@ -57,6 +56,7 @@ import qualified Name
 import Plicity
 import qualified Postponement
 import Prettyprinter (Doc)
+import qualified Prettyprinter.Render.Text as Prettyprinter
 import Protolude hiding (catch, check, force, moduleName, state)
 import qualified Query
 import Rock
@@ -66,45 +66,36 @@ import Telescope (Telescope)
 import qualified Telescope
 import Var
 
-data Context (v :: Data.Kind.Type) = Context
-  { definitionKind :: !Scope.DefinitionKind
-  , definitionName :: !Name.Qualified
-  , definitionType :: Maybe Domain.Type
-  , span :: !Span.Relative
-  , indices :: Index.Map v Var
-  , surfaceNames :: HashMap Name.Surface (Domain.Value, Domain.Type)
-  , varNames :: EnumMap Var Name
-  , values :: EnumMap Var Domain.Value
-  , types :: EnumMap Var Domain.Type
-  , boundVars :: IntSeq Var
-  , metas :: !(IORef (Meta.State M))
-  , postponed :: !(IORef Postponed.Checks)
-  , coveredConstructors :: CoveredConstructors
-  , coveredLiterals :: CoveredLiterals
-  , coverageChecks :: !(IORef (Tsil CoverageCheck))
-  , errors :: !(IORef (Tsil Error))
-  }
-
 moduleName :: Context v -> Name.Module
 moduleName context = context.definitionName.moduleName
 
-type CoveredConstructors = EnumMap Var (HashSet Name.QualifiedConstructor)
-
-type CoveredLiterals = EnumMap Var (HashSet Literal)
-
-data CoverageCheck = CoverageCheck
-  { allClauses :: Set Span.Relative
-  , usedClauses :: IORef (Set Span.Relative)
-  , matchKind :: !Error.MatchKind
-  }
-
 toEnvironment
   :: Context v
   -> Domain.Environment v
 toEnvironment context =
   Environment
     { indices = context.indices
-    , values = mempty
+    , values =
+        EnumMap.fromList
+          $ mapMaybe
+            ( \(head_, spines) ->
+                case head_ of
+                  Domain.Var var -> do
+                    let emptySpineValues =
+                          mapMaybe
+                            ( \(spine, value) ->
+                                case spine of
+                                  Domain.Empty -> Just (var, value)
+                                  _ -> Nothing
+                            )
+                            spines
+                    case emptySpineValues of
+                      [value] -> Just value
+                      [] -> Nothing
+                      _ -> panic "multiple spine values"
+                  _ -> Nothing
+            )
+          $ HashMap.toList context.equations.equal
     , glueableBefore = Index.Zero
     }
 
@@ -123,15 +114,13 @@ empty definitionKind definitionName = do
       , surfaceNames = mempty
       , varNames = mempty
       , indices = Index.Map.Empty
-      , values = mempty
       , types = mempty
       , boundVars = mempty
       , metas = ms
       , postponed = ps
-      , errors = es
-      , coveredConstructors = mempty
-      , coveredLiterals = mempty
+      , equations = Equations mempty mempty
       , coverageChecks = cs
+      , errors = es
       }
 
 emptyFrom :: Context v -> Context Void
@@ -144,15 +133,13 @@ emptyFrom context =
     , surfaceNames = mempty
     , varNames = mempty
     , indices = Index.Map.Empty
-    , values = mempty
     , types = mempty
     , boundVars = mempty
     , metas = context.metas
     , postponed = context.postponed
-    , errors = context.errors
-    , coveredConstructors = mempty
-    , coveredLiterals = mempty
+    , equations = Equations mempty mempty
     , coverageChecks = context.coverageChecks
+    , errors = context.errors
     }
 
 spanned :: Span.Relative -> Context v -> Context v
@@ -161,6 +148,50 @@ spanned s context =
     { span = s
     }
 
+-------------------------------------------------------------------------------
+coveredConstructorsAndLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Name.QualifiedConstructor, HashSet Literal)
+coveredConstructorsAndLiterals context head_ spine =
+  case HashMap.lookup head_ context.equations.notEqual of
+    Nothing -> pure mempty
+    Just spines ->
+      fold
+        <$> mapM
+          ( \(spine', constructors, literals) -> do
+              eq <- Unification.equalSpines context spine spine'
+              pure if eq then (constructors, literals) else mempty
+          )
+          spines
+
+coveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Name.QualifiedConstructor)
+coveredConstructors context head_ spine = fst <$> coveredConstructorsAndLiterals context head_ spine
+
+coveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> M (HashSet Literal)
+coveredLiterals context head_ spine = snd <$> coveredConstructorsAndLiterals context head_ spine
+
+withCoveredConstructors :: Context v -> Domain.Head -> Domain.Spine -> HashSet Name.QualifiedConstructor -> Context v
+withCoveredConstructors context head_ spine constructors =
+  context
+    { equations =
+        context.equations
+          { notEqual =
+              HashMap.insertWith (<>) head_ [(spine, constructors, mempty)] context.equations.notEqual
+          }
+    }
+
+withCoveredLiterals :: Context v -> Domain.Head -> Domain.Spine -> HashSet Literal -> Context v
+withCoveredLiterals context head_ spine literals =
+  context
+    { equations =
+        context.equations
+          { notEqual =
+              HashMap.insertWith
+                (<>)
+                head_
+                [(spine, mempty, literals)]
+                context.equations.notEqual
+          }
+    }
+
 -------------------------------------------------------------------------------
 -- Extension
 
@@ -212,7 +243,10 @@ extendSurfaceDef context surfaceName@(Name.Surface nameText) value type_ = do
         { surfaceNames = HashMap.insert surfaceName (Domain.var var, type_) context.surfaceNames
         , varNames = EnumMap.insert var (Name nameText) context.varNames
         , indices = context.indices Index.Map.:> var
-        , values = EnumMap.insert var value context.values
+        , equations =
+            context.equations
+              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              }
         , types = EnumMap.insert var type_ context.types
         }
     , var
@@ -236,7 +270,10 @@ extendDef context name value type_ = do
     ( context
         { varNames = EnumMap.insert var name context.varNames
         , indices = context.indices Index.Map.:> var
-        , values = EnumMap.insert var value context.values
+        , equations =
+            context.equations
+              { equal = HashMap.insert (Domain.Var var) [(Domain.Empty, value)] context.equations.equal
+              }
         , types = EnumMap.insert var type_ context.types
         }
     , var
@@ -263,11 +300,16 @@ extendBefore context beforeVar binding type_ = do
     , var
     )
 
-defineWellOrdered :: Context v -> Var -> Domain.Value -> Context v
-defineWellOrdered context var value =
+defineWellOrdered :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> Context v
+defineWellOrdered context head_ spine value =
   context
-    { values = EnumMap.insert var value context.values
-    , boundVars = IntSeq.delete var context.boundVars
+    { equations =
+        context.equations
+          { equal = HashMap.insertWith (<>) head_ [(spine, value)] context.equations.equal
+          }
+    , boundVars = case (head_, spine) of
+        (Domain.Var var, Domain.Empty) -> IntSeq.delete var context.boundVars
+        _ -> context.boundVars
     }
 
 skip :: Context v -> M (Context (Succ v))
@@ -275,65 +317,66 @@ skip context = do
   (context', _) <- extendDef context "skip" Builtin.Type Builtin.Type
   pure context'
 
-define :: Context v -> Var -> Domain.Value -> M (Context v)
-define context var value = do
-  deps <- evalStateT (dependencies context value) mempty
-  let context' = defineWellOrdered context var value
-      (pre, post) =
-        Tsil.partition (`EnumSet.member` deps) $
-          IntSeq.toTsil context'.boundVars
-  pure
-    context'
-      { boundVars =
-          IntSeq.fromTsil pre <> IntSeq.fromTsil post
-      }
+define :: Context v -> Domain.Head -> Domain.Spine -> Domain.Value -> M (Context v)
+define context head_ spine value = do
+  deps <- evalStateT (freeVars context value) mempty
+  let context' = defineWellOrdered context head_ spine value
+      context''
+        | EnumSet.null deps = context'
+        | otherwise =
+            context'
+              { boundVars =
+                  IntSeq.fromTsil pre <> IntSeq.fromTsil post
+              }
+      (pre, post) = Tsil.partition (`EnumSet.member` deps) $ IntSeq.toTsil context'.boundVars
+  pure context''
 
 -- TODO: Move
-dependencies
+freeVars
   :: Context v
   -> Domain.Value
   -> StateT (EnumMap Var (EnumSet Var)) M (EnumSet Var)
-dependencies context value = do
+freeVars context value = do
   value' <- lift $ forceHeadGlue context value
   case value' of
     Domain.Neutral hd spine -> do
       hdVars <- headVars hd
-      elimVars <- Domain.mapM eliminationDependencies spine
+      elimVars <- Domain.mapM eliminationVars spine
       pure $ hdVars <> fold elimVars
     Domain.Con _ args ->
-      fold <$> mapM (dependencies context . snd) args
+      fold <$> mapM (freeVars context . snd) args
     Domain.Lit _ ->
       pure mempty
     Domain.Glued (Domain.Global _) spine _ ->
-      fold <$> Domain.mapM eliminationDependencies spine
+      fold <$> Domain.mapM eliminationVars spine
     Domain.Glued _ _ value'' ->
-      dependencies context value''
+      freeVars context value''
     Domain.Lazy lazyValue -> do
       value'' <- lift $ force lazyValue
-      dependencies context value''
+      freeVars context value''
     Domain.Lam bindings type' _ closure ->
-      abstractionDependencies (Bindings.toName bindings) type' closure
+      abstractionVars (Bindings.toName bindings) type' closure
     Domain.Pi binding type' _ closure ->
-      abstractionDependencies (Binding.toName binding) type' closure
+      abstractionVars (Binding.toName binding) type' closure
     Domain.Fun domain _ target -> do
-      domainVars <- dependencies context domain
-      targetVars <- dependencies context target
+      domainVars <- freeVars context domain
+      targetVars <- freeVars context target
       pure $ domainVars <> targetVars
   where
-    eliminationDependencies elimination =
+    eliminationVars elimination =
       case elimination of
         Domain.App _plicity arg ->
-          dependencies context arg
+          freeVars context arg
         Domain.Case (Domain.Branches env branches defaultBranch) -> do
-          defaultBranchVars <- mapM (dependencies context <=< lift . Evaluation.evaluate env) defaultBranch
+          defaultBranchVars <- mapM (freeVars context <=< lift . Evaluation.evaluate env) defaultBranch
           brVars <- branchVars context env branches
           pure $ fold defaultBranchVars <> brVars
 
-    abstractionDependencies name type' closure = do
-      typeVars <- dependencies context type'
+    abstractionVars name type' closure = do
+      typeVars <- freeVars context type'
       (context', var) <- lift $ extend context name type'
       body <- lift $ Evaluation.evaluateClosure closure $ Domain.var var
-      bodyVars <- dependencies context' body
+      bodyVars <- freeVars context' body
       pure $ typeVars <> EnumSet.delete var bodyVars
 
     headVars hd =
@@ -343,7 +386,7 @@ dependencies context value = do
               cache <- get
               typeDeps <- case EnumMap.lookup v cache of
                 Nothing -> do
-                  typeDeps <- dependencies context $ lookupVarType v context
+                  typeDeps <- freeVars context $ lookupVarType v context
                   modify $ EnumMap.insert v typeDeps
                   pure typeDeps
                 Just typeDeps ->
@@ -370,7 +413,7 @@ dependencies context value = do
           Syntax.LiteralBranches literalBranches ->
             forM (toList literalBranches) \(_, branch) -> do
               branch' <- lift $ Evaluation.evaluate env branch
-              dependencies context' branch'
+              freeVars context' branch'
 
     telescopeVars
       :: Context v
@@ -381,10 +424,10 @@ dependencies context value = do
       case tele of
         Telescope.Empty body -> do
           body' <- lift $ Evaluation.evaluate env body
-          dependencies context' body'
+          freeVars context' body'
         Telescope.Extend binding domain _ tele' -> do
           domain' <- lift $ Evaluation.evaluate env domain
-          domainVars <- dependencies context' domain'
+          domainVars <- freeVars context' domain'
           (context'', var) <- lift $ extend context' (Bindings.toName binding) domain'
           let env' =
                 Environment.extendVar env var
@@ -419,10 +462,6 @@ lookupVarType :: Var -> Context v -> Domain.Type
 lookupVarType var context =
   EnumMap.findWithDefault (panic $ "Context.lookupVarType " <> show var) var context.types
 
-lookupVarValue :: Var -> Context v -> Maybe Domain.Type
-lookupVarValue var context =
-  EnumMap.lookup var context.values
-
 -------------------------------------------------------------------------------
 -- Prettyable terms
 
@@ -496,12 +535,7 @@ newMetaReturningIndex context type_ = do
 piBoundVars :: Context v -> Domain.Type -> M (Syntax.Type Void, Int)
 piBoundVars context type_ = do
   let arity = IntSeq.length context.boundVars
-  piType <-
-    varPis
-      context
-      Environment.empty {Environment.values = context.values}
-      ((Explicit,) <$> toList context.boundVars)
-      type_
+  piType <- varPis context Environment.empty ((Explicit,) <$> toList context.boundVars) type_
   pure (piType, arity)
 
 varPis
@@ -594,13 +628,8 @@ forceHead
   -> M Domain.Value
 forceHead context value =
   case value of
-    Domain.Neutral (Domain.Var var) spine
-      | Just headValue <- lookupVarValue var context -> do
-          value' <- Evaluation.applySpine headValue spine
-          forceHead context value'
     Domain.Neutral (Domain.Meta metaIndex) spine -> do
       meta <- lookupEagerMeta context metaIndex
-
       case meta of
         Meta.EagerSolved headValue _ _ -> do
           headValue' <- Evaluation.evaluate Environment.empty headValue
@@ -608,6 +637,19 @@ forceHead context value =
           forceHead context value'
         Meta.EagerUnsolved {} ->
           pure value
+    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
+                    eq <- Unification.equalSpines context spinePrefix eqSpine
+                    if eq
+                      then do
+                        value' <- Evaluation.applySpine eqValue spineSuffix
+                        forceHead context value'
+                      else go rest
+              go (_ : rest) = go rest
+          go spineValues
     Domain.Glued _ _ value' ->
       forceHead context value'
     Domain.Lazy lazyValue -> do
@@ -624,23 +666,29 @@ forceHeadGlue
   -> M Domain.Value
 forceHeadGlue context value =
   case value of
-    Domain.Neutral (Domain.Var var) spine
-      | Just headValue <- lookupVarValue var context -> do
-          lazyValue <- lazy $ do
-            value' <- Evaluation.applySpine headValue spine
-            forceHeadGlue context value'
-          pure $ Domain.Glued (Domain.Var var) spine $ Domain.Lazy lazyValue
     Domain.Neutral (Domain.Meta metaIndex) spine -> do
       meta <- lookupEagerMeta context metaIndex
       case meta of
         Meta.EagerSolved headValue _ _ -> do
-          lazyValue <- lazy $ do
+          lazyValue <- lazy do
             headValue' <- Evaluation.evaluate Environment.empty headValue
-            value' <- Evaluation.applySpine headValue' spine
-            forceHeadGlue context value'
+            Evaluation.applySpine headValue' spine
           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
+          let go [] = pure value
+              go ((eqSpine, eqValue) : rest)
+                | Just (spinePrefix, spineSuffix) <- Domain.matchSpinePrefix spine eqSpine = do
+                    eq <- Unification.equalSpines context spinePrefix eqSpine
+                    if eq
+                      then do
+                        lazyValue <- lazy $ Evaluation.applySpine eqValue spineSuffix
+                        pure $ Domain.Glued head_ spine $ Domain.Lazy lazyValue
+                      else go rest
+              go (_ : rest) = go rest
+          go spineValues
     Domain.Lazy lazyValue -> do
       value' <- force lazyValue
       forceHeadGlue context value'
diff --git a/src/Elaboration/Equation.hs b/src/Elaboration/Equation.hs
new file mode 100644
index 0000000..33ff969
--- /dev/null
+++ b/src/Elaboration/Equation.hs
@@ -0,0 +1,214 @@
+{-# LANGUAGE BlockArguments #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE NoFieldSelectors #-}
+
+module Elaboration.Equation where
+
+import Control.Exception.Lifted
+import qualified Core.Binding as Binding
+import Core.Bindings (Bindings)
+import qualified Core.Bindings as Bindings
+import qualified Core.Domain as Domain
+import qualified Core.Evaluation as Evaluation
+import qualified Core.Syntax as Syntax
+import qualified Data.HashSet as HashSet
+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
+import Monad
+import Protolude hiding (catch, force, throwIO)
+import Telescope (Telescope)
+import qualified Telescope
+
+data Error
+  = Nope
+  | Dunno
+  deriving (Eq, Ord, Show, Exception)
+
+type Equate v = StateT (Context v) M
+
+equate :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v)
+equate context flexibility value1 value2 = do
+  putText "Equating"
+  Context.dumpValue context value1
+  Context.dumpValue context value2
+  execStateT
+    (equateM flexibility value1 value2)
+    context
+
+contextual1 :: (Context v -> a -> M b) -> a -> Equate v b
+contextual1 f x = do
+  c <- get
+  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
+
+    -- Vars
+    (Domain.Neutral head1 spine1, _)
+      | Flexibility.Rigid <- max (Domain.headFlexibility head1) flexibility ->
+          solve head1 spine1 value2
+    (_, Domain.Neutral head2 spine2)
+      | Flexibility.Rigid <- max (Domain.headFlexibility head2) flexibility ->
+          solve head2 spine2 value1
+    _ ->
+      throwIO Dunno
+
+solve :: Domain.Head -> Domain.Spine -> Domain.Value -> Equate v ()
+solve head_ spine value = do
+  context <- get
+  context' <- lift do
+    value' <- Context.forceHead context value
+    case value' of
+      Domain.Con con _ -> do
+        covered <- Context.coveredConstructors context head_ spine
+        when (con `HashSet.member` covered) $
+          throwIO Nope
+      Domain.Lit lit -> do
+        covered <- Context.coveredLiterals context head_ spine
+        when (lit `HashSet.member` covered) $
+          throwIO Nope
+      _ -> pure ()
+    occurs context (== head_) Flexibility.Rigid value
+    -- occursSpine context isMeta Flexibility.Rigid spine
+    Context.define context head_ spine value
+  put context'
+
+-- where
+--   isMeta (Domain.Meta _) = True
+--   isMeta _ = False
+
+equateSpines
+  :: Flexibility
+  -> Domain.Spine
+  -> Domain.Spine
+  -> Equate v ()
+equateSpines flexibility spine1 spine2 =
+  case (spine1, spine2) of
+    (Domain.Empty, Domain.Empty) -> pure ()
+    (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
+
+occurs :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Value -> M ()
+occurs context occ flexibility value = do
+  value' <- Context.forceHeadGlue context value
+  case value' of
+    Domain.Neutral hd spine
+      | occ hd ->
+          throwIO case flexibility of
+            Flexibility.Rigid -> Nope
+            Flexibility.Flexible -> Dunno
+      | otherwise ->
+          occursSpine context occ (max (Domain.headFlexibility hd) flexibility) spine
+    Domain.Con _ args ->
+      mapM_ (occurs context occ flexibility . snd) args
+    Domain.Lit _ ->
+      pure ()
+    Domain.Glued (Domain.Var _) _ value'' ->
+      occurs context occ flexibility value''
+    Domain.Glued hd spine value'' ->
+      occurs context occ Flexibility.Flexible (Domain.Neutral hd spine) `catch` \(_ :: Error) ->
+        occurs context occ flexibility value''
+    Domain.Lazy lazyValue -> do
+      value'' <- force lazyValue
+      occurs context occ flexibility 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
+      occurs context occ flexibility domain
+      occurs context occ flexibility target
+  where
+    occursAbstraction name type_ closure = do
+      occurs context occ flexibility type_
+      (context', var) <- Context.extend context name type_
+      let varValue = Domain.var var
+      body <- Evaluation.evaluateClosure closure varValue
+      occurs context' occ flexibility body
+
+occursSpine :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Spine -> M ()
+occursSpine context occ flexibility =
+  Domain.mapM_ $ occursElimination context occ flexibility
+
+occursElimination :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Elimination -> M ()
+occursElimination context occ flexibility elimination =
+  case elimination of
+    Domain.App _plicity arg -> occurs context occ flexibility arg
+    Domain.Case branches -> occursBranches context occ flexibility branches
+
+occursBranches :: Context v -> (Domain.Head -> Bool) -> Flexibility -> Domain.Branches -> M ()
+occursBranches context occ flexibility (Domain.Branches outerEnv branches defaultBranch) = do
+  case branches of
+    Syntax.ConstructorBranches _ constructorBranches ->
+      forM_ constructorBranches $ mapM_ $ occursTele context outerEnv
+    Syntax.LiteralBranches literalBranches ->
+      forM_ literalBranches $
+        mapM_ $
+          occursTele context outerEnv . Telescope.Empty
+  forM_ defaultBranch $
+    occursTele context outerEnv . Telescope.Empty
+  where
+    occursTele
+      :: Context v1
+      -> Domain.Environment v2
+      -> Telescope Bindings Syntax.Type Syntax.Term v2
+      -> M ()
+    occursTele context' env tele =
+      case tele of
+        Telescope.Extend bindings type_ _plicity tele' -> do
+          type' <- Evaluation.evaluate env type_
+          occurs context' occ flexibility type'
+          (context'', var) <- Context.extend context (Bindings.toName bindings) type'
+          occursTele context'' (Environment.extendVar env var) tele'
+        Telescope.Empty body -> do
+          body' <- Evaluation.evaluate env body
+          occurs context' occ flexibility body'
diff --git a/src/Elaboration/Matching.hs b/src/Elaboration/Matching.hs
index 0fea5a9..1addf26 100644
--- a/src/Elaboration/Matching.hs
+++ b/src/Elaboration/Matching.hs
@@ -24,9 +24,7 @@ import qualified Core.Domain.Pattern as Domain.Pattern
 import qualified Core.Domain.Telescope as Domain (Telescope)
 import qualified Core.Domain.Telescope as Domain.Telescope
 import qualified Core.Evaluation as Evaluation
-import qualified Core.Readback as Readback
 import qualified Core.Syntax as Syntax
-import qualified Data.EnumMap as EnumMap
 import Data.HashMap.Lazy (HashMap)
 import qualified Data.HashMap.Lazy as HashMap
 import Data.HashSet (HashSet)
@@ -41,14 +39,14 @@ import qualified Data.Tsil as Tsil
 import {-# SOURCE #-} qualified Elaboration
 import Elaboration.Context (Context)
 import qualified Elaboration.Context as Context
+import qualified Elaboration.Equation as Equation
 import qualified Elaboration.Matching.SuggestedName as SuggestedName
+import qualified Elaboration.Meta as Meta
 import qualified Elaboration.Unification as Unification
-import qualified Elaboration.Unification.Indices as Indices
 import qualified Environment
 import qualified Error
 import qualified Flexibility
 import GHC.Exts (fromList)
-import qualified Index
 import Literal (Literal)
 import qualified Meta
 import Monad
@@ -166,109 +164,30 @@ resolvePattern context unspannedPattern type_ canPostpone = do
 
 checkCase
   :: Context v
-  -> Syntax.Term (Index.Succ v)
+  -> Syntax.Term v
   -> Domain.Type
   -> [(Surface.Pattern, Surface.Term)]
   -> Domain.Type
-  -> Postponement.CanPostpone
   -> M (Syntax.Term v)
-checkCase context scrutinee scrutineeType branches expectedType canPostpone = do
-  skippedContext <- Context.skip context
-  scrutineeValue <- Elaboration.evaluate skippedContext scrutinee
-  blockingMetaOrIsPatternScrutinee <- runExceptT $ isPatternValue context scrutineeValue
-  case (canPostpone, blockingMetaOrIsPatternScrutinee) of
-    (Postponement.CanPostpone, Left blockingMeta) ->
-      postponeCaseCheck context scrutinee scrutineeType branches expectedType blockingMeta
-    _ -> do
-      (context', var) <-
-        if fromRight False blockingMetaOrIsPatternScrutinee
-          then Context.extendDef context "scrutinee" scrutineeValue scrutineeType
-          else Context.extend context "scrutinee" scrutineeType
-
-      let scrutineeVarValue =
-            Domain.var var
-      usedClauses <- newIORef mempty
-      term <-
-        checkWithCoverage
-          context'
-          Config
-            { expectedType = expectedType
-            , scrutinees = pure (Explicit, scrutineeVarValue)
-            , clauses =
-                [ Clause
-                  { span = Span.add patSpan rhsSpan
-                  , matches = [Match scrutineeVarValue scrutineeVarValue Explicit (unresolvedPattern pat) scrutineeType]
-                  , rhs = rhs'
-                  }
-                | (pat@(Surface.Pattern patSpan _), rhs'@(Surface.Term rhsSpan _)) <- branches
-                ]
-            , usedClauses = usedClauses
-            , matchKind = Error.Branch
+checkCase context scrutinee scrutineeType branches expectedType = do
+  scrutineeValue <- Elaboration.evaluate context scrutinee
+  usedClauses <- newIORef mempty
+  checkWithCoverage
+    context
+    Config
+      { expectedType = expectedType
+      , scrutinees = pure (Explicit, scrutineeValue)
+      , clauses =
+          [ Clause
+            { span = Span.add patSpan rhsSpan
+            , matches = [Match scrutineeValue scrutineeValue Explicit (unresolvedPattern pat) scrutineeType]
+            , rhs = rhs'
             }
-      scrutineeType' <- Readback.readback (Context.toEnvironment context) scrutineeType
-      pure $
-        Syntax.Lets $
-          Syntax.LetType "scrutinee" scrutineeType' $
-            Syntax.Let "scrutinee" Index.Zero scrutinee $
-              Syntax.In term
-
-postponeCaseCheck
-  :: Context v
-  -> Syntax.Term (Index.Succ v)
-  -> Domain.Type
-  -> [(Surface.Pattern, Surface.Term)]
-  -> Domain.Type
-  -> Meta.Index
-  -> M (Syntax.Term v)
-postponeCaseCheck context scrutinee scrutineeType branches expectedType blockingMeta =
-  Elaboration.postpone context expectedType blockingMeta $
-    checkCase context scrutinee scrutineeType branches expectedType
-
-isPatternValue :: Context v -> Domain.Value -> ExceptT Meta.Index M Bool
-isPatternValue context value = do
-  value' <- lift $ Context.forceHead context value
-  case value' of
-    Domain.Neutral (Domain.Var _) Domain.Empty ->
-      pure True
-    Domain.Neutral (Domain.Var _) (_ Domain.:> _) ->
-      pure False
-    Domain.Neutral (Domain.Global _) _ ->
-      pure False
-    Domain.Neutral (Domain.Meta blockingMeta) _ ->
-      throwError blockingMeta
-    Domain.Lit _ ->
-      pure True
-    Domain.Con constr args -> do
-      constrTypeTele <- fetch $ Query.ConstructorType constr
-      let spine' =
-            dropTypeArgs constrTypeTele $ toList args
-
-      and <$> mapM (isPatternValue context . snd) spine'
-    Domain.Glued _ _ value'' ->
-      isPatternValue context value''
-    Domain.Lazy lazyValue -> do
-      value'' <- lift $ force lazyValue
-      isPatternValue context value''
-    Domain.Lam {} ->
-      pure False
-    Domain.Pi {} ->
-      pure False
-    Domain.Fun {} ->
-      pure False
-  where
-    dropTypeArgs
-      :: Telescope n t t' v
-      -> [(Plicity, value)]
-      -> [(Plicity, value)]
-    dropTypeArgs tele args =
-      case (tele, args) of
-        (Telescope.Empty _, _) ->
-          args
-        (Telescope.Extend _ _ plicity1 tele', (plicity2, _) : args')
-          | plicity1 == plicity2 ->
-              dropTypeArgs tele' args'
-        _ ->
-          panic "chooseBranch arg mismatch"
+          | (pat@(Surface.Pattern patSpan _), rhs'@(Surface.Term rhsSpan _)) <- branches
+          ]
+      , usedClauses = usedClauses
+      , matchKind = Error.Branch
+      }
 
 checkClauses
   :: Context v
@@ -302,14 +221,9 @@ checkSingle
   -> Domain.Type
   -> M (Syntax.Term v)
 checkSingle context scrutinee plicity pat@(Surface.Pattern patSpan _) rhs@(Surface.Term rhsSpan _) expectedType = do
-  let scrutineeValue =
-        Domain.var scrutinee
-
-      scrutineeType =
-        Context.lookupVarType scrutinee context
-
+  let scrutineeValue = Domain.var scrutinee
+      scrutineeType = Context.lookupVarType scrutinee context
   usedClauses <- newIORef mempty
-
   checkWithCoverage
     context
     Config
@@ -364,7 +278,7 @@ check context config canPostpone = do
     firstClause : _ -> do
       let matches = firstClause.matches
       splitEqualityOr context config' matches $
-        splitConstructorOr context config' matches $ do
+        splitConstructorOr context config' matches canPostpone do
           let indeterminateIndexUnification = do
                 Context.report context $ Error.IndeterminateIndexUnification config.matchKind
                 Elaboration.readback context $ Builtin.Unknown config.expectedType
@@ -396,6 +310,10 @@ findPatternResolutionBlocker context clauses =
         forM_ clause.matches \case
           Match _ _ _ (UnresolvedPattern span unspannedSurfacePattern) type_ ->
             void $ resolvePattern (Context.spanned span context) unspannedSurfacePattern type_ Postponement.CanPostpone
+          Match _ (Domain.Neutral (Domain.Meta blockingMeta) _) _ (Pattern _ Con {}) _ ->
+            throwError blockingMeta
+          Match _ (Domain.Neutral (Domain.Meta blockingMeta) _) _ (Pattern _ Lit {}) _ ->
+            throwError blockingMeta
           Match _ _ _ Pattern {} _ ->
             pure ()
 
@@ -425,10 +343,8 @@ uncoveredScrutineePatterns
 uncoveredScrutineePatterns context value = do
   value' <- Context.forceHead context value
   case value' of
-    Domain.Neutral (Domain.Var v) Domain.Empty -> do
-      let covered =
-            EnumMap.findWithDefault mempty v context.coveredConstructors
-
+    Domain.Neutral head_ spine -> do
+      covered <- Context.coveredConstructors context head_ spine
       case HashSet.toList covered of
         [] ->
           pure [Domain.Pattern.Wildcard]
@@ -453,12 +369,6 @@ uncoveredScrutineePatterns context value = do
                       ]
             _ ->
               panic "uncoveredScrutineePatterns non-data"
-    Domain.Neutral (Domain.Var _) (_ Domain.:> _) ->
-      pure []
-    Domain.Neutral (Domain.Meta _) _ ->
-      pure []
-    Domain.Neutral (Domain.Global _) _ ->
-      pure []
     Domain.Lit lit ->
       pure [Domain.Pattern.Lit lit]
     Domain.Con constr args -> do
@@ -531,11 +441,14 @@ simplifyMatch context canPostpone match@(Match value forcedValue plicity pat typ
           simplifyMatch context canPostpone $ Match value forcedValue plicity (Pattern span unspannedPattern) type_
     Pattern span unspannedPattern -> do
       forcedValue' <- lift $ Context.forceHead context forcedValue
+      putText "forced value"
+      lift $ Context.dumpValue context forcedValue'
       let match' =
             Match value forcedValue' plicity pat type_
       case (forcedValue', unspannedPattern) of
         (Domain.Con constr args, Con _ constr' pats)
           | constr == constr' -> do
+              putText $ "matching con" <> show constr
               matches' <- lift $ do
                 constrType <- fetch $ Query.ConstructorType constr
                 (patsType, patSpine) <-
@@ -557,14 +470,16 @@ simplifyMatch context canPostpone match@(Match value forcedValue plicity pat typ
               pure []
           | otherwise ->
               fail "Literal mismatch"
-        (Domain.Neutral (Domain.Var var) Domain.Empty, Con _ constr _)
-          | Just coveredConstrs <- EnumMap.lookup var context.coveredConstructors
-          , HashSet.member constr coveredConstrs ->
-              fail "Constructor already covered"
-        (Domain.Neutral (Domain.Var var) Domain.Empty, Lit lit)
-          | Just coveredLits <- EnumMap.lookup var context.coveredLiterals
-          , HashSet.member lit coveredLits ->
-              fail "Literal already covered"
+        (Domain.Neutral head_ spine, Con _ constr _) -> do
+          covered <- lift $ Context.coveredConstructors context head_ spine
+          if HashSet.member constr covered
+            then fail "Constructor already covered"
+            else pure [match']
+        (Domain.Neutral head_ spine, Lit lit) -> do
+          covered <- lift $ Context.coveredLiterals context head_ spine
+          if HashSet.member lit covered
+            then fail "Literal already covered"
+            else pure [match']
         _ ->
           pure [match']
 
@@ -700,7 +615,7 @@ expandAnnotations context matches =
                 pure ()
               pure $ Match value forcedValue plicity (unresolvedPattern pat) type_ : matches'
             _ ->
-              fail "couldn't create instantitation for prefix"
+              fail "couldn't create instantiation for prefix"
 
 matchInstantiation :: Match -> Maybe PatternInstantiation
 matchInstantiation match =
@@ -712,7 +627,7 @@ matchInstantiation match =
     Match _ _ _ (Pattern _ (Forced _)) _ ->
       pure mempty
     _ ->
-      fail "No match instantitation"
+      fail "No match instantiation"
 
 solved :: [Match] -> Maybe PatternInstantiation
 solved =
@@ -724,31 +639,36 @@ splitConstructorOr
   :: Context v
   -> Config
   -> [Match]
+  -> Postponement.CanPostpone
   -> M (Syntax.Term v)
   -> M (Syntax.Term v)
-splitConstructorOr context config matches k =
+splitConstructorOr context config matches canPostpone k =
   case matches of
     [] ->
       k
     match : matches' ->
       case match of
-        Match scrutinee (Domain.Neutral (Domain.Var var) Domain.Empty) _ (Pattern span (Con _ constr _)) type_ ->
-          splitConstructor context config scrutinee var span constr type_
-        Match scrutinee (Domain.Neutral (Domain.Var var) Domain.Empty) _ (Pattern span (Lit lit)) type_ ->
-          splitLiteral context config scrutinee var span lit type_
+        Match _ (Domain.Neutral (Domain.Meta _) _) _ _ _
+          | Postponement.CanPostpone <- canPostpone ->
+              splitConstructorOr context config matches' canPostpone k
+        Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Con _ constr _)) type_ ->
+          splitConstructor context config scrutinee head_ spine span constr type_
+        Match scrutinee (Domain.Neutral head_ spine) _ (Pattern span (Lit lit)) type_ ->
+          splitLiteral context config scrutinee head_ spine span lit type_
         _ ->
-          splitConstructorOr context config matches' k
+          splitConstructorOr context config matches' canPostpone k
 
 splitConstructor
   :: Context v
   -> Config
   -> Domain.Value
-  -> Var
+  -> Domain.Head
+  -> Domain.Spine
   -> Span.Relative
   -> Name.QualifiedConstructor
   -> Domain.Type
   -> M (Syntax.Term v)
-splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.QualifiedConstructor typeName _) outerType = do
+splitConstructor outerContext config scrutineeValue scrutineeHead scrutineeSpine span (Name.QualifiedConstructor typeName _) outerType = do
   (definition, _) <- fetch $ Query.ElaboratedDefinition typeName
   case definition of
     Syntax.DataDefinition _ tele -> do
@@ -761,14 +681,17 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
         _ -> do
           typeType <- fetch $ Query.ElaboratedType typeName
           typeType' <- Evaluation.evaluate Environment.empty typeType
-          let
-            -- Ensure the metas don't depend on the scrutineeVar, because that
-            -- is guaranteed to lead to circularity when solving scrutineeVar
-            -- later.
-            contextWithoutScrutineeVar =
-              outerContext
-                { Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
-                }
+          let contextWithoutScrutineeVar =
+                case scrutineeHead of
+                  Domain.Var scrutineeVar ->
+                    -- Ensure the metas don't depend on the scrutineeVar, because that
+                    -- is guaranteed to lead to circularity when solving scrutineeVar
+                    -- later.
+                    outerContext
+                      { Context.boundVars = IntSeq.delete scrutineeVar outerContext.boundVars
+                      }
+                  -- TODO: is this correct?
+                  _ -> outerContext
           (metas, _) <- Elaboration.insertMetas contextWithoutScrutineeVar Elaboration.UntilTheEnd typeType'
           f <- Unification.tryUnify outerContext (Domain.Neutral (Domain.Global typeName) $ Domain.Apps $ fromList metas) outerType
           result <- goParams (Context.spanned span outerContext) metas mempty tele'
@@ -785,11 +708,12 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
     goParams context params conArgs dataTele =
       case (params, dataTele) of
         ([], Domain.Telescope.Empty constructors) -> do
-          let matchedConstructors =
-                OrderedHashMap.fromListWith (<>) $
-                  concat $
-                    takeWhile (not . null) $
-                      findVarConstructorMatches scrutineeVar . (.matches) <$> config.clauses
+          matchedConstructors <-
+            OrderedHashMap.fromListWith (<>)
+              . concat
+              <$> mapWhileM
+                (fmap $ \xs -> if null xs then Nothing else Just xs)
+                (findConstructorMatches context scrutineeHead scrutineeSpine . (.matches) <$> config.clauses)
 
           branches <- forM (OrderedHashMap.toList matchedConstructors) \(qualifiedConstr@(Name.QualifiedConstructor _ constr), patterns) -> do
             let constrType =
@@ -807,19 +731,13 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
           defaultBranch <-
             if OrderedHashMap.size matchedConstructors == length constructors
               then pure Nothing
-              else
-                Just
-                  <$> check
-                    context
-                      { Context.coveredConstructors =
-                          EnumMap.insertWith
-                            (<>)
-                            scrutineeVar
-                            (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedConstructors)
-                            context.coveredConstructors
-                      }
-                    config
-                    Postponement.CanPostpone
+              else do
+                let context' =
+                      Context.withCoveredConstructors context scrutineeHead scrutineeSpine $
+                        HashSet.fromMap $
+                          void $
+                            OrderedHashMap.toMap matchedConstructors
+                Just <$> check context' config Postponement.CanPostpone
 
           scrutinee <- Elaboration.readback context scrutineeValue
 
@@ -852,7 +770,7 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
               Constraint ->
                 pure (Bindings.Unspanned piName, patterns)
 
-          (context', fieldVar) <- Context.extendBefore context scrutineeVar bindings domain
+          (context', fieldVar) <- Context.extend context (Bindings.toName bindings) domain
           let fieldValue = Domain.var fieldVar
               conArgs' = conArgs Tsil.:> (plicity, fieldValue)
           target <- Evaluation.evaluateClosure targetClosure fieldValue
@@ -868,86 +786,100 @@ splitConstructor outerContext config scrutineeValue scrutineeVar span (Name.Qual
                 SuggestedName.nextImplicit context "x" patterns
               Constraint ->
                 pure (Bindings.Unspanned "x", patterns)
-          (context', fieldVar) <- Context.extendBefore context scrutineeVar bindings domain
+          (context', fieldVar) <- Context.extend context (Bindings.toName bindings) domain
           let fieldValue = Domain.var fieldVar
               conArgs' = conArgs Tsil.:> (plicity, fieldValue)
           tele <- goConstrFields context' constr conArgs' target patterns'
           pure $ Telescope.Extend bindings domain'' plicity tele
         _ -> do
-          let context' =
-                Context.defineWellOrdered context scrutineeVar $ Domain.Con constr conArgs
+          putText "Equating con"
+          context' <- Equation.equate context Flexibility.Rigid scrutineeValue $ Domain.Con constr conArgs
           result <- check context' config Postponement.CanPostpone
           pure $ Telescope.Empty result
 
-findVarConstructorMatches
-  :: Var
+mapWhileM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]
+mapWhileM f as =
+  case as of
+    [] -> pure []
+    a : as' -> do
+      mb <- f a
+      case mb of
+        Nothing -> pure []
+        Just b -> (b :) <$> mapWhileM f as'
+
+findConstructorMatches
+  :: Context v
+  -> Domain.Head
+  -> Domain.Spine
   -> [Match]
-  -> [(Name.QualifiedConstructor, [(Span.Relative, [Surface.PlicitPattern])])]
-findVarConstructorMatches var matches =
+  -> M [(Name.QualifiedConstructor, [(Span.Relative, [Surface.PlicitPattern])])]
+findConstructorMatches context head_ spine matches =
   case matches of
     [] ->
-      []
-    Match _ (Domain.Neutral (Domain.Var var') Domain.Empty) _ (Pattern _ (Con span constr patterns)) _ : matches'
-      | var == var' ->
-          (constr, [(span, patterns)]) : findVarConstructorMatches var matches'
+      pure []
+    Match _ (Domain.Neutral head' spine') _ (Pattern _ (Con span constr patterns)) _ : matches'
+      | head_ == head' -> do
+          eq <- Unification.equalSpines context spine spine'
+          if eq
+            then ((constr, [(span, patterns)]) :) <$> findConstructorMatches context head_ spine matches'
+            else findConstructorMatches context head_ spine matches
     _ : matches' ->
-      findVarConstructorMatches var matches'
+      findConstructorMatches context head_ spine matches'
 
 splitLiteral
   :: Context v
   -> Config
   -> Domain.Value
-  -> Var
+  -> Domain.Head
+  -> Domain.Spine
   -> Span.Relative
   -> Literal
   -> Domain.Type
   -> M (Syntax.Term v)
-splitLiteral context config scrutineeValue scrutineeVar span lit outerType = do
-  let matchedLiterals =
-        OrderedHashMap.fromListWith (<>) $
-          concat $
-            takeWhile (not . null) $
-              findVarLiteralMatches scrutineeVar . (.matches) <$> config.clauses
+splitLiteral context config scrutineeValue scrutineeHead scrutineeSpine span lit outerType = do
+  matchedLiterals <-
+    OrderedHashMap.fromListWith (<>) . concat
+      <$> mapWhileM
+        (fmap $ \xs -> if null xs then Nothing else Just xs)
+        (findLiteralMatches context scrutineeHead scrutineeSpine . (.matches) <$> config.clauses)
 
   f <- Unification.tryUnify (Context.spanned span context) (Elaboration.inferLiteral lit) outerType
 
   branches <- forM (OrderedHashMap.toList matchedLiterals) \(int, spans) -> do
-    let context' =
-          Context.defineWellOrdered context scrutineeVar $ Domain.Lit int
+    let context' = Context.defineWellOrdered context scrutineeHead scrutineeSpine $ Domain.Lit int
     result <- check context' config Postponement.CanPostpone
     pure (int, (spans, f result))
 
-  defaultBranch <-
-    Just
-      <$> check
-        context
-          { Context.coveredLiterals =
-              EnumMap.insertWith
-                (<>)
-                scrutineeVar
-                (HashSet.fromMap $ void $ OrderedHashMap.toMap matchedLiterals)
-                context.coveredLiterals
-          }
-        config
-        Postponement.CanPostpone
+  defaultBranch <- do
+    let context' =
+          Context.withCoveredLiterals context scrutineeHead scrutineeSpine $
+            HashSet.fromMap $
+              void $
+                OrderedHashMap.toMap matchedLiterals
+    Just <$> check context' config Postponement.CanPostpone
 
   scrutinee <- Elaboration.readback context scrutineeValue
 
   pure $ f $ Syntax.Case scrutinee (Syntax.LiteralBranches $ OrderedHashMap.fromList branches) defaultBranch
 
-findVarLiteralMatches
-  :: Var
+findLiteralMatches
+  :: Context v
+  -> Domain.Head
+  -> Domain.Spine
   -> [Match]
-  -> [(Literal, [Span.Relative])]
-findVarLiteralMatches var matches =
+  -> M [(Literal, [Span.Relative])]
+findLiteralMatches context head_ spine matches =
   case matches of
     [] ->
-      []
-    Match _ (Domain.Neutral (Domain.Var var') Domain.Empty) _ (Pattern span (Lit lit)) _ : matches'
-      | var == var' ->
-          (lit, [span]) : findVarLiteralMatches var matches'
+      pure []
+    Match _ (Domain.Neutral head' spine') _ (Pattern span (Lit lit)) _ : matches'
+      | head_ == head' -> do
+          eq <- Unification.equalSpines context spine spine'
+          if eq
+            then ((lit, [span]) :) <$> findLiteralMatches context head_ spine matches'
+            else findLiteralMatches context head_ spine matches'
     _ : matches' ->
-      findVarLiteralMatches var matches'
+      findLiteralMatches context head_ spine matches'
 
 -------------------------------------------------------------------------------
 
@@ -964,24 +896,27 @@ splitEqualityOr context config matches k =
     match : matches' ->
       case match of
         Match
-          _
-          (Domain.Neutral (Domain.Var var) Domain.Empty)
+          scrutineeValue
+          scrutineeValue'
           _
           (Pattern _ Wildcard)
           (Builtin.Equals type_ value1 value2) -> do
-            unificationResult <- try $ Indices.unify context Flexibility.Rigid value1 value2
+            unificationResult <- try $ do
+              putText "equating equality"
+              context' <- Equation.equate context Flexibility.Rigid value1 value2
+              putText "equating equality refl"
+              Equation.equate context' Flexibility.Rigid scrutineeValue' $ Builtin.Refl type_ value1 value2
             case unificationResult of
-              Left Indices.Nope ->
-                check
-                  context
-                  config {clauses = drop 1 config.clauses}
-                  Postponement.CanPostpone
-              Left Indices.Dunno ->
+              Left Equation.Nope -> do
+                putText "nope"
+                check context config {clauses = drop 1 config.clauses} Postponement.CanPostpone
+              Left Equation.Dunno -> do
+                putText "dunno"
                 splitEqualityOr context config matches' k
               Right context' -> do
-                context'' <- Context.define context' var $ Builtin.Refl type_ value1 value2
-                result <- check context'' config Postponement.CanPostpone
-                scrutinee <- Elaboration.readback context'' $ Domain.var var
+                putText "yes"
+                result <- check context' config Postponement.CanPostpone
+                scrutinee <- Elaboration.readback context' scrutineeValue
                 pure $
                   Syntax.Case
                     scrutinee
@@ -994,15 +929,28 @@ splitEqualityOr context config matches k =
           splitEqualityOr context config matches' k
 
 -------------------------------------------------------------------------------
+-- TODO use Core.TypeOf.typeOfHead
+typeOfHead :: Context v -> Domain.Head -> M Domain.Type
+typeOfHead context hd =
+  case hd of
+    Domain.Var var ->
+      pure $ Context.lookupVarType var context
+    Domain.Global global -> do
+      type_ <- fetch $ Query.ElaboratedType global
+      Evaluation.evaluate Environment.empty type_
+    Domain.Meta index -> do
+      solution <- Context.lookupMeta context index
+      Evaluation.evaluate Environment.empty $ Meta.entryType solution
 
 uninhabitedScrutinee :: Context v -> Domain.Value -> M Bool
 uninhabitedScrutinee context value = do
   value' <- Context.forceHead context value
   case value' of
-    Domain.Neutral (Domain.Var var) (Domain.Apps args) -> do
-      let varType = Context.lookupVarType var context
-      type_ <- Context.instantiateType context varType args
-      uninhabitedType context 1 (EnumMap.findWithDefault mempty var context.coveredConstructors) type_
+    Domain.Neutral head_ spine@(Domain.Apps args) -> do
+      headType_ <- typeOfHead context head_
+      type_ <- Context.instantiateType context headType_ args
+      covered <- Context.coveredConstructors context head_ spine
+      uninhabitedType context 1 covered type_
     Domain.Con constr constructorArgs -> do
       constrType <- fetch $ Query.ConstructorType constr
       let args = snd <$> drop (Telescope.length constrType) (toList constructorArgs)
@@ -1016,15 +964,16 @@ uninhabitedType
   -> HashSet Name.QualifiedConstructor
   -> Domain.Type
   -> M Bool
-uninhabitedType context fuel coveredConstructors type_ = do
+uninhabitedType context fuel covered type_ = do
   type' <- Context.forceHead context type_
   case type' of
     Builtin.Equals _ value1 value2 -> do
-      result <- try $ Indices.unify context Flexibility.Rigid value1 value2
+      putText "equating for uninhabited type"
+      result <- try $ Equation.equate context Flexibility.Rigid value1 value2
       pure $ case result of
-        Left Indices.Nope ->
+        Left Equation.Nope ->
           True
-        Left Indices.Dunno ->
+        Left Equation.Dunno ->
           False
         Right _ ->
           False
@@ -1044,7 +993,7 @@ uninhabitedType context fuel coveredConstructors type_ = do
 
                   uncoveredConstructorTypes =
                     toList $
-                      OrderedHashMap.differenceFromMap qualifiedConstructors (HashSet.toMap coveredConstructors)
+                      OrderedHashMap.differenceFromMap qualifiedConstructors (HashSet.toMap covered)
 
               allM (uninhabitedConstrType context fuel) uncoveredConstructorTypes
             _ ->
diff --git a/src/Elaboration/Unification.hs b/src/Elaboration/Unification.hs
index a3966f2..e43d3e3 100644
--- a/src/Elaboration/Unification.hs
+++ b/src/Elaboration/Unification.hs
@@ -1,6 +1,5 @@
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE DuplicateRecordFields #-}
-{-# LANGUAGE OverloadedRecordDot #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -28,7 +27,6 @@ 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
 import qualified Error
 import Extra
@@ -330,6 +328,11 @@ unifySpines context flexibility spine1 spine2 =
     _ ->
       throwIO $ Error.TypeMismatch mempty
 
+equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool
+equalSpines context spine1 spine2 =
+  (True <$ unifySpines context Flexibility.Flexible spine1 spine2)
+    `catch` \(_ :: Error.Elaboration) -> pure False
+
 unifyBranches
   :: Context v
   -> Flexibility
@@ -606,10 +609,9 @@ checkSolution outerContext meta vars value = do
         PartialRenaming
           { occurs = Just meta
           , environment =
-              Environment
-                { indices = Index.Map indices
-                , values = outerContext.values
-                , glueableBefore = Index $ IntSeq.length indices
+              (Context.toEnvironment outerContext)
+                { Environment.indices = Index.Map indices
+                , Environment.glueableBefore = Index $ IntSeq.length indices
                 }
           , renamingFlexibility = Flexibility.Rigid
           }
@@ -642,10 +644,9 @@ addAndRenameLambdas outerContext meta plicities vars term =
             PartialRenaming
               { occurs = Just meta
               , environment =
-                  Environment
-                    { indices = Index.Map vars'
-                    , values = outerContext.values
-                    , glueableBefore = Index $ IntSeq.length vars'
+                  (Context.toEnvironment outerContext)
+                    { Environment.indices = Index.Map vars'
+                    , Environment.glueableBefore = Index $ IntSeq.length vars'
                     }
               , renamingFlexibility = Flexibility.Rigid
               }
@@ -706,7 +707,7 @@ renameValue outerContext renaming value = do
           if EnumSet.member occursMeta metas
             then -- The meta solution might contain `occurs`, so we need to force.
               renameValue outerContext renaming value''
-            else -- The solved meta (`meta`) does contain the meta we're solving
+            else -- The solved meta (`meta`) doesn't contain the meta we're solving
             -- (`occursMeta`) in scope, so we can try without unfolding
             -- `meta`.
 
diff --git a/src/Elaboration/Unification.hs-boot b/src/Elaboration/Unification.hs-boot
new file mode 100644
index 0000000..e8996f6
--- /dev/null
+++ b/src/Elaboration/Unification.hs-boot
@@ -0,0 +1,8 @@
+module Elaboration.Unification where
+
+import  Elaboration.Context.Type
+import Monad
+import Protolude
+import qualified Core.Domain as Domain
+
+equalSpines :: Context v -> Domain.Spine -> Domain.Spine -> M Bool
diff --git a/src/Elaboration/Unification/Indices.hs b/src/Elaboration/Unification/Indices.hs
deleted file mode 100644
index fb4db05..0000000
--- a/src/Elaboration/Unification/Indices.hs
+++ /dev/null
@@ -1,392 +0,0 @@
-{-# LANGUAGE BlockArguments #-}
-{-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE OverloadedRecordDot #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE NoFieldSelectors #-}
-
-module Elaboration.Unification.Indices where
-
-import Control.Exception.Lifted
-import qualified Core.Binding as Binding
-import Core.Bindings (Bindings)
-import qualified Core.Bindings as Bindings
-import qualified Core.Domain as Domain
-import qualified Core.Evaluation as Evaluation
-import qualified Core.Syntax as Syntax
-import qualified Data.EnumMap as EnumMap
-import qualified Data.IntSeq as IntSeq
-import qualified Data.OrderedHashMap as OrderedHashMap
-import qualified Data.Tsil as Tsil
-import Elaboration.Context (Context)
-import qualified Elaboration.Context as Context
-import qualified Environment
-import Flexibility (Flexibility)
-import qualified Flexibility
-import Index
-import qualified Index.Map
-import Monad
-import Name (Name)
-import Protolude hiding (catch, force, throwIO)
-import Telescope (Telescope)
-import qualified Telescope
-import Var
-
-data Error
-  = Nope
-  | Dunno
-  deriving (Eq, Ord, Show, Exception)
-
-data UnificationState v = UnificationState
-  { context :: !(Context v)
-  , touchableBefore :: !(Index (Succ v))
-  }
-
-type Unify v = StateT (UnificationState v) M
-
-unify :: Context v -> Flexibility -> Domain.Value -> Domain.Value -> M (Context v)
-unify context flexibility value1 value2 =
-  (.context)
-    <$> execStateT
-      (unifyM flexibility value1 value2)
-      UnificationState
-        { context = context
-        , touchableBefore = Index.Zero
-        }
-
-isTouchable :: Var -> Unify v Bool
-isTouchable 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
-extend name type_ k = do
-  st <- get
-  (result, st') <- lift do
-    (context', var) <- Context.extend st.context name type_
-    runStateT (k var) st {context = context', touchableBefore = Index.Succ st.touchableBefore}
-  put st' {context = unextend st'.context, touchableBefore = st.touchableBefore}
-  pure result
-
-unextend :: Context (Succ v) -> Context v
-unextend context =
-  case (context.indices, context.boundVars) of
-    (indices Index.Map.:> var, boundVars IntSeq.:> _) ->
-      context
-        { Context.varNames = EnumMap.delete var context.varNames
-        , Context.indices = indices
-        , Context.types = EnumMap.delete var context.types
-        , Context.boundVars = boundVars
-        }
-    _ ->
-      panic "Unification.Indices.unextend"
-
-contextual1 :: (Context v -> a -> M b) -> a -> Unify 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 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
-  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
-          unifySpines 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
-      | 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 ->
-          unifySpines Flexibility.Flexible spine1 spine2 `catch` \(_ :: Error) ->
-            unifyM flexibility value1'' value2''
-    (Domain.Glued _ _ value1'', _) ->
-      unifyM flexibility value1'' value2'
-    (_, Domain.Glued _ _ value2'') ->
-      unifyM flexibility value1' value2''
-    (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
-          unifyM flexibility domain2 domain1
-          extend (Binding.toName binding1) domain1 \var -> do
-            target1 <- lift $ Evaluation.evaluateClosure targetClosure1 $ Domain.var var
-            unifyM flexibility target1 target2
-    (Domain.Fun domain1 plicity1 target1, Domain.Pi binding2 domain2 plicity2 targetClosure2)
-      | plicity1 == plicity2 -> do
-          unifyM flexibility domain2 domain1
-          extend (Binding.toName binding2) domain2 \var -> do
-            target2 <- lift $ Evaluation.evaluateClosure targetClosure2 $ Domain.var var
-            unifyM flexibility target1 target2
-    (Domain.Fun domain1 plicity1 target1, Domain.Fun domain2 plicity2 target2)
-      | plicity1 == plicity2 -> do
-          unifyM flexibility domain2 domain1
-          unifyM flexibility target1 target2
-
-    -- Eta expand
-    (Domain.Lam bindings1 type1 plicity1 closure1, v2) ->
-      extend (Bindings.toName bindings1) type1 \var -> do
-        let varValue = Domain.var var
-        body1 <- lift $ Evaluation.evaluateClosure closure1 varValue
-        body2 <- lift $ Evaluation.apply v2 plicity1 varValue
-        unifyM 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
-
-    -- Vars
-    (Domain.Neutral (Domain.Var var1) Domain.Empty, _)
-      | Flexibility.Rigid <- flexibility ->
-          solve var1 value2'
-    (_, Domain.Neutral (Domain.Var var2) Domain.Empty)
-      | Flexibility.Rigid <- flexibility ->
-          solve var2 value1'
-    _ ->
-      throwIO Dunno
-  where
-    unifyAbstraction name type1 closure1 type2 closure2 = do
-      unifyM 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
-
-    solve var value = do
-      touchable <- isTouchable var
-      if touchable
-        then do
-          occurs var Flexibility.Rigid value
-          context' <- contextual2 Context.define var value
-          modify \st -> st {context = context'}
-        else throwIO Dunno
-
-unifySpines
-  :: Flexibility
-  -> Domain.Spine
-  -> Domain.Spine
-  -> Unify v ()
-unifySpines 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
-    _ ->
-      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
-withInstantiatedTele env tele k =
-  case tele of
-    Telescope.Empty body -> do
-      body' <- lift $ Evaluation.evaluate env body
-      k body'
-    Telescope.Extend bindings type_ _plicity tele' -> do
-      type' <- lift $ Evaluation.evaluate env type_
-      extend (Bindings.toName bindings) type' \var ->
-        withInstantiatedTele (Environment.extendVar env var) tele' k
-
-occurs :: Var -> Flexibility -> Domain.Value -> Unify v ()
-occurs occ flexibility value = do
-  value' <- contextual1 Context.forceHeadGlue value
-  case value' of
-    Domain.Neutral hd spine -> do
-      occursHead occ flexibility hd
-      Domain.mapM_ (occursElimination occ (max (Domain.headFlexibility hd) flexibility)) spine
-    Domain.Con _ args ->
-      mapM_ (occurs occ flexibility . snd) args
-    Domain.Lit _ ->
-      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.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
-      occurs occ flexibility domain
-      occurs occ flexibility target
-  where
-    occursAbstraction name type_ closure = do
-      occurs occ flexibility type_
-      extend name type_ \var -> do
-        let varValue = Domain.var var
-        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
-          unless touchable $
-            throwIO case flexibility of
-              Flexibility.Rigid -> Nope
-              Flexibility.Flexible -> Dunno
-    Domain.Global _ -> pure ()
-    Domain.Meta _ -> pure ()
-
-occursElimination
-  :: Var
-  -> Flexibility
-  -> Domain.Elimination
-  -> Unify 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 occ flexibility (Domain.Branches outerEnv branches defaultBranch) = do
-  case branches of
-    Syntax.ConstructorBranches _ constructorBranches ->
-      forM_ constructorBranches $ mapM_ $ occursTele outerEnv
-    Syntax.LiteralBranches literalBranches ->
-      forM_ literalBranches $
-        mapM_ \branch ->
-          occursTele outerEnv $ Telescope.Empty branch
-  forM_ defaultBranch \branch ->
-    occursTele outerEnv $ Telescope.Empty branch
-  where
-    occursTele
-      :: Domain.Environment v1
-      -> Telescope Bindings Syntax.Type Syntax.Term v1
-      -> Unify v ()
-    occursTele env tele =
-      case tele of
-        Telescope.Extend bindings type_ _plicity tele' -> do
-          type' <- lift $ Evaluation.evaluate env type_
-          occurs occ flexibility type'
-          extend (Bindings.toName bindings) type' \var ->
-            occursTele
-              (Environment.extendVar env var)
-              tele'
-        Telescope.Empty body -> do
-          body' <- lift $ Evaluation.evaluate env body
-          occurs occ flexibility body'
diff --git a/tests/singles/type-checking/case-of-meta.vix b/tests/singles/type-checking/case-of-meta.vix
index 0b161af..e199e7f 100644
--- a/tests/singles/type-checking/case-of-meta.vix
+++ b/tests/singles/type-checking/case-of-meta.vix
@@ -5,6 +5,6 @@ f =
   let x : Bool
       x = _ -- unsolved meta error expected
   in
-  case x of
-    False -> True
-    True -> False
+  case x of -- indeterminate index unification error expected
+    False -> True -- redundant match error expected
+    True -> False -- redundant match error expected
diff --git a/tests/singles/type-checking/case-pattern-scrutinee.vix b/tests/singles/type-checking/case-pattern-scrutinee.vix
index 6d072d8..6ed6200 100644
--- a/tests/singles/type-checking/case-pattern-scrutinee.vix
+++ b/tests/singles/type-checking/case-pattern-scrutinee.vix
@@ -15,25 +15,25 @@ zipWithCase f as bs =
     MkTuple (Cons a as') (Cons b bs') -> Cons (f a b) (zipWithCase f as' bs')
     MkTuple Nil Nil -> Nil
 
-zipWithTuple : forall a b c n. (a -> b -> c) -> Tuple (Vector n a) (Vector n b) -> Vector n c
-zipWithTuple f (MkTuple Nil Nil) = Nil
-zipWithTuple f (MkTuple (Cons a as') (Cons b bs')) = Cons (f a b) (zipWithTuple f (MkTuple as' bs'))
+-- zipWithTuple : forall a b c n. (a -> b -> c) -> Tuple (Vector n a) (Vector n b) -> Vector n c
+-- zipWithTuple f (MkTuple Nil Nil) = Nil
+-- zipWithTuple f (MkTuple (Cons a as') (Cons b bs')) = Cons (f a b) (zipWithTuple f (MkTuple as' bs'))
 
-data List a = Nil | Cons a (List a)
+-- data List a = Nil | Cons a (List a)
 
-zipWithListCase : forall a b c. (a -> b -> c) -> List a -> List b -> List c
-zipWithListCase f as bs =
-  case MkTuple as bs of
-    MkTuple (Cons a as') (Cons b bs') -> case as of
-      Cons _ _ -> Cons (f a b) (zipWithListCase f as' bs')
-      -- as is a Cons cell, so no Nil case
-    MkTuple _ _ -> Nil
+-- zipWithListCase : forall a b c. (a -> b -> c) -> List a -> List b -> List c
+-- zipWithListCase f as bs =
+--   case MkTuple as bs of
+--     MkTuple (Cons a as') (Cons b bs') -> case as of
+--       Cons _ _ -> Cons (f a b) (zipWithListCase f as' bs')
+--       -- as is a Cons cell, so no Nil case
+--     MkTuple _ _ -> Nil
 
-zipWithListCaseLet : forall a b c. (a -> b -> c) -> List a -> List b -> List c
-zipWithListCaseLet f as bs =
-  let x = MkTuple as bs in
-  case x of
-    MkTuple (Cons a as') (Cons b bs') -> case as of
-      Cons _ _ -> Cons (f a b) (zipWithListCase f as' bs')
-      -- as is a Cons cell, so no Nil case
-    MkTuple _ _ -> Nil
+-- zipWithListCaseLet : forall a b c. (a -> b -> c) -> List a -> List b -> List c
+-- zipWithListCaseLet f as bs =
+--   let x = MkTuple as bs in
+--   case x of
+--     MkTuple (Cons a as') (Cons b bs') -> case as of
+--       Cons _ _ -> Cons (f a b) (zipWithListCase f as' bs')
+--       -- as is a Cons cell, so no Nil case
+--     MkTuple _ _ -> Nil