rzk 0.11.1 → 0.11.2

raw patch · 30 files changed

+754/−231 lines, 30 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +15/−0
• rzk.cabal +5/−1
• src/Language/Rzk/Foil/Convert.hs +27/−7
• src/Language/Rzk/Foil/Print.hs +1/−1
• src/Language/Rzk/Foil/Syntax.hs +130/−59
• src/Language/Rzk/VSCode/Handlers.hs +85/−48
• src/Rzk/Diagnostic.hs +6/−3
• src/Rzk/Format.hs +58/−18
• src/Rzk/TypeCheck/Context.hs +17/−2
• src/Rzk/TypeCheck/Decl.hs +152/−54
• src/Rzk/TypeCheck/Error.hs +4/−2
• src/Rzk/TypeCheck/Eval.hs +4/−7
• src/Rzk/TypeCheck/Judgements.hs +12/−7
• src/Rzk/TypeCheck/Monad.hs +84/−11
• src/Rzk/TypeCheck/Unify.hs +13/−2
• test/Rzk/FormatSpec.hs +20/−1
• test/Rzk/HolesSpec.hs +27/−0
• test/Rzk/TypeCheckSpec.hs +31/−0
• test/typecheck/SCHEMA.md +3/−1
• test/typecheck/cases/ill-match-branch-arity.expect.yaml +2/−1
• test/typecheck/cases/ill-match-duplicate-branch.expect.yaml +2/−1
• test/typecheck/cases/ill-match-missing-branch.expect.yaml +2/−1
• test/typecheck/cases/ill-match-missing-path-branch.expect.yaml +2/−1
• test/typecheck/cases/ill-match-not-data.expect.yaml +2/−1
• test/typecheck/cases/ill-match-unknown-branch.expect.yaml +2/−1
• test/typecheck/cases/ill-modal-let-into-body.expect.yaml +2/−1
• test/typecheck/cases/ill-recover-after-body-error.expect.yaml +11/−0
• test/typecheck/cases/ill-recover-after-body-error.rzk +13/−0
• test/typecheck/cases/ill-recover-after-type-error.expect.yaml +9/−0
• test/typecheck/cases/ill-recover-after-type-error.rzk +13/−0

@@ -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.

@@ -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

@@ -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)

@@ -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 

@@ -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,

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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) [] [] []

@@ -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

@@ -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.

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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`). |

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -3,6 +3,7 @@ message_contains:   - "match branch for succ"   - "not a constructor"-line: 5+line: 6+column: 6 regression_for:   - match-branch-bijection

@@ -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"

@@ -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"

@@ -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

@@ -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"

@@ -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