diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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: diff --git a/rzk.cabal b/rzk.cabal --- a/rzk.cabal +++ b/rzk.cabal @@ -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 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 diff --git a/src/Language/Rzk/Free/Syntax.hs b/src/Language/Rzk/Free/Syntax.hs --- a/src/Language/Rzk/Free/Syntax.hs +++ b/src/Language/Rzk/Free/Syntax.hs @@ -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 diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs --- a/src/Rzk/TypeCheck.hs +++ b/src/Rzk/TypeCheck.hs @@ -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 = diff --git a/test/Rzk/HolesSpec.hs b/test/Rzk/HolesSpec.hs --- a/test/Rzk/HolesSpec.hs +++ b/test/Rzk/HolesSpec.hs @@ -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 diff --git a/test/typecheck/cases/happy-multivar-binder.expect.yaml b/test/typecheck/cases/happy-multivar-binder.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-multivar-binder.expect.yaml @@ -0,0 +1,3 @@ +status: ok +regression_for: + - multivar-binder-desugar-unsafeTermToPattern-crash diff --git a/test/typecheck/cases/happy-multivar-binder.rzk b/test/typecheck/cases/happy-multivar-binder.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-multivar-binder.rzk @@ -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