diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -6,6 +6,21 @@
 and this project adheres to the
 [Haskell Package Versioning Policy](https://pvp.haskell.org/).
 
+## v0.11.2 — 2026-08-20
+
+A maintenance release. Checking no longer stops at the first declaration that fails, errors are reported at the sub-term rather than at the enclosing declaration, and a lemma stated over a motive is offered as a hole candidate, so an eliminator written in the sHoTT style is visible as a move.
+
+Changed:
+
+- **Checking continues past a declaration that fails** (see [#336](https://github.com/rzk-lang/rzk/pull/336), [#337](https://github.com/rzk-lang/rzk/pull/337)). A file used to stop at its first bad definition, so one mistake hid every later one; each declaration is now checked on its own and every error is reported. What a failing command recorded is kept rather than discarded, which is what makes the later declarations checkable at all.
+- **A type error is reported where the offending sub-term is** (see [#336](https://github.com/rzk-lang/rzk/pull/336)), not at the enclosing `#!rzk #define`. An untyped term now carries its source position for this, so a tool that draws a squiggle can mark the term at fault instead of the whole declaration.
+
+Fixed:
+
+- **A lemma whose result type is a motive application is offered as a hole candidate** (see [#338](https://github.com/rzk-lang/rzk/pull/338)). A spine such as `#!rzk ind-path ? ? ? ? ? ?` has the type `#!rzk ?C ?x ?p`, an application headed by a hole. Such a type has no shape to mismatch with — filling the head decides what it is — so it now unifies with any goal while probing candidates, and the lemma is offered like any other. Previously only the built-in `#!rzk idJ` was suggested at an identity goal, and every eliminator written in the sHoTT style (`#!rzk ind-path`, a library `#!rzk ind-Void`, an `#!rzk ind-hom2`) was invisible as a move even when explicitly allow-listed. The allow-list still gates the suggestion, and a hole-headed spine is a suggestion rather than a solution: the motive and the base case are left as holes and the written term is type-checked as usual.
+- **Holes are not errors again in the LSP** (see [#336](https://github.com/rzk-lang/rzk/pull/336)), so an in-progress proof with a `#!rzk ?` in it reports its goal rather than a failure.
+- **The formatter no longer deletes a file's final newline** (see [#335](https://github.com/rzk-lang/rzk/pull/335)). Formatting now indexes the lines and tokens it works over instead of rescanning them, which is what let the last newline go missing.
+
 ## v0.11.1 — 2026-07-25
 
 This release adds higher inductive types: a `#!rzk #data` constructor may now return an identity type, declaring a path, and the generated eliminators gain one method and one propositional computation rule per path constructor. Declarations may re-ascribe the type of a generated eliminator or computation rule with a definitionally equal spelling of their own, which is what makes the generated types readable through a library `#!rzk transport`/`#!rzk ap`/`#!rzk apd`. Modal `#!rzk let mod` gains an explicit motive, and the playground deploys are fixed.
diff --git a/rzk.cabal b/rzk.cabal
--- a/rzk.cabal
+++ b/rzk.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           rzk
-version:        0.11.1
+version:        0.11.2
 synopsis:       An experimental proof assistant for synthetic ∞-categories
 description:    Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
 category:       Dependent Types
@@ -154,6 +154,8 @@
     test/typecheck/cases/ill-recor-as-tope.rzk
     test/typecheck/cases/ill-recor-coverage-required.rzk
     test/typecheck/cases/ill-recor-guard-disjoint.rzk
+    test/typecheck/cases/ill-recover-after-body-error.rzk
+    test/typecheck/cases/ill-recover-after-type-error.rzk
     test/typecheck/cases/ill-render-latex-define.rzk
     test/typecheck/cases/ill-repeated-binder-lambda.rzk
     test/typecheck/cases/ill-repeated-binder-pair.rzk
@@ -338,6 +340,8 @@
     test/typecheck/cases/ill-recor-as-tope.expect.yaml
     test/typecheck/cases/ill-recor-coverage-required.expect.yaml
     test/typecheck/cases/ill-recor-guard-disjoint.expect.yaml
+    test/typecheck/cases/ill-recover-after-body-error.expect.yaml
+    test/typecheck/cases/ill-recover-after-type-error.expect.yaml
     test/typecheck/cases/ill-render-latex-define.expect.yaml
     test/typecheck/cases/ill-repeated-binder-lambda.expect.yaml
     test/typecheck/cases/ill-repeated-binder-pair.expect.yaml
diff --git a/src/Language/Rzk/Foil/Convert.hs b/src/Language/Rzk/Foil/Convert.hs
--- a/src/Language/Rzk/Foil/Convert.hs
+++ b/src/Language/Rzk/Foil/Convert.hs
@@ -27,7 +27,7 @@
 -- they can be shown back to the user.
 module Language.Rzk.Foil.Convert where
 
-import           Control.Monad.Foil       (Distinct, NameBinder, NameMap, Scope)
+import           Control.Monad.Foil       (Distinct, NameMap, Scope)
 import qualified Control.Monad.Foil       as Foil
 import           Control.Monad.Foil.Internal (NameMap (..))
 import           Control.Monad.Free.Foil  (AST (..), ScopedAST (..))
@@ -41,8 +41,10 @@
 import           Unsafe.Coerce            (unsafeCoerce)
 
 import           Language.Rzk.Foil.Syntax
-import           Language.Rzk.Foil.Names (Binder (..), Display, TModality (..),
-                                           VarIdent, holeName, toBinder, varIdent)
+import           Language.Rzk.Foil.Names (Binder (..), Display,
+                                           RzkPosition (RzkPosition),
+                                           TModality (..), VarIdent, holeName,
+                                           toBinder, varIdent)
 import qualified Language.Rzk.Foil.Names as Free
 import qualified Language.Rzk.Syntax      as Rzk
 
@@ -65,7 +67,7 @@
   :: Distinct n
   => Scope n -> Rzk.Pattern -> Env n
   -> (forall l. Distinct l => Scope l -> Env l -> Term l)
-  -> ScopedAST NameBinder TermSig n
+  -> ScopedTerm n
 toScopedPatternWith scope pat env k =
   Foil.withFresh scope $ \binder ->
     let scope' = Foil.extendScope binder scope
@@ -78,14 +80,14 @@
 -- | Enter a pattern binder over a surface body.
 toScopedPattern
   :: Distinct n
-  => Scope n -> Rzk.Pattern -> Env n -> Rzk.Term -> ScopedAST NameBinder TermSig n
+  => Scope n -> Rzk.Pattern -> Env n -> Rzk.Term -> ScopedTerm n
 toScopedPattern scope pat env body =
   toScopedPatternWith scope pat env (\scope' env' -> toTerm scope' env' body)
 
 -- | Enter an anonymous binder (a non-dependent function type binds nothing).
 toScopedAnon
   :: Distinct n
-  => Scope n -> Env n -> Rzk.Term -> ScopedAST NameBinder TermSig n
+  => Scope n -> Env n -> Rzk.Term -> ScopedTerm n
 toScopedAnon scope env body =
   Foil.withFresh scope $ \binder ->
     let scope' = Foil.extendScope binder scope
@@ -115,8 +117,26 @@
       , "  " <> Rzk.printTree suggestion
       ]
 
+    -- Every node is tagged with where it was written, so that a diagnostic
+    -- points at the sub-term it is about rather than at the declaration around
+    -- it.
+    --
+    -- A node with no position of its own is left with whatever the conversion
+    -- of its body found. Desugaring builds surface nodes and hands them back to
+    -- 'go', and not all of them carry a position: the λ that @addParams@ wraps
+    -- a definition's body in is spelled nowhere, and overwriting the body's
+    -- position with its absence would put every such error back on the
+    -- declaration line.
+    --
+    -- The file is not recorded here: a term is converted while checking a known
+    -- module, and the diagnostic takes the path from the context around it.
     go :: Rzk.Term -> Term n
-    go = \case
+    go term = case Rzk.hasPosition term of
+      Nothing  -> go' term
+      Just pos -> atSrcPos (RzkPosition Nothing (Just pos)) (go' term)
+
+    go' :: Rzk.Term -> Term n
+    go' = \case
       -- ASCII aliases are desugared exactly as before.
       Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)
       Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)
diff --git a/src/Language/Rzk/Foil/Print.hs b/src/Language/Rzk/Foil/Print.hs
--- a/src/Language/Rzk/Foil/Print.hs
+++ b/src/Language/Rzk/Foil/Print.hs
@@ -269,7 +269,7 @@
 --
 -- (free-foil's own @freeVarsOf@ would do, but it is not in the 0.2.0 release --
 -- it is one of the unreleased helpers on free-foil's @main@.)
-scopeUsesItsBinder :: ScopedAST Foil.NameBinder TermSig n -> Bool
+scopeUsesItsBinder :: ScopedTerm n -> Bool
 scopeUsesItsBinder (ScopedAST binder body) =
   Foil.nameId (Foil.nameOf binder) `elem` nameIdsOf body
 
diff --git a/src/Language/Rzk/Foil/Syntax.hs b/src/Language/Rzk/Foil/Syntax.hs
--- a/src/Language/Rzk/Foil/Syntax.hs
+++ b/src/Language/Rzk/Foil/Syntax.hs
@@ -60,8 +60,9 @@
 import qualified GHC.Generics                   as GHC
 import           Unsafe.Coerce                  (unsafeCoerce)
 
-import           Language.Rzk.Foil.Names        (Binder (..), TModality (..),
-                                                 TypeInfo (..), VarIdent)
+import           Language.Rzk.Foil.Names        (Binder (..), RzkPosition (..),
+                                                 TModality (..), TypeInfo (..),
+                                                 VarIdent)
 
 -- * The signature
 --
@@ -199,10 +200,30 @@
   zipMatchWithK (f :^: M0) (TypeInfo t1 _ _) (TypeInfo t2 _ _) =
     Just (TypeInfo (maybe (error "ZipMatchK TypeInfo: annotation forced") id (f t1 t2)) Nothing Nothing)
 
+-- | Where a term was written.
+--
+-- This is the annotation of an /untyped/ term, so that a diagnostic can point
+-- at the sub-term it is about rather than at the declaration around it (issue
+-- #81). It is a phantom in the node's term parameter: the annotation machinery
+-- wants a functor of the term, and a position holds no terms.
+newtype SrcPos term = SrcPos RzkPosition
+  deriving (Functor, Foldable, Traversable)
+
+-- | Two terms written in different places are the same term, so a position is
+-- ignored in matching, as a node's type is.
+instance ZipMatchK SrcPos where
+  zipMatchWithK _ (SrcPos pos) _ = Just (SrcPos pos)
+
+-- | No position: what a node the checker builds itself carries, and what a node
+-- gets until the conversion from the surface syntax puts the real one on it.
+noSrcPos :: SrcPos term
+noSrcPos = SrcPos (RzkPosition Nothing Nothing)
+
 -- * Terms
 
--- | An untyped term: the surface syntax, elaborated but without annotations.
-type Term = AST NameBinder TermSig
+-- | An untyped term: the surface syntax, elaborated, every node carrying where
+-- it was written.
+type Term = AST NameBinder (AnnSig SrcPos TermSig)
 
 -- | A typed term: every node carries its type. The successor of @TermT@.
 type TermT = AST NameBinder (AnnSig TypeInfo TermSig)
@@ -211,8 +232,33 @@
 type ScopedTermT = ScopedAST NameBinder (AnnSig TypeInfo TermSig)
 
 -- | A scope of an untyped term.
-type ScopedTerm = ScopedAST NameBinder TermSig
+type ScopedTerm = ScopedAST NameBinder (AnnSig SrcPos TermSig)
 
+-- | Record where a term was written, unless it is already recorded.
+--
+-- The conversion tags a node after converting what is under it, and desugaring
+-- hands surface nodes back to the conversion carrying the position of the node
+-- they came from. A node that already knows where it was written therefore
+-- learnt it from something more specific, and keeps it: the λ that a
+-- definition's parameters are wrapped in reuses the λ's own position as it
+-- peels them off, and would otherwise claim every diagnostic in the body.
+--
+-- A variable carries no node of its own, so it is returned unchanged; where a
+-- variable occurrence was written is on its 'VarIdent' instead.
+atSrcPos :: RzkPosition -> Term n -> Term n
+atSrcPos pos t@(Node (AnnSig (SrcPos old) sig))
+  | Nothing <- rzkLineCol old = Node (AnnSig (SrcPos pos) sig)
+  | otherwise                 = t
+atSrcPos _ t@(Var _)          = t
+
+-- | Where the term was written, when it came from a file.
+positionOfTerm :: Term n -> Maybe RzkPosition
+positionOfTerm (Var _)                        = Nothing
+positionOfTerm (Node (AnnSig (SrcPos pos) _)) =
+  case rzkLineCol pos of
+    Nothing -> Nothing
+    Just _  -> Just pos
+
 -- | The annotation of a node: its type, and its memoised normal forms. A
 -- variable carries none — its type lives in the context.
 typeInfoOf :: TermT n -> Maybe (TypeInfo (TermT n))
@@ -222,7 +268,7 @@
 -- | Drop every annotation, for printing and for the surface-facing API.
 untyped :: TermT n -> Term n
 untyped (Var name)              = Var name
-untyped (Node (AnnSig _ann sig)) = Node (bimap untypedScoped untyped sig)
+untyped (Node (AnnSig _ann sig)) = UntypedNode (bimap untypedScoped untyped sig)
   where
     untypedScoped (ScopedAST binder body) = ScopedAST binder (untyped body)
 
@@ -275,7 +321,7 @@
 -- makes the coercion back to the outer scope right.
 freeVarsOfTerm :: Term n -> [Foil.Name n]
 freeVarsOfTerm (Var x)    = [x]
-freeVarsOfTerm (Node sig) = bifoldMap freeVarsOfScoped freeVarsOfTerm sig
+freeVarsOfTerm (UntypedNode sig) = bifoldMap freeVarsOfScoped freeVarsOfTerm sig
   where
     freeVarsOfScoped :: ScopedTerm n' -> [Foil.Name n']
     freeVarsOfScoped (ScopedAST binder body) =
@@ -296,7 +342,7 @@
 containsUniverse :: Term n -> Bool
 containsUniverse Universe   = True
 containsUniverse (Var _)    = False
-containsUniverse (Node sig) =
+containsUniverse (UntypedNode sig) =
   bifoldr (\scoped acc -> containsUniverseScoped scoped || acc)
           (\t acc -> containsUniverse t || acc) False sig
   where
@@ -308,11 +354,25 @@
 isHoleT HoleT{} = True
 isHoleT _       = False
 
+-- | Is the term a /flexible/ spine: a hole, or an application headed by one
+-- (@? a b@)?
+--
+-- Such a term is not yet committed to any shape: filling the head hole can turn
+-- it into anything. A type of this form therefore stands for an arbitrary type,
+-- which is what lets an eliminator whose result type is a motive application
+-- (@ind-path A a C d x p : C x p@) be judged against a concrete goal. Contrast
+-- 'containsHole', which is also true of a term whose /shape/ is already fixed
+-- and only has holes among its parts (@? = ?@ is an identity type either way).
+isHoleHeadedT :: TermT n -> Bool
+isHoleHeadedT HoleT{}     = True
+isHoleHeadedT (AppT _ f _) = isHoleHeadedT f
+isHoleHeadedT _           = False
+
 -- | The name of every hole in a term.
 holeNamesOf :: Term n -> [Maybe VarIdent]
 holeNamesOf (Hole mname) = [mname]
 holeNamesOf (Var _)      = []
-holeNamesOf (Node sig)   = bifoldr (\scoped acc -> holeNamesOfScoped scoped <> acc)
+holeNamesOf (UntypedNode sig) = bifoldr (\scoped acc -> holeNamesOfScoped scoped <> acc)
                                    (\t acc -> holeNamesOf t <> acc) [] sig
   where
     holeNamesOfScoped (ScopedAST _ body) = holeNamesOf body
@@ -520,57 +580,68 @@
 
 -- ** Untyped patterns
 --
--- The same constructors on 'Term' (no annotation), for the surface conversions
--- and the printer.
+-- The same constructors on 'Term', for the surface conversions and the printer.
+--
+-- Each goes through 'UntypedNode', which ignores a node's position on the way in
+-- and leaves it unset on the way out. So the checker builds and matches untyped
+-- terms exactly as it did before terms carried a position, and the conversion
+-- from the surface syntax ('atSrcPos') is the only place that puts a real one on.
 
-pattern Universe = Node UniverseF
-pattern UniverseCube = Node UniverseCubeF
-pattern UniverseTope = Node UniverseTopeF
-pattern CubeUnit = Node CubeUnitF
-pattern CubeUnitStar = Node CubeUnitStarF
-pattern Cube2 = Node Cube2F
-pattern Cube2_0 = Node Cube2_0F
-pattern Cube2_1 = Node Cube2_1F
-pattern CubeI = Node CubeIF
-pattern CubeI_0 = Node CubeI_0F
-pattern CubeI_1 = Node CubeI_1F
-pattern CubeProduct l r = Node (CubeProductF l r)
-pattern CubeFlip t = Node (CubeFlipF t)
-pattern CubeUnflip t = Node (CubeUnflipF t)
-pattern CubeSup l r = Node (CubeSupF l r)
-pattern CubeInf l r = Node (CubeInfF l r)
-pattern TopeTop = Node TopeTopF
-pattern TopeBottom = Node TopeBottomF
-pattern TopeEQ l r = Node (TopeEQF l r)
-pattern TopeLEQ l r = Node (TopeLEQF l r)
-pattern TopeAnd l r = Node (TopeAndF l r)
-pattern TopeOr l r = Node (TopeOrF l r)
-pattern TopeInv t = Node (TopeInvF t)
-pattern TopeUninv t = Node (TopeUninvF t)
-pattern RecBottom = Node RecBottomF
-pattern RecOr rs = Node (RecOrF rs)
-pattern TypeFun orig md param mtope ret = Node (TypeFunF orig md param mtope ret)
-pattern TypeSigma orig md a b = Node (TypeSigmaF orig md a b)
-pattern TypeId a mtA b = Node (TypeIdF a mtA b)
-pattern App f x = Node (AppF f x)
-pattern Let orig mparam val body = Node (LetF orig mparam val body)
-pattern Lambda orig mparam body = Node (LambdaF orig mparam body)
-pattern Pair l r = Node (PairF l r)
-pattern First t = Node (FirstF t)
-pattern Second t = Node (SecondF t)
-pattern Refl mx = Node (ReflF mx)
-pattern IdJ a b c d e f = Node (IdJF a b c d e f)
-pattern Match scrut mmotive branches = Node (MatchF scrut mmotive branches)
-pattern MatchArm orig arm = Node (MatchArmF orig arm)
-pattern Unit = Node UnitF
-pattern TypeUnit = Node TypeUnitF
-pattern TypeAsc term ty = Node (TypeAscF term ty)
-pattern TypeRestricted ty rs = Node (TypeRestrictedF ty rs)
-pattern TypeModal md ty = Node (TypeModalF md ty)
-pattern ModApp md t = Node (ModAppF md t)
-pattern ModExtract app inn t = Node (ModExtractF app inn t)
-pattern LetMod orig app inn mparam mmotive val body = Node (LetModF orig app inn mparam mmotive val body)
-pattern Hole mname = Node (HoleF mname)
+-- | An untyped node, taken and made without regard for where it was written.
+pattern UntypedNode :: TermSig (ScopedTerm n) (Term n) -> Term n
+pattern UntypedNode sig <- Node (AnnSig _ sig) where
+  UntypedNode sig = Node (AnnSig noSrcPos sig)
+
+{-# COMPLETE Var, UntypedNode #-}
+
+pattern Universe = UntypedNode UniverseF
+pattern UniverseCube = UntypedNode UniverseCubeF
+pattern UniverseTope = UntypedNode UniverseTopeF
+pattern CubeUnit = UntypedNode CubeUnitF
+pattern CubeUnitStar = UntypedNode CubeUnitStarF
+pattern Cube2 = UntypedNode Cube2F
+pattern Cube2_0 = UntypedNode Cube2_0F
+pattern Cube2_1 = UntypedNode Cube2_1F
+pattern CubeI = UntypedNode CubeIF
+pattern CubeI_0 = UntypedNode CubeI_0F
+pattern CubeI_1 = UntypedNode CubeI_1F
+pattern CubeProduct l r = UntypedNode (CubeProductF l r)
+pattern CubeFlip t = UntypedNode (CubeFlipF t)
+pattern CubeUnflip t = UntypedNode (CubeUnflipF t)
+pattern CubeSup l r = UntypedNode (CubeSupF l r)
+pattern CubeInf l r = UntypedNode (CubeInfF l r)
+pattern TopeTop = UntypedNode TopeTopF
+pattern TopeBottom = UntypedNode TopeBottomF
+pattern TopeEQ l r = UntypedNode (TopeEQF l r)
+pattern TopeLEQ l r = UntypedNode (TopeLEQF l r)
+pattern TopeAnd l r = UntypedNode (TopeAndF l r)
+pattern TopeOr l r = UntypedNode (TopeOrF l r)
+pattern TopeInv t = UntypedNode (TopeInvF t)
+pattern TopeUninv t = UntypedNode (TopeUninvF t)
+pattern RecBottom = UntypedNode RecBottomF
+pattern RecOr rs = UntypedNode (RecOrF rs)
+pattern TypeFun orig md param mtope ret = UntypedNode (TypeFunF orig md param mtope ret)
+pattern TypeSigma orig md a b = UntypedNode (TypeSigmaF orig md a b)
+pattern TypeId a mtA b = UntypedNode (TypeIdF a mtA b)
+pattern App f x = UntypedNode (AppF f x)
+pattern Let orig mparam val body = UntypedNode (LetF orig mparam val body)
+pattern Lambda orig mparam body = UntypedNode (LambdaF orig mparam body)
+pattern Pair l r = UntypedNode (PairF l r)
+pattern First t = UntypedNode (FirstF t)
+pattern Second t = UntypedNode (SecondF t)
+pattern Refl mx = UntypedNode (ReflF mx)
+pattern IdJ a b c d e f = UntypedNode (IdJF a b c d e f)
+pattern Match scrut mmotive branches = UntypedNode (MatchF scrut mmotive branches)
+pattern MatchArm orig arm = UntypedNode (MatchArmF orig arm)
+pattern Unit = UntypedNode UnitF
+pattern TypeUnit = UntypedNode TypeUnitF
+pattern TypeAsc term ty = UntypedNode (TypeAscF term ty)
+pattern TypeRestricted ty rs = UntypedNode (TypeRestrictedF ty rs)
+pattern TypeModal md ty = UntypedNode (TypeModalF md ty)
+pattern ModApp md t = UntypedNode (ModAppF md t)
+pattern ModExtract app inn t = UntypedNode (ModExtractF app inn t)
+pattern LetMod orig app inn mparam mmotive val body = UntypedNode (LetModF orig app inn mparam mmotive val body)
+pattern Hole mname = UntypedNode (HoleF mname)
 
 {-# COMPLETE Var, Universe, UniverseCube, UniverseTope, CubeUnit, CubeUnitStar,
   Cube2, Cube2_0, Cube2_1, CubeI, CubeI_0, CubeI_1, CubeProduct, CubeFlip,
diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs
--- a/src/Language/Rzk/VSCode/Handlers.hs
+++ b/src/Language/Rzk/VSCode/Handlers.hs
@@ -76,7 +76,7 @@
 import           Language.Rzk.VSCode.Tokenize  (mergeTokens, tokenizeModule,
                                                 tokenizeSyntaxSymbols)
 import qualified Rzk.Diagnostic                as Diag
-import           Rzk.Format                    (format)
+import qualified Rzk.Format                    as Fmt
 import           Rzk.Project.Config            (ProjectConfig (include))
 import           Rzk.TypeCheck
 import           Text.Read                     (readMaybe)
@@ -135,16 +135,33 @@
 -- buffer when the file is open, from disk otherwise. A file that cannot be
 -- read converts as all-BMP, i.e. the conversion is the identity.
 astralLinesOfFile :: FilePath -> LSP Enc.AstralLines
-astralLinesOfFile path = do
+astralLinesOfFile = fmap Enc.astralLines . sourceOfFile
+
+-- | The text of a file as the client sees it: from the editor buffer when the
+-- file is open, from disk otherwise. A file that cannot be read is empty.
+sourceOfFile :: FilePath -> LSP T.Text
+sourceOfFile path = do
   mdoc <- getVirtualFile (filePathToNormalizedUri path)
   case virtualFileText <$> mdoc of
-    Just text -> return (Enc.astralLines (T.filter (/= '\r') text))
+    Just text -> return (T.filter (/= '\r') text)
     Nothing -> liftIO $ do
       result <- try @SomeException (readFile path)
       return $ case result of
-        Left _    -> Enc.astralLines ""
-        Right src -> Enc.astralLines (T.filter (/= '\r') (T.pack src))
+        Left _    -> ""
+        Right src -> T.filter (/= '\r') (T.pack src)
 
+-- | The lines of a document, by 0-based line number, for reading the token a
+-- diagnostic marks.
+newtype SourceLines = SourceLines (Map.Map Int T.Text)
+
+sourceLinesOf :: T.Text -> SourceLines
+sourceLinesOf src = SourceLines (Map.fromDistinctAscList (zip [0 ..] (T.lines src)))
+
+-- | A line outside the document is empty, as is one in a file that could not be
+-- read; a marking there falls back to a single character.
+lineOf :: SourceLines -> Int -> T.Text
+lineOf (SourceLines ls) line = Map.findWithDefault "" line ls
+
 fromLspPosition :: Enc.AstralLines -> LSP.Position -> RefInd.Position
 fromLspPosition als (LSP.Position l c) =
   RefInd.Position (fromIntegral l)
@@ -249,7 +266,7 @@
           -- /is/ the elaborated prefix, so nothing is replayed or re-elaborated.
           let prefix = case reverse checked of
                 (_, entry) : _ -> cachedModuleChecked entry
-                []             -> emptyChecked
+                []             -> emptyCheckedWithHoles
           tcResult <- liftIO $ tryTypecheck $ evaluate $
             recheckFrom prefix [(path, module_)]
           case tcResult of
@@ -293,20 +310,30 @@
     -- max count of 0 forces an empty publish to the client, clearing it.
     publishModuleDiagnostics :: FilePath -> [TypeErrorInScopedContext] -> [CheckWarning] -> [HoleInfo] -> LSP ()
     publishModuleDiagnostics path typeErrors warnings holeInfos = do
-      let errDiagnostics  = [ (filepathOfTypeError err, [diagnosticOfTypeError err])
+      let errDiagnostics  = [ (filepathOfTypeError err, [Diag.diagnoseTypeError TopDown err])
                             | err <- typeErrors ]
-          warnDiagnostics = [ (path', [diagnosticOfWarning warning])
+          warnDiagnostics = [ (path', [Diag.diagnoseCheckWarning warning])
                             | warning <- warnings
                             , let path' = fromMaybe path
                                     (warningLocation warning >>= locationFilePath) ]
-          holeDiagnostics = [ (path', [diagnosticOfHole hole])
+          holeDiagnostics = [ (path', [Diag.diagnoseHole hole])
                             | hole <- holeInfos
                             , Just path' <- [holeLocation hole >>= locationFilePath] ]
           diagnosticsByFile = Map.insertWith (flip (<>)) path [] $
             Map.fromListWith (flip (<>)) (errDiagnostics <> warnDiagnostics <> holeDiagnostics)
-      forM_ (Map.toList diagnosticsByFile) $ \(path', diags) ->
-        publishDiagnostics (if null diags then 0 else maxDiagnosticCount)
-          (filePathToNormalizedUri path') Nothing (partitionBySource diags)
+      -- The source of each file with something to report, read once: a
+      -- diagnostic marks the token it points at, and its column is converted
+      -- to the UTF-16 the client counts in.
+      forM_ (Map.toList diagnosticsByFile) $ \(path', diags) -> do
+        lspDiags <- case diags of
+          [] -> return []
+          _  -> do
+            src <- sourceOfFile path'
+            let als = Enc.astralLines src
+                sourceLines = sourceLinesOf src
+            return (map (lspDiagnosticOf als sourceLines) diags)
+        publishDiagnostics (if null lspDiags then 0 else maxDiagnosticCount)
+          (filePathToNormalizedUri path') Nothing (partitionBySource lspDiags)
 
     -- Modules that a run never reaches (they come after a module with an
     -- error, and every rzk module depends on all earlier ones) get a single
@@ -339,11 +366,11 @@
         Just path -> path
         _         -> error "the impossible happened! Please contact Abdelrahman immediately!!!"
 
-    -- Map a structured library diagnostic to an LSP diagnostic. The range is
-    -- line-level (whole line), reflecting the granularity rzk currently retains.
-    lspDiagnosticOf :: Diag.Diagnostic -> Diagnostic
-    lspDiagnosticOf d = Diagnostic
-                      (Range (Position line 0) (Position line 99)) -- 99 to reach end of line and be visible until we actually have column information
+    -- Map a structured library diagnostic to an LSP diagnostic, marking the
+    -- term it is about in the given source.
+    lspDiagnosticOf :: Enc.AstralLines -> SourceLines -> Diag.Diagnostic -> Diagnostic
+    lspDiagnosticOf als sourceLines d = Diagnostic
+                      (Enc.rangeToUtf16 als (diagnosticRange sourceLines d))
                       (Just (lspSeverity (Diag.diagnosticSeverity d)))
                       (Just (InR (T.pack (Diag.diagnosticCode d))))
                       Nothing                   -- diagnostic description
@@ -352,11 +379,42 @@
                       Nothing                   -- tags
                       (Just [])                 -- related information
                       Nothing                   -- data that is preserved between different calls
+
+    -- What the diagnostic marks: the token the term it is about starts with.
+    --
+    -- The checker knows where a term begins and not where it ends (the surface
+    -- syntax records only the start of a node), so the marked span is the head
+    -- token. That puts the squiggle on the right thing without claiming an
+    -- extent that was never measured, and a hole is marked exactly, since @?@
+    -- and @?name@ are the whole term. A diagnostic that has no column is about
+    -- a whole declaration and still marks the line.
+    diagnosticRange :: SourceLines -> Diag.Diagnostic -> Range
+    diagnosticRange sourceLines d = case Diag.diagnosticLocation d of
+      Just loc
+        | Just lineNo <- locationLine loc
+        , Just col <- locationColumn loc
+        , let line = fromIntegral (lineNo - 1)  -- LSP counts lines from 0
+        , let start = fromIntegral (col - 1)    -- and columns too
+        -> Range (Position line start)
+                 (Position line (start + tokenWidth sourceLines line start))
+      Just loc
+        | Just lineNo <- locationLine loc
+        , let line = fromIntegral (lineNo - 1)
+        -> Range (Position line 0) (Position line 99) -- to the end of the line
+      _ -> Range (Position 0 0) (Position 0 99)
+
+    -- The width of the token starting at a position, in code points, and never
+    -- zero: an empty marking shows nothing at all. A token that opens with a
+    -- bracket or a separator is one character wide, since those delimit rather
+    -- than name; anything else runs to the next space or delimiter.
+    tokenWidth :: SourceLines -> UInt -> UInt -> UInt
+    tokenWidth sourceLines line start =
+      case T.drop (fromIntegral start) (lineOf sourceLines (fromIntegral line)) of
+        rest | Just (c, _) <- T.uncons rest, not (isDelimiter c)
+             -> max 1 (fromIntegral (T.length (T.takeWhile (not . isDelimiter) rest)))
+        _    -> 1
       where
-        line = fromIntegral $ fromMaybe 0 $ do
-          loc <- Diag.diagnosticLocation d
-          lineNo <- locationLine loc
-          return (lineNo - 1) -- VS Code indexes lines from 0, but locationLine starts with 1
+        isDelimiter c = c `elem` (" \t()[]{},;" :: String)
 
     lspSeverity :: Diag.Severity -> DiagnosticSeverity
     lspSeverity = \case
@@ -365,15 +423,6 @@
       Diag.SeverityInformation -> DiagnosticSeverity_Information
       Diag.SeverityHint        -> DiagnosticSeverity_Hint
 
-    diagnosticOfTypeError :: TypeErrorInScopedContext -> Diagnostic
-    diagnosticOfTypeError = lspDiagnosticOf . Diag.diagnoseTypeError TopDown
-
-    diagnosticOfHole :: HoleInfo -> Diagnostic
-    diagnosticOfHole = lspDiagnosticOf . Diag.diagnoseHole
-
-    diagnosticOfWarning :: CheckWarning -> Diagnostic
-    diagnosticOfWarning = lspDiagnosticOf . Diag.diagnoseCheckWarning
-
     diagnosticOfParseError :: Enc.AstralLines -> T.Text -> Diagnostic
     diagnosticOfParseError als err = Diagnostic (Enc.rangeToUtf16 als (Range (Position errLine errColumnStart) (Position errLine errColumnEnd)))
                       (Just DiagnosticSeverity_Error)
@@ -478,25 +527,13 @@
     possibleEdits <- case virtualFileText <$> mdoc of
       Nothing         -> return (Left "Failed to get file contents")
       Just sourceCode -> do
+        -- 'fullDocumentRange' spans the trailing newlines too, so the
+        -- replacement carries them: 'formatDocument' keeps as many as the
+        -- source had, and the document is returned with its final newline
+        -- intact.
         let source = T.filter (/= '\r') sourceCode
-            formatted = format source
-            -- Preserve trailing newlines of the source so formatting is idempotent.
-            formatted'
-              | T.null source = formatted
-              | otherwise =
-                  let inputTrailing = T.length (T.takeWhileEnd (== '\n') source)
-                      outTrailing = T.length (T.takeWhileEnd (== '\n') formatted)
-                  in if outTrailing > inputTrailing
-                     then T.dropEnd (outTrailing - inputTrailing) formatted
-                     else if outTrailing < inputTrailing
-                          then formatted <> T.replicate (inputTrailing - outTrailing) (T.singleton '\n')
-                          else formatted
-            -- Never send trailing newlines: some clients add one when applying a
-            -- full-document edit, so we send content ending with no newline to avoid
-            -- an extra blank line on each format.
-            formatted'' = T.dropWhileEnd (== '\n') formatted'
             range = fullDocumentRange source
-        return (Right [TextEdit range formatted''])
+        return (Right [TextEdit range (Fmt.formatDocument source)])
     case possibleEdits of
 #if MIN_VERSION_lsp(2,7,0)
       Left err    -> res $ Left $ TResponseError (InR ErrorCodes_InternalError) err Nothing
@@ -899,7 +936,7 @@
   -- Re-check this file from the context of the prefix before it.
   let prefix = case reverse (takeWhile ((/= path) . fst) cache) of
         (_, entry) : _ -> cachedModuleChecked entry
-        []             -> emptyChecked
+        []             -> emptyCheckedWithHoles
   e <- toExceptTLifted $ try @SomeException $ evaluate $
     recheckFrom prefix [(path, module')]
   (checkedNow, _holes) <- toExceptT $ return e
diff --git a/src/Rzk/Diagnostic.hs b/src/Rzk/Diagnostic.hs
--- a/src/Rzk/Diagnostic.hs
+++ b/src/Rzk/Diagnostic.hs
@@ -93,9 +93,10 @@
 -- | Encode a location as JSON. A plain helper rather than a @ToJSON@ instance,
 -- to avoid an orphan instance ('LocationInfo' is defined in "Rzk.TypeCheck").
 locationToJSON :: LocationInfo -> Value
-locationToJSON (LocationInfo path line) = object
+locationToJSON (LocationInfo path line column) = object
   [ "file" .= path
   , "line" .= line
+  , "column" .= column
   ]
 
 instance ToJSON Diagnostic where
@@ -278,5 +279,7 @@
             | e <- entries ]
 
 ppLocationInfo :: LocationInfo -> String
-ppLocationInfo (LocationInfo mpath mline) =
-  maybe "<input>" id mpath <> maybe "" ((":" <>) . show) mline
+ppLocationInfo (LocationInfo mpath mline mcol) =
+  maybe "<input>" id mpath
+    <> maybe "" ((":" <>) . show) mline
+    <> maybe "" ((":" <>) . show) mcol
diff --git a/src/Rzk/Format.hs b/src/Rzk/Format.hs
--- a/src/Rzk/Format.hs
+++ b/src/Rzk/Format.hs
@@ -18,6 +18,9 @@
   normalizeTabs,
 ) where
 
+import           Data.Array              (Array, listArray, (!))
+import           Data.IntMap.Strict      (IntMap)
+import qualified Data.IntMap.Strict      as IntMap
 import           Data.List               (sort)
 
 import qualified Data.Text               as T
@@ -55,7 +58,10 @@
   , lambdaArrow      :: Bool -- ^ After a lambda '\', in the parameters (to leave its -> on the same line)
   , eqBraceDepth     :: Int  -- ^ Depth inside =_{ ... }; 0 = not inside, 1 = at top level after =_{
   , eqBraceOnOwnLine :: Bool -- ^ True if the current =_{ started at the beginning of its line (after spaces)
-  , allTokens        :: [Token] -- ^ The full array of tokens after resolving the layout
+  , tokensOnLine     :: IntMap [Token]
+    -- ^ All the tokens after resolving the layout, grouped by the line they
+    -- start on. Only one rule needs them, and only those on a single line, so
+    -- they are indexed rather than scanned (see 'lineTokensBefore').
   }
 
 -- | Replace every tab character with a single space.
@@ -68,16 +74,41 @@
 formatTextEdits contents =
   case resolveLayout True (tokens rzkBlocks) of
     Left _err     -> [] -- TODO: log error (in a CLI and LSP friendly way)
-    Right allToks -> go (initialState {allTokens = allToks}) allToks
+    Right allToks -> go (initialState {tokensOnLine = groupByLine allToks}) allToks
   where
-    initialState = FormatState { parensDepth = 0, letDepth  = 0, inDataCommand = False, definingName = False, lambdaArrow = False, eqBraceDepth = 0, eqBraceOnOwnLine = False, allTokens = [] }
+    initialState = FormatState { parensDepth = 0, letDepth  = 0, inDataCommand = False, definingName = False, lambdaArrow = False, eqBraceDepth = 0, eqBraceOnOwnLine = False, tokensOnLine = IntMap.empty }
     incParensDepth s = s { parensDepth = parensDepth s + 1 }
     decParensDepth s = s { parensDepth = 0 `max` (parensDepth s - 1) }
     rzkBlocks = tryExtractMarkdownCodeBlocks "rzk" contents
-    contentLines line = T.lines rzkBlocks !! (line - 1) -- Sorry
-    lineTokensBefore toks line col = filter isBefore toks
+
+    -- Almost every rule reads the line its token sits on, and some read the
+    -- neighbouring ones, so the lines are split once and indexed. Splitting the
+    -- whole document afresh on each lookup made formatting quadratic in the
+    -- file size: sHoTT's largest module took 0.8 s, past the editor's
+    -- format-on-save budget, so saving it looked like it had been refused.
+    sourceLines :: [T.Text]
+    sourceLines = T.lines rzkBlocks
+    lineCount = length sourceLines
+    lineArray :: Array Int T.Text
+    lineArray = listArray (1, lineCount) sourceLines
+
+    -- | The content of a line, by its 1-based number. A line outside the
+    -- document is empty, which is what the rules looking at a neighbour want at
+    -- the first and last line.
+    contentLines line
+      | line >= 1 && line <= lineCount = lineArray ! line
+      | otherwise                      = ""
+
+    groupByLine :: [Token] -> IntMap [Token]
+    groupByLine toks =
+      IntMap.fromListWith (<>) [ (l, [t]) | t@(PT (Pn _ l _) _) <- toks ]
+
+    -- | The tokens preceding a position on its own line. The order within a
+    -- line is not preserved: the one rule that asks only tests them all.
+    lineTokensBefore s line col =
+      filter isBefore (IntMap.findWithDefault [] line (tokensOnLine s))
       where
-        isBefore (PT (Pn _ l c) _) = l == line && c < col
+        isBefore (PT (Pn _ _ c) _) = c < col
         isBefore _                 = False
     unicodeTokens :: [(T.Text, T.Text)]
     unicodeTokens =
@@ -162,7 +193,7 @@
       where
         spaceCol = col + 1
         lineContent = contentLines line
-        precededBySingleCharOnly = all isPunctuation (lineTokensBefore (allTokens s) line col)
+        precededBySingleCharOnly = all isPunctuation (lineTokensBefore s line col)
         singleCharUnicodeTokens = filter (\(_, unicode) -> T.length unicode == 1) unicodeTokens
         punctuations :: [T.Text]
         punctuations = concat
@@ -216,7 +247,7 @@
           | closingEqBrace && onOwnLine && not isLastOnLine
           = [ FormattingEdit line braceEndCol line (braceEndCol + spacesAfter) "\n  " ]
           | closingEqBrace && onOwnLine && isLastOnLine
-          = let nextLine = if line < length (T.lines rzkBlocks) then contentLines (line + 1) else ""
+          = let nextLine = contentLines (line + 1)
                 spacesNextLine = T.length $ T.takeWhile (== ' ') nextLine
             in if spacesNextLine /= 2 then [ FormattingEdit (line + 1) 1 (line + 1) (1 + spacesNextLine) "  " ] else []
           | otherwise
@@ -316,12 +347,8 @@
         spacesAfter = T.length $ T.takeWhile (== ' ') (T.drop (col + T.length tk - 1) lineContent)
         isFirstNonSpaceChar = T.all (== ' ') (T.take (col - 1) lineContent)
         isLastNonSpaceChar = T.all (== ' ') (T.drop (col + T.length tk - 1) lineContent)
-        prevLine
-          | line > 0 = contentLines (line - 1)
-          | otherwise = ""
-        nextLine
-          | line + 1 < length (T.lines rzkBlocks) = contentLines (line + 1)
-          | otherwise = ""
+        prevLine = contentLines (line - 1)
+        nextLine = contentLines (line + 1)
         spacesNextLine = T.length $ T.takeWhile (== ' ') nextLine
         edits = spaceEdits ++ unicodeEdits
         spaceEdits
@@ -382,11 +409,24 @@
   let normalized = normalizeTabs contents
   in applyTextEdits (formatTextEdits normalized) normalized
 
--- | Same as 'format'. Use this when replacing the entire document (e.g. from
---   the language server), so that tab normalization and all formatting rules
---   are applied correctly instead of applying incremental edits to tabbed source.
+-- | Format a whole document, for a consumer that replaces it wholesale (the
+--   language server does, so that tab normalization and all formatting rules
+--   are applied instead of incremental edits to tabbed source).
+--
+--   The document ends in as many newlines as it began with. Formatting is a
+--   rewriting of the code, and whether a file ends in a newline is not
+--   something it has an opinion on: that is the editor's @insert_final_newline@
+--   and whatever else formats the surrounding Markdown. The language server
+--   used to send the document with every trailing newline stripped, which
+--   silently deleted the final one on each save and left the file failing a
+--   @.editorconfig@ or Prettier check that no further formatting could satisfy.
 formatDocument :: T.Text -> T.Text
-formatDocument = format
+formatDocument contents = matchTrailingNewlines contents (format contents)
+
+-- | Give the second text as many trailing newlines as the first one has.
+matchTrailingNewlines :: T.Text -> T.Text -> T.Text
+matchTrailingNewlines source formatted =
+  T.dropWhileEnd (== '\n') formatted <> T.takeWhileEnd (== '\n') source
 
 -- | Format Rzk code from a file
 formatFile :: FilePath -> IO T.Text
diff --git a/src/Rzk/TypeCheck/Context.hs b/src/Rzk/TypeCheck/Context.hs
--- a/src/Rzk/TypeCheck/Context.hs
+++ b/src/Rzk/TypeCheck/Context.hs
@@ -49,8 +49,9 @@
 import           Unsafe.Coerce               (unsafeCoerce)
 
 import           Language.Rzk.Foil.Syntax
-import           Language.Rzk.Foil.Names    (Binder (..), TModality (..),
-                                              VarIdent, binderName)
+import           Language.Rzk.Foil.Names    (Binder (..), RzkPosition (..),
+                                              TModality (..), VarIdent,
+                                              binderName)
 import qualified Language.Rzk.Syntax         as Rzk
 
 -- * The pieces of a context
@@ -70,10 +71,24 @@
   | Silent
   deriving (Eq, Ord)
 
+-- | Where a diagnostic points.
+--
+-- The line and column are the start of whatever the diagnostic is about: the
+-- declaration being checked, narrowed to the sub-term as the checker descends
+-- into it (see @narrowLocation@ in "Rzk.TypeCheck.Monad"). The surface syntax
+-- records the start of a node and not its extent, so there is no end position
+-- to carry.
 data LocationInfo = LocationInfo
   { locationFilePath :: Maybe FilePath
   , locationLine     :: Maybe Int
+  , locationColumn   :: Maybe Int
   } deriving (Eq, Show)
+
+-- | Point a location at a position in the same file.
+atPosition :: RzkPosition -> LocationInfo -> LocationInfo
+atPosition pos loc = case rzkLineCol pos of
+  Nothing          -> loc
+  Just (line, col) -> loc { locationLine = Just line, locationColumn = Just col }
 
 -- | What is known about a hypothesis, local or top-level.
 data VarInfo n = VarInfo
diff --git a/src/Rzk/TypeCheck/Decl.hs b/src/Rzk/TypeCheck/Decl.hs
--- a/src/Rzk/TypeCheck/Decl.hs
+++ b/src/Rzk/TypeCheck/Decl.hs
@@ -25,10 +25,9 @@
 module Rzk.TypeCheck.Decl where
 
 import           Control.Monad             (forM, forM_, unless, when)
-import           Control.Monad.Except      (catchError, runExcept)
+import           Control.Monad.Except      (catchError)
 import           Data.Data                 (Data, cast, gmapQ)
-import           Control.Monad.Reader      (ask, asks, local, runReaderT)
-import           Control.Monad.Trans.Writer.CPS (runWriterT)
+import           Control.Monad.Reader      (ask, asks, local)
 import           Data.List                 (intercalate)
 import qualified Data.Map                  as Map
 import qualified Data.Text                 as T
@@ -1000,7 +999,11 @@
       { ctxCurrentCommand = Just command
       , ctxLocation = updatePosition (Rzk.hasPosition command) <$> ctxLocation ctx
       }
-    updatePosition pos loc = loc { locationLine = fst <$> pos }
+    -- Where the command starts. A judgement made inside it narrows this to the
+    -- sub-term it is about (see @narrowLocation@); this is what an error with
+    -- no sub-term of its own falls back to.
+    updatePosition pos loc =
+      loc { locationLine = fst <$> pos, locationColumn = snd <$> pos }
 
 -- | The binder leaves repeated within one binder /group/ of a surface
 -- command: the parameter list of a λ, of a declaration, or of a constructor
@@ -1060,6 +1063,49 @@
             earlier -> (varIdent v, map varIdent (reverse earlier)) : go (v : seen) vs
     sameSpelling (Rzk.VarIdent _ a) (Rzk.VarIdent _ b) = a == b
 
+-- | Report a command's error and go on to the next one, with the command
+-- itself contributing nothing to the scope.
+--
+-- This is the recovery for a command that cannot be stood in for: a
+-- declaration whose /type/ does not check has no type to enter it at. The uses
+-- of it below then report an undefined variable, which is noisier than the one
+-- error but keeps the rest of the file's own errors and holes visible, which is
+-- what a file being edited is wanted for.
+skippingCommand
+  :: Distinct n
+  => TypeErrorInScopedContext
+  -> Maybe FilePath -> Integer -> Integer -> [Rzk.Command]
+  -> (forall l. (DExt n l, Distinct l)
+        => [Decl l] -> [TypeErrorInScopedContext] -> TypeCheck l r)
+  -> TypeCheck n r
+skippingCommand err path i total more k =
+  checkCommands path (i + 1) total more $ \decls errs -> k decls (err : errs)
+
+-- | Run a check, handing back its error instead of propagating it.
+--
+-- What it recorded on the way is kept: the record lives in the state beneath
+-- the error channel, so the holes the user wrote in a definition that fails are
+-- still reported (see "Rzk.TypeCheck.Monad").
+tryCheck :: TypeCheck n a -> TypeCheck n (Either TypeErrorInScopedContext a)
+tryCheck action = (Right <$> action) `catchError` (pure . Left)
+
+-- | Run a check with the location narrowed to where a surface term was written.
+--
+-- Descending through a judgement already narrows to the sub-term it is about
+-- (@narrowLocation@ in "Rzk.TypeCheck.Monad"), but only a /node/ carries a
+-- position: a variable is a leaf of the core syntax, with nowhere to put one.
+-- So a check that starts from a surface term says where that term starts, and a
+-- definition whose body is a bare variable is reported at the body rather than
+-- at the declaration above it.
+atSurface :: Rzk.HasPosition a => a -> TypeCheck n b -> TypeCheck n b
+atSurface x = local $ \ctx ->
+  ctx { ctxLocation = narrow <$> ctxLocation ctx }
+  where
+    narrow loc = case Rzk.hasPosition x of
+      Nothing          -> loc
+      Just (line, col) ->
+        loc { locationLine = Just line, locationColumn = Just col }
+
 -- | Elaborate a surface term in the current top-level scope: a free identifier
 -- resolves to the top-level entry it names.
 elaborate :: forall n. Distinct n => Rzk.Term -> TypeCheck n (Term n)
@@ -1125,27 +1171,43 @@
   command@(Rzk.CommandDefine _loc name (Rzk.DeclUsedVars _ vars) params ty term) : more ->
     announce (" Checking #define " <> Rzk.printTree name) $
       withCommand command k $ do
-        used <- mapM (checkDefined . varIdentAt path) vars
-        paramDecls <- concat <$> mapM paramToParamDecl params
         -- Store the elaborated type and term unreduced, but memoise their WHNF on
         -- the top node. Reducing in place would discard or expose a variable
         -- occurrence, so the section unused/implicit-assumption checks (run over the
         -- stored type and value) would disagree with the term the user wrote;
         -- keeping the WHNF cached preserves the original one-shot reduction.
-        tyTerm <- elaborate (addParamDecls paramDecls ty)
-        ty' <- memoizeWHNF =<< typecheck tyTerm universeT
-        valTerm <- elaborate (addParams params term)
-        term' <- memoizeWHNF =<< typecheck valTerm ty'
-        withTopLevel (varIdentAt path name) ty' (Just term') False used Nothing $ \binder decl -> do
-          backend <- asks ctxRenderBackend
-          termSVG <- case backend of
-            Just RenderSVG   -> renderTermSVG (Var (Foil.nameOf binder))
-            Just RenderLaTeX -> issueTypeError $
-              TypeErrorOther "\"latex\" rendering is not yet supported"
-            Nothing          -> pure Nothing
-          maybe id trace termSVG $
-            checkCommands path (i + 1) total more $ \decls errs ->
-              k (sinkDecl decl : decls) errs
+        typeResult <- tryCheck $ do
+          used <- mapM (checkDefined . varIdentAt path) vars
+          paramDecls <- concat <$> mapM paramToParamDecl params
+          tyTerm <- elaborate (addParamDecls paramDecls ty)
+          ty' <- atSurface ty $ memoizeWHNF =<< typecheck tyTerm universeT
+          pure (used, ty')
+        case typeResult of
+          Left typeError -> skippingCommand typeError path i total more k
+          Right (used, ty') -> do
+            -- The body is checked on its own, so that a definition whose type
+            -- is fine but whose proof is not still enters the scope, as a
+            -- postulate of that type. The rest of the file is then checked
+            -- against it and its own errors and holes reported, instead of the
+            -- run stopping at this one.
+            result <- tryCheck $ do
+              valTerm <- elaborate (addParams params term)
+              atSurface term $ memoizeWHNF =<< typecheck valTerm ty'
+            let (mvalue, bodyErrors) = case result of
+                  Right term'  -> (Just term', [])
+                  Left bodyErr -> (Nothing, [bodyErr])
+            withTopLevel (varIdentAt path name) ty' mvalue False used Nothing $ \binder decl -> do
+              -- A definition with no proof term has no diagram to draw.
+              termSVG <- case mvalue of
+                Nothing -> pure Nothing
+                Just _  -> asks ctxRenderBackend >>= \case
+                  Just RenderSVG   -> renderTermSVG (Var (Foil.nameOf binder))
+                  Just RenderLaTeX -> issueTypeError $
+                    TypeErrorOther "\"latex\" rendering is not yet supported"
+                  Nothing          -> pure Nothing
+              maybe id trace termSVG $
+                checkCommands path (i + 1) total more $ \decls errs ->
+                  k (sinkDecl decl : decls) (bodyErrors <> errs)
 
   command@(Rzk.CommandData _loc name (Rzk.DeclUsedVars _ vars) params sort body) : more ->
     announce (" Checking #data " <> Rzk.printTree name) $
@@ -1164,32 +1226,47 @@
   command@(Rzk.CommandPostulate _loc name (Rzk.DeclUsedVars _ vars) params ty) : more ->
     announce (" Checking #postulate " <> Rzk.printTree name) $
       withCommand command k $ do
-        used <- mapM (checkDefined . varIdentAt path) vars
-        paramDecls <- concat <$> mapM paramToParamDecl params
-        tyTerm <- elaborate (addParamDecls paramDecls ty)
-        ty' <- memoizeWHNF =<< typecheck tyTerm universeT
-        withTopLevel (varIdentAt path name) ty' Nothing False used Nothing $ \_binder decl ->
-          checkCommands path (i + 1) total more $ \decls errs ->
-            k (sinkDecl decl : decls) errs
+        typeResult <- tryCheck $ do
+          used <- mapM (checkDefined . varIdentAt path) vars
+          paramDecls <- concat <$> mapM paramToParamDecl params
+          tyTerm <- elaborate (addParamDecls paramDecls ty)
+          ty' <- atSurface ty $ memoizeWHNF =<< typecheck tyTerm universeT
+          pure (used, ty')
+        case typeResult of
+          Left typeError -> skippingCommand typeError path i total more k
+          Right (used, ty') ->
+            withTopLevel (varIdentAt path name) ty' Nothing False used Nothing $ \_binder decl ->
+              checkCommands path (i + 1) total more $ \decls errs ->
+                k (sinkDecl decl : decls) errs
 
   command@(Rzk.CommandAssume _loc names ty) : more ->
     announce (" Checking #assume "
         <> intercalate " " [ Rzk.printTree name | name <- names ]) $
       withCommand command k $ do
-        tyTerm <- elaborate ty
-        ty' <- typecheck tyTerm universeT
-        assume (map (varIdentAt path) names) ty' $ \assumed ->
-          checkCommands path (i + 1) total more $ \decls errs ->
-            k (sinkDecls assumed <> decls) errs
+        typeResult <- tryCheck $ do
+          tyTerm <- elaborate ty
+          atSurface ty $ typecheck tyTerm universeT
+        case typeResult of
+          Left typeError -> skippingCommand typeError path i total more k
+          Right ty' ->
+            assume (map (varIdentAt path) names) ty' $ \assumed ->
+              checkCommands path (i + 1) total more $ \decls errs ->
+                k (sinkDecls assumed <> decls) errs
 
   command@(Rzk.CommandCheck _loc term ty) : more ->
     announce (" Checking " <> Rzk.printTree term <> " : " <> Rzk.printTree ty) $
       withCommand command k $ do
-        tyTerm <- elaborate ty
-        ty' <- typecheck tyTerm universeT >>= whnfT
-        termTerm <- elaborate term
-        _term' <- typecheck termTerm ty'
-        checkCommands path (i + 1) total more k
+        -- A #check declares nothing, so its failure costs the rest of the file
+        -- nothing either.
+        result <- tryCheck $ do
+          tyTerm <- elaborate ty
+          ty' <- atSurface ty $ typecheck tyTerm universeT >>= whnfT
+          termTerm <- elaborate term
+          _term' <- atSurface term $ typecheck termTerm ty'
+          pure ()
+        case result of
+          Left err -> skippingCommand err path i total more k
+          Right () -> checkCommands path (i + 1) total more k
 
   Rzk.CommandCompute loc term : more ->
     checkCommands path i total (Rzk.CommandComputeWHNF loc term : more) k
@@ -1197,18 +1274,24 @@
   command@(Rzk.CommandComputeNF _loc term) : more ->
     announce (" Computing NF for " <> Rzk.printTree term) $
       withCommand command k $ do
-        term' <- elaborate term >>= infer >>= nfT
-        shown <- ppInContext term'
-        traceTypeCheck Normal ("  " <> shown) $
-          checkCommands path (i + 1) total more k
+        result <- tryCheck $ do
+          term' <- atSurface term $ elaborate term >>= infer >>= nfT
+          ppInContext term'
+        case result of
+          Left err -> skippingCommand err path i total more k
+          Right shown -> traceTypeCheck Normal ("  " <> shown) $
+            checkCommands path (i + 1) total more k
 
   command@(Rzk.CommandComputeWHNF _loc term) : more ->
     announce (" Computing WHNF for " <> Rzk.printTree term) $
       withCommand command k $ do
-        term' <- elaborate term >>= infer >>= whnfT
-        shown <- ppInContext term'
-        traceTypeCheck Normal ("  " <> shown) $
-          checkCommands path (i + 1) total more k
+        result <- tryCheck $ do
+          term' <- atSurface term $ elaborate term >>= infer >>= whnfT
+          ppInContext term'
+        case result of
+          Left err -> skippingCommand err path i total more k
+          Right shown -> traceTypeCheck Normal ("  " <> shown) $
+            checkCommands path (i + 1) total more k
 
   command@(Rzk.CommandSection _loc name) : more ->
     withCommand command k $ do
@@ -1276,7 +1359,10 @@
   -> TypeCheck n r
 checkModuleWithLocation (path, module_) k =
   traceTypeCheck Normal ("Checking module from " <> path) $
-    withLocation (LocationInfo { locationFilePath = Just path, locationLine = Nothing }) $
+    withLocation (LocationInfo
+      { locationFilePath = Just path
+      , locationLine = Nothing
+      , locationColumn = Nothing }) $
       checkModule (Just path) module_ k
 
 -- | Check a list of modules, one after another, in a scope that grows as it goes.
@@ -1299,17 +1385,18 @@
 -- * The public entry points
 
 -- | Check the modules, and package the result with the scope it was checked in.
--- The warnings live on the writer channel during the run and are folded into
--- the 'Checked' package here.
+-- The warnings are recorded during the run and are folded into the 'Checked'
+-- package here.
 checkedModules :: [(FilePath, Rzk.Module)] -> Context Foil.VoidS -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
 checkedModules modules ctx =
-  fmap package $ runExcept $ runWriterT $ flip runReaderT ctx $
+  package $ runTypeCheckWith ctx $
     checkModules modules $ \decls errs -> do
       ctx' <- ask
       pure (Checked ctx' decls errs [])
   where
-    package (Checked ctx' decls errs _, (holes, warnings)) =
-      (Checked ctx' decls errs warnings, holes)
+    package (Left err, _) = Left err
+    package (Right (Checked ctx' decls errs _), (holes, warnings)) =
+      Right (Checked ctx' decls errs warnings, holes)
 
 -- | Check the modules strictly: an unfilled hole is an error, and the first error
 -- stops the run.
@@ -1411,15 +1498,16 @@
   -> [(FilePath, Rzk.Module)]
   -> Either TypeErrorInScopedContext (Checked, [HoleInfo])
 recheckFrom (Checked ctx decls _errs _warnings) modules =
-  fmap package $ runExcept $ runWriterT $ flip runReaderT ctx $
+  package $ runTypeCheckWith ctx $
     checkModules modules $ \newDecls errs -> do
       ctx' <- ask
       pure (Checked ctx' (sinkDeclGroups decls <> newDecls) errs [])
   where
     -- Only this run's warnings: like the errors, the prefix's warnings were
     -- already reported when the prefix was checked.
-    package (Checked ctx' decls' errs _, (holes, warnings)) =
-      (Checked ctx' decls' errs warnings, holes)
+    package (Left err, _) = Left err
+    package (Right (Checked ctx' decls' errs _), (holes, warnings)) =
+      Right (Checked ctx' decls' errs warnings, holes)
 
 -- | The errors of a checked run.
 checkedErrors :: Checked -> [TypeErrorInScopedContext]
@@ -1432,3 +1520,13 @@
 -- | Nothing checked yet: the empty context, and no declarations.
 emptyChecked :: Checked
 emptyChecked = Checked emptyContext [] [] []
+
+-- | Nothing checked yet, in lenient hole mode: what an editor resumes from.
+--
+-- A hole is work in progress there, to be reported with its goal and context
+-- rather than as an error (see 'allowHoles'). 'recheckFrom' continues in the
+-- context it is given, so the mode has to be set on the empty one it starts
+-- with: resuming from 'emptyChecked' made every hole a @TypeErrorUnsolvedHole@
+-- and stopped the file at the first one.
+emptyCheckedWithHoles :: Checked
+emptyCheckedWithHoles = Checked (allowHoles emptyContext) [] [] []
diff --git a/src/Rzk/TypeCheck/Error.hs b/src/Rzk/TypeCheck/Error.hs
--- a/src/Rzk/TypeCheck/Error.hs
+++ b/src/Rzk/TypeCheck/Error.hs
@@ -383,9 +383,11 @@
   [ block TopDown
     [ case ctxLocation of
         _ | dir == TopDown -> "" -- FIXME
-        Just (LocationInfo (Just path) (Just lineNo)) ->
+        Just (LocationInfo (Just path) (Just lineNo) (Just col)) ->
+          path <> " (line " <> show lineNo <> ", column " <> show col <> "):"
+        Just (LocationInfo (Just path) (Just lineNo) Nothing) ->
           path <> " (line " <> show lineNo <> "):"
-        Just (LocationInfo (Just path) _) ->
+        Just (LocationInfo (Just path) _ _) ->
           path <> ":"
         _  -> ""
     , case ctxCurrentCommand of
diff --git a/src/Rzk/TypeCheck/Eval.hs b/src/Rzk/TypeCheck/Eval.hs
--- a/src/Rzk/TypeCheck/Eval.hs
+++ b/src/Rzk/TypeCheck/Eval.hs
@@ -21,10 +21,7 @@
 module Rzk.TypeCheck.Eval where
 
 import           Control.Monad               (forM, forM_, unless, when)
-import           Control.Monad.Except        (runExcept)
-import           Control.Monad.Reader        (ask, asks, local,
-                                              runReaderT)
-import           Control.Monad.Trans.Writer.CPS (runWriterT)
+import           Control.Monad.Reader        (ask, asks, local)
 import           Data.List                   (intercalate, nub, nubBy,
                                               tails)
 import           Data.Maybe                  (catMaybes)
@@ -354,9 +351,9 @@
   => (Context n -> Context n) -> TypeCheck n a -> TypeCheck n a
 withRefreshedTopes f action = do
   ctx' <- asks f
-  let sat = case runExcept (runWriterT (runReaderT (saturateForEntailment (ctxTopesNF ctx')) ctx')) of
-        Left _       -> Nothing
-        Right (s, _) -> Just s
+  let sat = case runTypeCheckIn ctx' (saturateForEntailment (ctxTopesNF ctx')) of
+        Left _  -> Nothing
+        Right s -> Just s
   local (const ctx' { ctxTopesSaturated = SaturationCached sat }) action
 
 -- | Run a check in every alternative of a disjunctive tope context.
diff --git a/src/Rzk/TypeCheck/Judgements.hs b/src/Rzk/TypeCheck/Judgements.hs
--- a/src/Rzk/TypeCheck/Judgements.hs
+++ b/src/Rzk/TypeCheck/Judgements.hs
@@ -19,7 +19,6 @@
 import           Control.Monad            (forM, forM_, unless, when)
 import           Control.Monad.Except     (catchError)
 import           Control.Monad.Reader     (ask, asks, local)
-import           Control.Monad.Writer.CPS (censor)
 import           Data.List                (intercalate, sortOn, tails)
 import qualified Data.IntMap              as IntMap
 import qualified Data.IntSet              as IntSet
@@ -281,6 +280,12 @@
 -- mismatch (an under-applied function does not match an extension-type goal, but a
 -- partial application that genuinely fits an ordinary-function goal does).
 --
+-- The exception is a /flexible/ type, one headed by a hole: it has no shape to
+-- mismatch with, so it fits any target. This is what makes an eliminator stated
+-- over a motive usable as a candidate --- @ind-path ? ? ? ? ? ?@ has type
+-- @?C ?x ?p@ and so is offered at every goal, exactly as @idJ@ already is, with
+-- the motive and the base case left as holes.
+--
 -- Outer type restrictions are stripped from both sides first: an extension-type
 -- boundary is satisfied by later refinement, not by the choice of spine, and
 -- matching against the restricted goal would reject the very spine that introduces
@@ -292,7 +297,7 @@
 fitsInto term ty target = do
   ty'     <- stripTypeRestrictions <$> whnfT ty
   target' <- stripTypeRestrictions <$> whnfT target
-  censor (const mempty) $ local structuralHoleUnify
+  suppressing $ local structuralHoleUnify
     ((unify (Just term) target' ty' >> pure True) `catchError` \_ -> pure False)
 
 -- | The eliminators a value of the given (weak head normal) type admits, each as a
@@ -575,7 +580,7 @@
 -- probing are discarded, leaving a pure yes\/no query.
 endpointsAgree :: Distinct n => TermT n -> TermT n -> TypeCheck n Bool
 endpointsAgree a b =
-  censor (const mempty)
+  suppressing
     ((unify Nothing a b >> pure True) `catchError` \_ -> pure False)
 
 -- | Ex falso: in a contradictory tope context @recBOT@ inhabits any type, so it is a
@@ -785,8 +790,8 @@
 
   -- for each local hypothesis (and allow-listed lemma), the elimination spines that
   -- land in the goal (arguments left as holes). Probing must not leak holes into the
-  -- recorded output, hence the 'censor'.
-  candidates <- censor (const mempty) $ do
+  -- recorded output, hence the 'suppressing'.
+  candidates <- suppressing $ do
     -- over the shown hypotheses: a unit-bound point admits no elimination,
     -- and offering it bare would duplicate the @unit@ introduction
     elims <- concat <$>
@@ -843,7 +848,7 @@
   -- the introduction forms for the goal itself (constituents left as holes); the Π
   -- binder is freshened against the names in scope so that it does not shadow,
   -- and the parse-back check applies like it does to the candidates.
-  introductions <- censor (const mempty) (allIntroductionsOf goalTy takenNames)
+  introductions <- suppressing (allIntroductionsOf goalTy takenNames)
   introductionMoves <- fmap concat $ forM introductions $ \i -> do
     let r = renderMove i
     ok <- parsesBackTo table i r
@@ -851,7 +856,7 @@
   -- the goal cell: an SVG of the shape the hole must inhabit (an arrow, triangle or
   -- square), drawn from an abstract inhabitant with the proof term hidden. 'Nothing'
   -- when the goal is not a renderable shape.
-  diagram <- censor (const mempty) (renderGoalCellSVG goal')
+  diagram <- suppressing (renderGoalCellSVG goal')
 
   recordHoleInfo HoleInfo
     { holeName          = mname
diff --git a/src/Rzk/TypeCheck/Monad.hs b/src/Rzk/TypeCheck/Monad.hs
--- a/src/Rzk/TypeCheck/Monad.hs
+++ b/src/Rzk/TypeCheck/Monad.hs
@@ -16,18 +16,20 @@
 module Rzk.TypeCheck.Monad where
 
 import           Control.Monad            (unless)
-import           Control.Monad.Except     (Except, MonadError (throwError),
-                                           runExcept)
+import           Control.Monad.Except     (ExceptT,
+                                           MonadError (catchError, throwError),
+                                           runExceptT)
 import           Control.Monad.Reader     (ReaderT (..), ask, asks, local)
 import           Control.Monad.Trans      (lift)
-import           Control.Monad.Trans.Writer.CPS (WriterT, runWriterT)
-import           Control.Monad.Writer.CPS (tell)
+import           Control.Monad.Trans.State.Strict (State, get, modify', put,
+                                           runState)
 import           Debug.Trace              (trace)
 
 import           Control.Monad.Foil       (Distinct)
 import qualified Control.Monad.Foil       as Foil
 
 import           Language.Rzk.Foil.Names (VarIdent)
+import           Language.Rzk.Foil.Syntax (positionOfTerm)
 import           Rzk.TypeCheck.Context
 import           Rzk.TypeCheck.Display
 import           Rzk.TypeCheck.Error
@@ -101,24 +103,56 @@
   | MetaPrefixStrictOnly
   deriving (Eq, Show)
 
+-- | What a run records besides its result: the holes it found and the non-fatal
+-- findings it made. Both accumulate in reverse and are turned around by
+-- 'checkLog' when the run ends.
+data CheckLog = CheckLog
+  { logHolesRev    :: [HoleInfo]
+  , logWarningsRev :: [CheckWarning]
+  }
+
+emptyCheckLog :: CheckLog
+emptyCheckLog = CheckLog [] []
+
+-- | What a run recorded, in the order it was recorded.
+checkLog :: CheckLog -> ([HoleInfo], [CheckWarning])
+checkLog (CheckLog holes warnings) = (reverse holes, reverse warnings)
+
+-- | The record of a run is kept in the /state/, beneath the error channel,
+-- rather than on a writer channel above it.
+--
+-- The two differ exactly where a caught error is concerned: a writer discards
+-- what the failing action wrote, and the state keeps it. That is what the
+-- checker wants. A command that fails still reports the holes the user wrote in
+-- it, and checking goes on to the next command with those holes in hand (see
+-- @withCommand@ in "Rzk.TypeCheck.Decl"). A probe that wants the older
+-- behaviour asks for it, with 'suppressing'.
 type TypeCheck n =
   ReaderT (Context n)
-    (WriterT ([HoleInfo], [CheckWarning]) (Except TypeErrorInScopedContext))
+    (ExceptT TypeErrorInScopedContext (State CheckLog))
 
+-- | Run a judgement in a given context, keeping what it recorded.
+runTypeCheckWith
+  :: Context n -> TypeCheck n a
+  -> (Either TypeErrorInScopedContext a, ([HoleInfo], [CheckWarning]))
+runTypeCheckWith ctx tc =
+  case runState (runExceptT (runReaderT tc ctx)) emptyCheckLog of
+    (result, logged) -> (result, checkLog logged)
+
 -- | Run a judgement in the empty context, discarding the holes it records.
 runTypeCheck :: TypeCheck Foil.VoidS a -> Either TypeErrorInScopedContext a
-runTypeCheck tc = fst <$> runExcept (runWriterT (runReaderT tc emptyContext))
+runTypeCheck = runTypeCheckIn emptyContext
 
 -- | Run a judgement in a given context, discarding the holes it records.
 runTypeCheckIn :: Context n -> TypeCheck n a -> Either TypeErrorInScopedContext a
-runTypeCheckIn ctx tc = fst <$> runExcept (runWriterT (runReaderT tc ctx))
+runTypeCheckIn ctx tc = fst (runTypeCheckWith ctx tc)
 
 -- | Run a judgement in another scope's context.
 --
 -- The error channel and the hole channel are shared and carry no scope index, so
 -- there is nothing to translate: this is 'runReaderT' with the inner scope's
--- context, lifted back. Holes recorded inside are told into the same writer, and
--- an error thrown inside already carries its own context.
+-- context, lifted back. Holes recorded inside land in the same state, and an
+-- error thrown inside already carries its own context.
 inContext :: Context l -> TypeCheck l a -> TypeCheck n a
 inContext ctx = lift . flip runReaderT ctx
 
@@ -193,6 +227,7 @@
   let ctx' = ctx
         { ctxActionStack = action : ctxActionStack
         , ctxActionStackDepth = ctxActionStackDepth + 1
+        , ctxLocation = narrowLocation action ctxLocation
         }
   -- The trace message is built only when it is actually printed: at normal
   -- verbosity rendering the action's terms on every judgement would cost a
@@ -202,15 +237,53 @@
            local (const ctx') tc
     else local (const ctx') tc
 
+-- | Point the location at the sub-term an action is about.
+--
+-- The checker descends through 'performing', so the location narrows as it
+-- goes and an error is reported where the sub-term that caused it was written,
+-- rather than at the declaration it is in (issue #81). A judgement about a term
+-- the checker built itself carries no position, and leaves the location as it
+-- found it: that is the innermost enclosing term the user did write.
+narrowLocation :: Action n -> Maybe LocationInfo -> Maybe LocationInfo
+narrowLocation action loc = case termOf action of
+  Just term | Just pos <- positionOfTerm term -> atPosition pos <$> loc
+  _                                           -> loc
+  where
+    termOf (ActionTypeCheck term _) = Just term
+    termOf (ActionInfer term)       = Just term
+    termOf _                        = Nothing
+
+-- * What a run records
+
+modifyLog :: (CheckLog -> CheckLog) -> TypeCheck n ()
+modifyLog f = lift (lift (modify' f))
+
+-- | Run a probe for its answer alone, discarding whatever it records.
+--
+-- A hole's inventory is built by trying candidate moves and seeing which fit,
+-- and each trial checks terms of its own; their holes and warnings are not the
+-- user's and must not reach the report. This is what the writer channel's
+-- @censor@ did before the record moved into the state: the state survives an
+-- error, so it is put back on that path too.
+suppressing :: TypeCheck n a -> TypeCheck n a
+suppressing action = do
+  saved <- lift (lift get)
+  let restore = lift (lift (put saved))
+  result <- action `catchError` \err -> restore >> throwError err
+  restore
+  return result
+
 -- * Holes
 
 recordHoleInfo :: HoleInfo -> TypeCheck n ()
-recordHoleInfo info = lift (tell ([info], []))
+recordHoleInfo info =
+  modifyLog $ \l -> l { logHolesRev = info : logHolesRev l }
 
 -- * Warnings
 
 recordCheckWarning :: CheckWarning -> TypeCheck n ()
-recordCheckWarning warning = lift (tell ([], [warning]))
+recordCheckWarning warning =
+  modifyLog $ \l -> l { logWarningsRev = warning : logWarningsRev l }
 
 -- * Locations
 
diff --git a/src/Rzk/TypeCheck/Unify.hs b/src/Rzk/TypeCheck/Unify.hs
--- a/src/Rzk/TypeCheck/Unify.hs
+++ b/src/Rzk/TypeCheck/Unify.hs
@@ -174,10 +174,21 @@
       -- mentions it. Such a branch is only entered because the hole is unfilled, so
       -- a mismatch under it is deferred too. 'structuralHoleUnify' turns this off,
       -- keeping a structural mismatch around a hole an error.
+      --
+      -- A /flexible/ side is the exception 'structuralHoleUnify' does not cover:
+      -- a term headed by a hole ('isHoleHeadedT') has no shape to mismatch with
+      -- yet, since filling the head decides what it is. It therefore unifies with
+      -- anything even under 'structuralHoleUnify'. This is what lets an
+      -- eliminator whose result is a motive application be offered as a hole
+      -- candidate: @ind-path ? ? ? ? ? ?@ has type @?C ?x ?p@, which fits any
+      -- goal. A move is a suggestion, not a solution -- the motive and the base
+      -- case are left as holes for the caller, and the result is type-checked
+      -- like any other term once written.
       defer <- asks ctxDeferHoleMismatches
       topeContextHasHole <- asks (any (containsHole . tTope) . ctxTopes)
-      let holePresent = defer &&
-            (containsHole expected' || containsHole actual' || topeContextHasHole)
+      let holePresent =
+            (defer && (containsHole expected' || containsHole actual' || topeContextHasHole))
+              || isHoleHeadedT expected' || isHoleHeadedT actual'
 
           err :: TypeCheck n ()
           err
diff --git a/test/Rzk/FormatSpec.hs b/test/Rzk/FormatSpec.hs
--- a/test/Rzk/FormatSpec.hs
+++ b/test/Rzk/FormatSpec.hs
@@ -2,12 +2,13 @@
 Module      : FormatterSpec
 Description : Tests related to the formatter module
 -}
+{-# LANGUAGE OverloadedStrings #-}
 module Rzk.FormatSpec where
 
 import qualified Data.Text.IO as T
 import           Test.Hspec
 
-import           Rzk.Format   (format, isWellFormatted)
+import           Rzk.Format   (format, formatDocument, isWellFormatted)
 
 formatsTo :: FilePath -> FilePath -> Expectation
 formatsTo beforePath afterPath = do
@@ -66,3 +67,21 @@
     it "Fixes indentation" pending
 
     it "Wraps long lines" pending
+
+  -- The language server replaces the whole document, and used to send it with
+  -- every trailing newline stripped: saving deleted the file's final newline,
+  -- which then failed the .editorconfig and Prettier checks that sHoTT's CI
+  -- runs, with no formatting able to satisfy both.
+  describe "formatDocument" $ do
+    it "Keeps the final newline" $ do
+      formatDocument "#lang rzk-1\n" `shouldBe` "#lang rzk-1\n"
+
+    it "Keeps a document that ends without a newline as it was" $ do
+      formatDocument "#lang rzk-1" `shouldBe` "#lang rzk-1"
+
+    it "Keeps the trailing blank lines the source had" $ do
+      formatDocument "#lang rzk-1\n\n\n" `shouldBe` "#lang rzk-1\n\n\n"
+
+    it "Is idempotent on the final newline" $ do
+      let src = "#lang rzk-1\n\n#define id (A : U)\n  : A → A\n  := \\ x → x\n"
+      formatDocument src `shouldBe` src
diff --git a/test/Rzk/HolesSpec.hs b/test/Rzk/HolesSpec.hs
--- a/test/Rzk/HolesSpec.hs
+++ b/test/Rzk/HolesSpec.hs
@@ -453,6 +453,33 @@
            cands h `shouldContain` ["my-id ?"]
            filter (== "my-id") (cands h) `shouldBe` []
 
+    -- A lemma whose result type is a motive application (@ind-path ... : C x p@)
+    -- is offered like any other: the spine's type is headed by a hole, which has
+    -- no shape to mismatch with, so it fits any goal. Without this, every
+    -- eliminator written in the sHoTT style is invisible as a move while the
+    -- built-in @idJ@ is offered, and a level cannot teach the library spelling.
+    it "offers a lemma whose result type is headed by a hole" $
+      let indSrc = "#lang rzk-1\n"
+                <> "#define ind-path (A : U) (a : A)\n"
+                <> "  (C : (x : A) -> (a = x) -> U) (d : C a refl)\n"
+                <> "  (x : A) (p : a = x) : C x p\n"
+                <> "  := idJ (A , a , C , d , x , p)\n"
+                <> "#define goal (A : U) (x y : A) (p : x = y) : y = x := ?\n"
+      in flip oneHole (holesWithLemmas ["ind-path"] indSrc) $ \h ->
+           cands h `shouldContain` ["ind-path ? ? ? ? ? ?"]
+
+    -- Fitting anything does not mean escaping the allow-list: a hole-headed
+    -- lemma is still only offered when the level grants it.
+    it "does not offer a hole-headed lemma that was not allow-listed" $
+      let indSrc = "#lang rzk-1\n"
+                <> "#define ind-path (A : U) (a : A)\n"
+                <> "  (C : (x : A) -> (a = x) -> U) (d : C a refl)\n"
+                <> "  (x : A) (p : a = x) : C x p\n"
+                <> "  := idJ (A , a , C , d , x , p)\n"
+                <> "#define goal (A : U) (x y : A) (p : x = y) : y = x := ?\n"
+      in flip oneHole (holesWithLemmas [] indSrc) $ \h ->
+           filter (isInfixOf "ind-path") (cands h) `shouldBe` []
+
   describe "holeCandidates under shadowing" $ do
     let cands = map show . holeCandidates
         -- the motive λ rebinds b, so at the inner hole the telescope's b is
diff --git a/test/Rzk/TypeCheckSpec.hs b/test/Rzk/TypeCheckSpec.hs
--- a/test/Rzk/TypeCheckSpec.hs
+++ b/test/Rzk/TypeCheckSpec.hs
@@ -39,6 +39,8 @@
   , expectErrorTag        :: Maybe String
   , expectMessageContains :: Maybe [String]
   , expectLine            :: Maybe Int
+  , expectColumn          :: Maybe Int
+  , expectErrorCount      :: Maybe Int
   , expectRegressionFor   :: Maybe [String]
   , expectModules         :: Maybe [FilePath]
   , expectApi             :: Maybe String
@@ -51,6 +53,8 @@
     <*> o .:? "error_tag"
     <*> o .:? "message_contains"
     <*> o .:? "line"
+    <*> o .:? "column"
+    <*> o .:? "error_count"
     <*> o .:? "regression_for"
     <*> o .:? "modules"
     <*> o .:? "api"
@@ -64,6 +68,10 @@
 errorLine :: TypeErrorInScopedContext -> Maybe Int
 errorLine err = locationOfTypeError err >>= locationLine
 
+-- | The column an error was raised at: the start of the sub-term it is about.
+errorColumn :: TypeErrorInScopedContext -> Maybe Int
+errorColumn err = locationOfTypeError err >>= locationColumn
+
 -- | The constructor name of a type error, used to match @error_tag@ in fixtures.
 -- This is the library's own tag (also used for diagnostic codes), so the two cannot
 -- drift apart.
@@ -150,6 +158,15 @@
         expectationFailure $ "in " <> label <> ", expected line " <> show ln
           <> " got " <> show got
       Just _ -> pure ()
+  case expectColumn of
+    Nothing -> pure ()
+    Just c -> case errorColumn err of
+      Nothing -> expectationFailure $ "in " <> label <> ", expected column "
+        <> show c <> " but error has no column"
+      Just got | got /= c ->
+        expectationFailure $ "in " <> label <> ", expected column " <> show c
+          <> " got " <> show got
+      Just _ -> pure ()
 assertExpect label Expect{expectStatus = "ok", expectWarnings = want} (Right checked) =
   assertWarnings label want checked
 assertExpect label Expect{expectStatus = st} _ =
@@ -177,6 +194,13 @@
     [] ->
       expectationFailure $ "in " <> label <> ", expected type errors but got none"
     err : _ -> do
+      case expectErrorCount of
+        Nothing -> pure ()
+        Just n | length errs /= n ->
+          expectationFailure $ "in " <> label <> ", expected " <> show n
+            <> " errors, got " <> show (length errs) <> ":\n"
+            <> unlines (map (ppTypeErrorInScopedContext BottomUp) errs)
+        Just _ -> pure ()
       let tag = typeErrorConstructorName err
       case expectErrorTag of
         Nothing -> expectationFailure "expect.yaml missing error_tag for status: error"
@@ -197,6 +221,13 @@
           Nothing -> expectationFailure "expected line number on error"
           Just got | got /= ln ->
             expectationFailure $ "line mismatch: wanted " <> show ln <> " got " <> show got
+          Just _ -> pure ()
+      case expectColumn of
+        Nothing -> pure ()
+        Just c -> case errorColumn err of
+          Nothing -> expectationFailure "expected column on error"
+          Just got | got /= c ->
+            expectationFailure $ "column mismatch: wanted " <> show c <> " got " <> show got
           Just _ -> pure ()
   st ->
     expectationFailure $ "in " <> label <> ", unknown status " <> show st
diff --git a/test/typecheck/SCHEMA.md b/test/typecheck/SCHEMA.md
--- a/test/typecheck/SCHEMA.md
+++ b/test/typecheck/SCHEMA.md
@@ -19,7 +19,9 @@
 | `status` | yes | `ok` if typechecking must succeed; `error` if it must fail with a type error. |
 | `error_tag` | if `status: error` | Name of the `TypeError` constructor after stripping `ScopedTypeError` wrappers, e.g. `TypeErrorUnify`, `TypeErrorUndefined`. |
 | `message_contains` | no | Substrings that must all appear in the rendered error (`ppTypeErrorInScopedContext'`). |
-| `line` | no | 1-based line number (approximate) in the Rzk file where the error is reported. |
+| `line` | no | 1-based line number in the Rzk file where the error is reported: the start of the sub-term the error is about, not of the declaration around it. |
+| `column` | no | 1-based column on that line, likewise the start of the sub-term. A variable is a leaf of the core syntax and carries no position of its own, so an error blamed on one is reported at the innermost term around it that does. |
+| `error_count` | no | With `api: collect`, the exact number of errors the run must report. A definition whose body fails to check is entered as a postulate of its declared type and checking continues, so a file reports every error it has. |
 | `regression_for` | no | Traceability: GitHub issue/PR URLs, commit themes, or short **semantic** rule names (e.g. `contextEntailsUnion-recOR-boundary`). Avoid `TypeCheck.hs` line numbers and `issueTypeError-<line>` tags — they go stale. |
 | `modules` | no | If set (directory case), ordered list of module files for one `typecheckModulesWithLocation` run. |
 | `api` | no | Omit or `strict` (default): `typecheckModulesWithLocation` (throws on first error). `collect`: `typecheckModulesWithLocation'` — returns a list of errors without using `throwError`; note that the typechecker still stops per-module chaining when a module reports errors (see implementation in `Rzk.TypeCheck`). |
diff --git a/test/typecheck/cases/ill-match-branch-arity.expect.yaml b/test/typecheck/cases/ill-match-branch-arity.expect.yaml
--- a/test/typecheck/cases/ill-match-branch-arity.expect.yaml
+++ b/test/typecheck/cases/ill-match-branch-arity.expect.yaml
@@ -3,6 +3,7 @@
 message_contains:
   - "match branch for constructor suc"
   - "binds 1 argument, but its method takes 2"
-line: 6
+line: 7
+column: 6
 regression_for:
   - match-branch-arity
diff --git a/test/typecheck/cases/ill-match-duplicate-branch.expect.yaml b/test/typecheck/cases/ill-match-duplicate-branch.expect.yaml
--- a/test/typecheck/cases/ill-match-duplicate-branch.expect.yaml
+++ b/test/typecheck/cases/ill-match-duplicate-branch.expect.yaml
@@ -2,6 +2,7 @@
 error_tag: TypeErrorMatchDuplicateBranch
 message_contains:
   - "duplicate match branch for constructor zero"
-line: 5
+line: 6
+column: 6
 regression_for:
   - match-branch-bijection
diff --git a/test/typecheck/cases/ill-match-missing-branch.expect.yaml b/test/typecheck/cases/ill-match-missing-branch.expect.yaml
--- a/test/typecheck/cases/ill-match-missing-branch.expect.yaml
+++ b/test/typecheck/cases/ill-match-missing-branch.expect.yaml
@@ -2,6 +2,7 @@
 error_tag: TypeErrorMatchMissingBranch
 message_contains:
   - "no branch for constructor suc"
-line: 5
+line: 6
+column: 6
 regression_for:
   - match-branch-bijection
diff --git a/test/typecheck/cases/ill-match-missing-path-branch.expect.yaml b/test/typecheck/cases/ill-match-missing-path-branch.expect.yaml
--- a/test/typecheck/cases/ill-match-missing-path-branch.expect.yaml
+++ b/test/typecheck/cases/ill-match-missing-path-branch.expect.yaml
@@ -2,6 +2,7 @@
 error_tag: TypeErrorMatchMissingBranch
 message_contains:
   - "match has no branch for constructor loop"
-line: 6
+line: 7
+column: 6
 regression_for:
   - data-stage3-path-constructors
diff --git a/test/typecheck/cases/ill-match-not-data.expect.yaml b/test/typecheck/cases/ill-match-not-data.expect.yaml
--- a/test/typecheck/cases/ill-match-not-data.expect.yaml
+++ b/test/typecheck/cases/ill-match-not-data.expect.yaml
@@ -3,6 +3,7 @@
 message_contains:
   - "match scrutinee"
   - "is not of a #data type"
-line: 3
+line: 4
+column: 6
 regression_for:
   - match-scrutinee-data-former
diff --git a/test/typecheck/cases/ill-match-unknown-branch.expect.yaml b/test/typecheck/cases/ill-match-unknown-branch.expect.yaml
--- a/test/typecheck/cases/ill-match-unknown-branch.expect.yaml
+++ b/test/typecheck/cases/ill-match-unknown-branch.expect.yaml
@@ -3,6 +3,7 @@
 message_contains:
   - "match branch for succ"
   - "not a constructor"
-line: 5
+line: 6
+column: 6
 regression_for:
   - match-branch-bijection
diff --git a/test/typecheck/cases/ill-modal-let-into-body.expect.yaml b/test/typecheck/cases/ill-modal-let-into-body.expect.yaml
--- a/test/typecheck/cases/ill-modal-let-into-body.expect.yaml
+++ b/test/typecheck/cases/ill-modal-let-into-body.expect.yaml
@@ -2,7 +2,8 @@
 error_tag: TypeErrorUnify
 message_contains:
   - "cannot unify expected type"
-line: 6
+line: 12
+column: 46
 regression_for:
   - "let-mod-into-motive-checks-body"
   - "https://github.com/rzk-lang/rzk/pull/327"
diff --git a/test/typecheck/cases/ill-recover-after-body-error.expect.yaml b/test/typecheck/cases/ill-recover-after-body-error.expect.yaml
new file mode 100644
--- /dev/null
+++ b/test/typecheck/cases/ill-recover-after-body-error.expect.yaml
@@ -0,0 +1,11 @@
+status: error
+api: collect
+error_tag: TypeErrorUnify
+message_contains:
+  - "cannot unify expected type"
+line: 7
+column: 6
+error_count: 2
+regression_for:
+  - "continue-checking-after-a-failed-definition-body"
+  - "https://github.com/rzk-lang/rzk/issues/81"
diff --git a/test/typecheck/cases/ill-recover-after-body-error.rzk b/test/typecheck/cases/ill-recover-after-body-error.rzk
new file mode 100644
--- /dev/null
+++ b/test/typecheck/cases/ill-recover-after-body-error.rzk
@@ -0,0 +1,13 @@
+#lang rzk-1
+
+-- The proof of `broken` does not check, but its type does, so it is entered
+-- as a postulate and the rest of the file is checked against it: `uses-broken`
+-- uses it and checks, and the separate error in `also-broken` is reported too.
+#define broken (A : U) (a : A) : A
+  := A
+
+#define uses-broken (A : U) (a : A) : A
+  := broken A a
+
+#define also-broken (A : U) (a : A) : A
+  := U
diff --git a/test/typecheck/cases/ill-recover-after-type-error.expect.yaml b/test/typecheck/cases/ill-recover-after-type-error.expect.yaml
new file mode 100644
--- /dev/null
+++ b/test/typecheck/cases/ill-recover-after-type-error.expect.yaml
@@ -0,0 +1,9 @@
+status: error
+api: collect
+error_tag: TypeErrorNotFunction
+line: 6
+column: 28
+error_count: 3
+regression_for:
+  - "continue-checking-after-a-failed-declaration-type"
+  - "https://github.com/rzk-lang/rzk/issues/81"
diff --git a/test/typecheck/cases/ill-recover-after-type-error.rzk b/test/typecheck/cases/ill-recover-after-type-error.rzk
new file mode 100644
--- /dev/null
+++ b/test/typecheck/cases/ill-recover-after-type-error.rzk
@@ -0,0 +1,13 @@
+#lang rzk-1
+
+-- The type of `bad-type` does not check, so nothing is entered for it and
+-- `uses-it` reports an undefined variable. The unrelated error below is
+-- reported too, instead of the file stopping at the first one.
+#define bad-type (A : U) : A A
+  := A
+
+#define uses-it (A : U) : A -> A
+  := \ x -> bad-type A
+
+#define also-wrong (A : U) (a : A) : A
+  := U