rzk 0.9.0 → 0.9.1

raw patch · 7 files changed

+245/−94 lines, 7 filesdep ~Globdep ~QuickCheckdep ~aesonPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: Glob, QuickCheck, aeson, array, bifunctors, bytestring, co-log-core, data-default-class, directory, doctest-parallel, filepath, hspec, hspec-discover, lens, lsp, lsp-types, mtl, optparse-generic, stm, template-haskell, text, with-utf8, yaml

API changes (from Hackage documentation)

Files

• ChangeLog.md +24/−0
• rzk.cabal +61/−59
• src/Language/Rzk/Free/Syntax.hs +22/−0
• src/Rzk/TypeCheck.hs +60/−35
• test/Rzk/HolesSpec.hs +60/−0
• test/typecheck/cases/happy-multivar-binder.expect.yaml +3/−0
• test/typecheck/cases/happy-multivar-binder.rzk +15/−0

@@ -6,6 +6,30 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## Unreleased++## v0.9.1 — 2026-06-26++Fixed:++- In lenient (`--allow-holes`) mode, an unused `#!rzk uses` variable is now tolerated whenever the section contains a hole, not only when the hole sits in the declaration itself. For example, with `#!rzk #def in-progress uses (P) : U := ?` and a hole-free wrapper `#!rzk #def check uses (P) : U := in-progress`, the wrapper's `#!rzk uses (P)` reads as unused only because `#!rzk in-progress` is incomplete; it no longer masks the hole the player is meant to see. Strict mode (the default, and CI) still reports a genuinely unused `#!rzk uses` (see [#262](https://github.com/rzk-lang/rzk/pull/262)).++- A multi-variable binder in a function type, such as `#!rzk (x y : A) → A`, no longer crashes the checker with `expected a pattern but got x y`. It is now desugared into nested one-variable binders `#!rzk (x : A) → (y : A) → A`, as one would expect. The crash was an uncaught `error` reached during translation, so it took down the playground, the game, and the LSP rather than surfacing as a diagnostic; both `rzk typecheck` and the hole query (`--allow-holes`) are fixed (see [#263](https://github.com/rzk-lang/rzk/pull/263)).++- A hole's hint inventory no longer drops a hypothesis or allow-listed lemma whose elimination spine is long. For a goal `#!rzk B` and a lemma `#!rzk deep : A -> A -> A -> A -> A -> A -> A -> A -> B`, the candidate `#!rzk deep ? ? ? ? ? ? ? ?` was silently omitted, because filling each of the eight arguments with a hole spent one unit of the search-depth bound. Filling a function's arguments is a forced spine step, so it no longer counts against the bound; only the genuinely branching eliminators (Σ/cube projections and `#!rzk idJ`) do. This affects only the candidate hints surfaced to the game and the LSP, not the strict `rzk typecheck` path (see [#261](https://github.com/rzk-lang/rzk/pull/261)).++- In lenient (`--allow-holes`) mode, a hole standing for an entire shape-restricted argument is now reported with its goal instead of failing the enclosing extension-type boundary check. When the hole is the whole point of a shape (e.g. a `#!rzk 2 × 2 | Δ¹×Δ¹` point), the surrounding term can unfold to a `#!rzk recOR` whose faces mention the hole (such as `#!rzk π₁ ? ≤ π₂ ?`). Checking an extension-type boundary then enters one of those faces, and a reduction there can drop the hole from the compared terms while the assumed face still depends on it. The boundary mismatch was reported as `cannot unify term`, even though filling the hole makes the term typecheck. A mismatch found under a tope context that still mentions an unfilled hole is now deferred, just like one whose terms still contain a hole. Strict mode (the default, and CI) still reports the hole as unsolved (see [#267](https://github.com/rzk-lang/rzk/pull/267)).++Packaging:++- Add upper bounds on all dependencies, as Hackage asks for. The bounds are at the next super-major version, so a new GHC's boot libraries (`array`, `bytestring`, `directory`, `mtl`, `template-haskell`, `text`) and the pinned Nix/GHCJS package set both stay in range without a Hackage revision on every minor dependency bump. The loose lower bounds are unchanged, so the GHCJS path still resolves (see [#259](https://github.com/rzk-lang/rzk/issues/259), [#134](https://github.com/rzk-lang/rzk/issues/134)).++CI / infrastructure:++- Upgrade the playground's build toolchain to Vite 7 and `tsx` 4.20, picking up the upstream security fixes, and build it with Node 22 under Nix to match (see [#265](https://github.com/rzk-lang/rzk/pull/265)).++- Fix the playground's `ASSET_URL` so the root (`main`) deployment loads its assets from the correct path.+ ## v0.9.0 — 2026-06-24  Added:

@@ -1,11 +1,11 @@ cabal-version: 2.0 --- This file has been generated from package.yaml by hpack version 0.39.6.+-- This file has been generated from package.yaml by hpack version 0.39.1. -- -- see: https://github.com/sol/hpack  name:           rzk-version:        0.9.0+version:        0.9.1 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@@ -31,6 +31,7 @@     test/typecheck/cases/happy-modal-inv.rzk     test/typecheck/cases/happy-modal-tope-unwrap.rzk     test/typecheck/cases/happy-modal-topes.rzk+    test/typecheck/cases/happy-multivar-binder.rzk     test/typecheck/cases/happy-op-hom-to-hom.rzk     test/typecheck/cases/happy-recbot-term-wellformed.rzk     test/typecheck/cases/happy-recor-guard-exceeds-context.rzk@@ -133,6 +134,7 @@     test/typecheck/cases/happy-modal-inv.expect.yaml     test/typecheck/cases/happy-modal-tope-unwrap.expect.yaml     test/typecheck/cases/happy-modal-topes.expect.yaml+    test/typecheck/cases/happy-multivar-binder.expect.yaml     test/typecheck/cases/happy-op-hom-to-hom.expect.yaml     test/typecheck/cases/happy-recbot-term-wellformed.expect.yaml     test/typecheck/cases/happy-recor-guard-exceeds-context.expect.yaml@@ -264,17 +266,17 @@       DeriveDataTypeable   ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path   build-depends:-      Glob >=0.9.3-    , aeson >=1.4-    , array >=0.5.3.0+      Glob >=0.9.3 && <1+    , aeson >=1.4 && <3+    , array >=0.5.3.0 && <1     , base >=4.7 && <5-    , bifunctors >=5.5.3-    , bytestring >=0.10.8.2-    , directory >=1.2.7.0-    , mtl >=2.3.1-    , template-haskell >=2.14.0.0-    , text >=1.2.3.1-    , yaml >=0.11.0.0+    , bifunctors >=5.5.3 && <6+    , bytestring >=0.10.8.2 && <1+    , directory >=1.2.7.0 && <2+    , mtl >=2.2.2 && <3+    , template-haskell >=2.14.0.0 && <3+    , text >=1.2.3.1 && <3+    , yaml >=0.11.0.0 && <1   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)     cpp-options: -DLSP_ENABLED@@ -287,15 +289,15 @@         Language.Rzk.VSCode.Lsp         Language.Rzk.VSCode.Tokenize     build-depends:-        aeson >=2.0.0.0-      , co-log-core >=0.3.2.0-      , data-default-class >=0.1.2.0-      , filepath >=1.4.100.0-      , lens >=5.0.1-      , lsp >=2.4.0.0-      , lsp-types >=2.1.1.0-      , mtl >=2.3.1-      , stm >=2.5.1.0+        aeson >=2.0.0.0 && <3+      , co-log-core >=0.3.2.0 && <1+      , data-default-class >=0.1.2.0 && <1+      , filepath >=1.4.100.0 && <2+      , lens >=5.0.1 && <6+      , lsp >=2.4.0.0 && <3+      , lsp-types >=2.1.1.0 && <3+      , mtl >=2.3.1 && <3+      , stm >=2.5.1.0 && <3  executable rzk   main-is: Main.hs@@ -309,25 +311,25 @@       DeriveDataTypeable   ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N   build-depends:-      Glob >=0.9.3-    , aeson >=1.4-    , array >=0.5.3.0+      Glob >=0.9.3 && <1+    , aeson >=1.4 && <3+    , array >=0.5.3.0 && <1     , base >=4.7 && <5-    , bifunctors >=5.5.3-    , bytestring >=0.10.8.2-    , directory >=1.2.7.0-    , mtl >=2.3.1+    , bifunctors >=5.5.3 && <6+    , bytestring >=0.10.8.2 && <1+    , directory >=1.2.7.0 && <2+    , mtl >=2.2.2 && <3     , rzk-    , template-haskell >=2.14.0.0-    , text >=1.2.3.1-    , yaml >=0.11.0.0+    , template-haskell >=2.14.0.0 && <3+    , text >=1.2.3.1 && <3+    , yaml >=0.11.0.0 && <1   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)     cpp-options: -DLSP_ENABLED   if !impl(ghcjs)     build-depends:-        optparse-generic >=1.4.7-      , with-utf8 >=1.0.3.0+        optparse-generic >=1.4.7 && <2+      , with-utf8 >=1.0.3.0 && <2  test-suite doctests   type: exitcode-stdio-1.0@@ -338,20 +340,20 @@       DeriveDataTypeable   ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path   build-depends:-      Glob >=0.9.3-    , QuickCheck >=2.14-    , aeson >=1.4-    , array >=0.5.3.0+      Glob >=0.9.3 && <1+    , QuickCheck >=2.14 && <3+    , aeson >=1.4 && <3+    , array >=0.5.3.0 && <1     , base >=4.11.0.0 && <5.0-    , bifunctors >=5.5.3-    , bytestring >=0.10.8.2-    , directory >=1.2.7.0-    , doctest-parallel >=0.3-    , mtl >=2.3.1+    , bifunctors >=5.5.3 && <6+    , bytestring >=0.10.8.2 && <1+    , directory >=1.2.7.0 && <2+    , doctest-parallel >=0.3 && <1+    , mtl >=2.2.2 && <3     , rzk-    , template-haskell >=2.14.0.0-    , text >=1.2.3.1-    , yaml >=0.11.0.0+    , template-haskell >=2.14.0.0 && <3+    , text >=1.2.3.1 && <3+    , yaml >=0.11.0.0 && <1   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)     cpp-options: -DLSP_ENABLED@@ -373,23 +375,23 @@       DeriveDataTypeable   ghc-options: -Wall -Wcompat -Widentities -Werror=missing-fields -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N   build-tool-depends:-      hspec-discover:hspec-discover+      hspec-discover:hspec-discover >=2.7 && <3   build-depends:-      Glob >=0.9.3-    , aeson-    , array >=0.5.3.0+      Glob >=0.9.3 && <1+    , aeson >=1.4 && <3+    , array >=0.5.3.0 && <1     , base >=4.7 && <5-    , bifunctors >=5.5.3-    , bytestring >=0.10.8.2-    , directory >=1.2.7.0-    , filepath-    , hspec-    , hspec-discover-    , mtl >=2.3.1+    , bifunctors >=5.5.3 && <6+    , bytestring >=0.10.8.2 && <1+    , directory >=1.2.7.0 && <2+    , filepath >=1.4 && <2+    , hspec >=2.7 && <3+    , hspec-discover >=2.7 && <3+    , mtl >=2.2.2 && <3     , rzk-    , template-haskell >=2.14.0.0-    , text >=1.2.3.1-    , yaml+    , template-haskell >=2.14.0.0 && <3+    , text >=1.2.3.1 && <3+    , yaml >=0.11.0.0 && <1   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)     cpp-options: -DLSP_ENABLED

@@ -356,6 +356,19 @@       Rzk.ReflTermType _loc x tA -> Refl (Just (go x, Just (go tA)))       Rzk.IdJ _loc a b c d e f -> IdJ (go a) (go b) (go c) (go d) (go e) (go f)       Rzk.TypeAsc _loc x t -> TypeAsc (go x) (go t)+      -- A binder may name several variables sharing a type, e.g. (x y : A),+      -- which is parsed as the application spine `x y`. Desugar it into nested+      -- one-variable binders ((x : A) → (y : A) → …) before translating, so the+      -- pattern conversion never sees a juxtaposition. (Shape binders are left+      -- alone: their tope refers to the single bound point.)+      Rzk.TypeFun loc (Rzk.ParamTermType loc' patTerm arg) ret+        | _ : _ : _ <- vars ->+            go (foldr (\v -> Rzk.TypeFun loc (Rzk.ParamTermType loc' v arg)) ret vars)+        where vars = flattenBinderApp patTerm+      Rzk.TypeFun loc (Rzk.ParamTermModalType loc' patTerm mc ty) ret+        | _ : _ : _ <- vars ->+            go (foldr (\v -> Rzk.TypeFun loc (Rzk.ParamTermModalType loc' v mc ty)) ret vars)+        where vars = flattenBinderApp patTerm       Rzk.TypeFun _loc (Rzk.ParamTermModalType _loc' patTerm mc ty) ret ->         let pat = unsafeTermToPattern patTerm             md  = modalColonToTModality mc@@ -489,6 +502,15 @@   Flat  -> Rzk.ModalColonFlat Nothing   Op    -> Rzk.ModalColonOp Nothing   Id    -> Rzk.ModalColonId Nothing++-- | Split a binder term into the individual variables it names. A multi-variable+-- binder like @(x y : A)@ is parsed as the application spine @x y@; this returns+-- @[x, y]@ so each can become its own nested binder. A single binder term (a+-- variable, a pair pattern, …) is returned unchanged as a singleton.+flattenBinderApp :: Rzk.Term -> [Rzk.Term]+flattenBinderApp = \case+  Rzk.App _loc f x -> flattenBinderApp f ++ [x]+  t                -> [t]  unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern unsafeTermToPattern = ttp

@@ -738,29 +738,37 @@ -- -- The search is driven uniformly by the eliminators a (weak head normal) type -- admits (see 'eliminatorsOf'), so adding a new eliminator extends it without--- touching the search. Depth is bounded by 'maxEliminationDepth'.+-- touching the search.+--+-- A Π-application is a forced spine step — there is exactly one way to fill an+-- argument (with a hole) — so it extends the spine for free and does not spend+-- the budget. Only the genuinely branching eliminators (Σ/cube projections and+-- @idJ@, flagged by 'eliminatorsOf') count against 'maxEliminationDepth'. The+-- bound therefore limits real search depth, not argument count, so a lemma that+-- must be applied to many holes is still reached. The free spine terminates+-- because each application strips one Π binder off a finite type. allEliminationsInto   :: Eq var => TermT var -> TermT var -> TypeCheck var [TermT var] allEliminationsInto target = go maxEliminationDepth   where     go depth term = do-      ty   <- typeOf term-      fits <- fitsInto term ty target-      deeper <--        if depth <= 0-          then pure []-          else do-            elims <- eliminatorsOf ty-            concat <$> mapM (\wrap -> go (depth - 1) (wrap term)) elims+      ty    <- typeOf term+      fits  <- fitsInto term ty target+      elims <- eliminatorsOf ty+      let step (SpineStep, wrap) = go depth (wrap term)+          step (Branching, wrap)+            | depth <= 0 = pure []+            | otherwise  = go (depth - 1) (wrap term)+      deeper <- concat <$> mapM step elims       pure ([term | fits] <> deeper) --- | How deep an elimination spine 'allEliminationsInto' will build. A temporary--- fixed bound: seven is enough for the spines seen so far (fully applying a--- five-argument hypothesis and projecting twice), and a larger bound mostly adds--- self-referential spines (a built result applied again). It should be made--- configurable, and likely raised, once there is more evidence of what real--- goals need. The chain only branches at Σ-types, which are shallow, so the--- search stays small.+-- | How many /branching/ eliminators 'allEliminationsInto' will chain. Forced+-- Π-applications are free (see 'allEliminationsInto'), so this bounds only the+-- Σ/cube projections and @idJ@ steps, not the argument count of a spine. A+-- temporary fixed bound: branching is shallow in the goals seen so far (a few+-- projections), and a larger bound mostly adds self-referential spines (a built+-- result eliminated again). It should be made configurable once there is more+-- evidence of what real goals need. maxEliminationDepth :: Int maxEliminationDepth = 7 @@ -784,24 +792,32 @@   censor (const []) $ local structuralHoleUnify     ((unify (Just term) target' ty' >> pure True) `catchError` \_ -> pure False) +-- | Whether eliminating a value spends the search budget. A forced+-- Π-application is a 'SpineStep' — there is one way to fill the argument (with a+-- hole), so 'allEliminationsInto' applies it for free; a 'Branching' eliminator+-- (a Σ/cube projection or @idJ@) costs one against 'maxEliminationDepth'.+data ElimCost = SpineStep | Branching+  deriving (Eq, Show)+ -- | The eliminators a value of the given (weak head normal) type admits, each--- as a function wrapping the eliminated term. A Π-type is eliminated by--- application to a fresh hole; a Σ-type by either projection; an identity type--- by path induction (@idJ@), with the motive and base case left as holes.+-- as a function wrapping the eliminated term, paired with its 'ElimCost'. A+-- Π-type is eliminated by application to a fresh hole (a spine step); a Σ-type+-- by either projection; an identity type by path induction (@idJ@), with the+-- motive and base case left as holes. The projections and @idJ@ branch. -- Anything else admits no simple eliminator.-eliminatorsOf :: Eq var => TermT var -> TypeCheck var [TermT var -> TermT var]+eliminatorsOf :: Eq var => TermT var -> TypeCheck var [(ElimCost, TermT var -> TermT var)] eliminatorsOf ty =   case stripTypeRestrictions ty of     TypeFunT _ty _orig _md param _mtope ret ->-      pure [ \term -> let h = mkHole param in appT (substituteT h ret) term h ]+      pure [ (SpineStep, \term -> let h = mkHole param in appT (substituteT h ret) term h) ]     TypeSigmaT _ty _orig _md a b ->-      pure [ \term -> firstT a term-           , \term -> secondT (substituteT (firstT a term) b) term ]+      pure [ (Branching, \term -> firstT a term)+           , (Branching, \term -> secondT (substituteT (firstT a term) b) term) ]     -- A cube point pair (e.g. a pattern-bound @(t , s) : 2 × 2@) projects to its     -- coordinates; rzk renders those projections back as the pattern names.     CubeProductT _ty a b ->-      pure [ \term -> firstT a term-           , \term -> secondT b term ]+      pure [ (Branching, \term -> firstT a term)+           , (Branching, \term -> secondT b term) ]     -- A path @p : a =_A x@ is eliminated by path induction. The motive     -- @C : (z : A) → (a =_A z) → U@ is always a function, so we introduce it     -- straight away as @\\ b q → ?@ rather than leaving it a bare hole: the spine@@ -825,7 +841,7 @@           d      = mkHole dType           motiveAt y p = appT universeT             (appT (typeFunT (BinderVar Nothing) Id (typeIdT a (Just tA) y) Nothing universeT) c y) p-      pure [ \p -> idJT (motiveAt x p) tA a c d x p ]+      pure [ (Branching, \p -> idJT (motiveAt x p) tA a c d x p) ]     _ -> pure []   where     mkHole t = HoleT TypeInfo{ infoType = t, infoWHNF = Nothing, infoNF = Nothing } Nothing@@ -1501,9 +1517,11 @@ scopeToDecls errs ScopeInfo{..} = do   -- In lenient (hole-checking) mode an as-yet-unfilled hole may still come to   -- use a declared variable, so we tolerate the unused-variable diagnostics-  -- wherever such a hole is present: a hole anywhere in the section for an-  -- unused section assumption, a hole in the declaration itself for an unused-  -- 'uses' variable. Strict mode (the default, and CI) keeps reporting both.+  -- wherever such a hole is present anywhere in the section. This covers both an+  -- unused section assumption and an unused 'uses' variable, and crucially a+  -- hole-free definition whose body refers to an in-progress (hole-bearing) one:+  -- its 'uses' reads as unused only because the referenced definition is+  -- incomplete. Strict mode (the default, and CI) keeps reporting both.   lenient <- not <$> asks holesAreErrors   let sectionHasHole = any (maybe False containsHole . varValue . snd) scopeVars   (decls, errs') <- collectScopeDecls (lenient && sectionHasHole) errs [] scopeVars@@ -1511,8 +1529,7 @@   -- when (null errs) $ do   unusedErrors <- forM decls $ \Decl{..} -> do     let unusedUsedVars = declUsedVars `intersect` map fst scopeVars-        declHasHole    = maybe False containsHole declValue-    if null errs && not (null unusedUsedVars) && not (lenient && declHasHole)+    if null errs && not (null unusedUsedVars) && not (lenient && sectionHasHole)       then do         err <- local (\c -> c { location = declLocation }) $           fromTypeError (TypeErrorUnusedUsedVariables unusedUsedVars declName)@@ -3168,12 +3185,20 @@                   -- unification that would otherwise fail is deferred when either                   -- side still contains an (unfilled) hole — including one nested                   -- in a larger term, e.g. @f ?@ checked against an extension-type-                  -- boundary. 'structuralHoleUnify' turns this off, keeping a-                  -- structural mismatch around a hole an error. Lazy: only runs on-                  -- the failure path.+                  -- boundary. The hole may also sit in the tope context rather+                  -- than the terms: a hole standing for a whole shape point makes+                  -- the enclosing 'recOR' split over hole-dependent faces, and a+                  -- branch reduction can drop the hole from the terms while the+                  -- assumed face (e.g. @π₁ ? ≤ π₂ ?@) still 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. Lazy: only runs on the failure path.                   defer <- asks deferHoleMismatches+                  topeContextHasHole <- asks (any (containsHole . tTope) . localTopes)                   let def = unless (expected' == actual') err-                      holePresent = defer && (containsHole expected' || containsHole actual')+                      holePresent = defer &&+                        (containsHole expected' || containsHole actual' || topeContextHasHole)                       err                         | holePresent = return ()                         | otherwise =

@@ -95,6 +95,18 @@       let holes2 = holesOf "#lang rzk-1\n#define q : (A : U) -> A -> A\n  := \\ A a -> ?\n#define r : (A : U) -> A -> A\n  := \\ A a -> ?\n"       length holes2 `shouldBe` 2 +    -- A multi-variable binder (x y : A) is parsed as the application spine+    -- `x y`; it must be desugared into nested binders rather than crash+    -- `unsafeTermToPattern` ("expected a pattern but got x y"). The hole query+    -- then sees the hypothesis as the nested function type.+    it "handles a hole whose context has a multi-variable binder" $ do+      case holesOf "#lang rzk-1\n#assume A : U\n#def foo (k : (x y : A) → A) : A := ?\n" of+        [h] -> do+          show (holeGoal h) `shouldBe` "A"+          map (show . holeEntryType) (holeTermVars h)+            `shouldContain` ["(x : A) → (y : A) → A"]+        hs  -> expectationFailure ("expected exactly one hole, got " <> show (length hs))+     -- A hole whose elaborated term reaches unification (here the `refl` endpoint)     -- must not panic ("unexpected term in UNIFY"); it unifies with anything.     it "handles a hole that flows into unification" $ do@@ -140,6 +152,33 @@         [h] -> show (holeGoal h) `shouldBe` "A"         hs  -> expectationFailure ("expected exactly one hole, got " <> show (length hs)) +    -- A hole standing for a /whole/ shape-restricted argument under an enclosing+    -- extension-type boundary. The argument unfolds to a recOR whose faces+    -- mention the hole (e.g. @π₁ ? ≤ π₂ ?@); checking the boundary enters such a+    -- face and a branch reduction then drops the hole from the compared terms+    -- (the triangle here, @const-pt A c@, discards its point). So the mismatch+    -- (@a@ vs @c@) is hole-free in the terms even though the assumed face still+    -- mentions the hole. The per-term deferral cannot see it; deferring on a+    -- hole-bearing tope context can, so the hole is reported with its shape goal+    -- rather than rejected. (Before the fix this raised TypeErrorUnifyTerms.)+    it "handles a hole for a whole shape argument under an extension boundary" $ do+      let src = "#lang rzk-1\n\+                \#def Δ¹ : 2 → TOPE := \\ t → TOP\n\+                \#def Δ¹×Δ¹ : (2 × 2) → TOPE := \\ (t , s) → TOP ∧ TOP\n\+                \#def unfold (A : U) (tri : (2 × 2) → A) : Δ¹×Δ¹ → A\n\+                \  := \\ (t , s) → recOR (t ≤ s ↦ tri (s , t) , s ≤ t ↦ tri (t , s))\n\+                \#def const-pt (A : U) (c : A) : (2 × 2) → A := \\ (t , s) → c\n\+                \#def hom (A : U) (x y : A) : U := (t : Δ¹) → A [ t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y ]\n\+                \#def test (A : U) (a b c : A) : hom A a b\n\+                \  := \\ t → unfold A (const-pt A c) ?\n"+      case holesOf src of+        [h] -> do+          show (holeGoal h) `shouldBe` "2 × 2"+          case holeGoalShape h of+            Just (s, tope) -> show tope `shouldBe` ("Δ¹×Δ¹ " <> show s)+            Nothing        -> expectationFailure "expected a shape goal (holeGoalShape)"+        hs  -> expectationFailure ("expected exactly one hole, got " <> show (length hs))+     -- A genuinely completable work-in-progress term is tolerated. The example     -- (the Yoneda game's square-transformation level) feeds an incomplete     -- `codomain-square A is-segal-A a b (f ?) ? ? ? ?` where a value of@@ -369,6 +408,18 @@       flip oneHole (holesWithLemmas ["concat"] src) $ \h ->         (names (holeTermVars h) <> names (holeCubeVars h)) `shouldNotContain` ["concat"] +    -- A lemma fully applied to many arguments is offered: filling a function's+    -- arguments with holes is a forced spine step that does not spend the search+    -- budget, so the eight-argument `deep` reaches the goal even though its spine+    -- is longer than `maxEliminationDepth`. (Regression: argument count used to be+    -- charged against the bound, silently dropping deep lemmas.)+    it "offers a lemma applied to more arguments than maxEliminationDepth" $+      let deepSrc = "#lang rzk-1\n#postulate A : U\n#postulate B : U\n"+                 <> "#postulate deep : A -> A -> A -> A -> A -> A -> A -> A -> B\n"+                 <> "#define goal : B := ?\n"+      in flip oneHole (holesWithLemmas ["deep"] deepSrc) $ \h ->+           cands h `shouldContain` ["deep ? ? ? ? ? ? ? ?"]+   describe "holeIntroductions (type-directed introduction forms)" $ do     let intros = map show . holeIntroductions @@ -475,6 +526,15 @@     it "still reports an unused 'uses' variable with no hole in the declaration" $       errTagsOf (usesSection "#define f uses (x) : U\n  := A")         `shouldContain` ["TypeErrorUnusedUsedVariables"]++    -- A hole-free definition whose body refers to an in-progress (hole-bearing)+    -- one declares 'uses (x)' that reads as unused only because the referenced+    -- definition is incomplete. The section has a hole, so it is tolerated (the+    -- check keys off a hole anywhere in the section, not the declaration alone).+    it "tolerates an unused 'uses' on a hole-free wrapper of a hole-bearing def" $+      errTagsOf (usesSection ("#define in-progress uses (x) : U\n  := ?\n"+                           <> "#define wrapper uses (x) : U\n  := in-progress"))+        `shouldNotContain` ["TypeErrorUnusedUsedVariables"]    -- The goal cell: when the goal is a renderable shape, the hole carries an SVG   -- of that shape, drawn from an abstract inhabitant with the proof term hidden

@@ -0,0 +1,3 @@+status: ok+regression_for:+  - multivar-binder-desugar-unsafeTermToPattern-crash

@@ -0,0 +1,15 @@+#lang rzk-1++-- A multi-variable binder like (x y : A) desugars to nested one-variable+-- binders (x : A) → (y : A) → …, so a function of that type accepts that many+-- arguments. Previously the surface term `x y` crashed `unsafeTermToPattern`.++#define app2 (A : U) (a : A) (k : (x y : A) → A)+  : A+  := k a a++#define app3 (A : U) (a : A) (k : (x y z : A) → A)+  : A+  := k a a a++#check app2 : (A : U) → (a : A) → ((x y : A) → A) → A