Skip to content

Commit 20df1a9

Browse files
fizrukfizruk
committed
Merge branch 'release-v0.7.7'
* release-v0.7.7: Bump version and update changelog Fix subtyping for AppT (do not assume variance of the argument) Add version bounds for successful Hackage upload Make refl symmetric and fix inferAs->typecheck Fix subtyping for Sigma-types and leave comments for simingly excessive checks Separate subtype checking for tope families and Pi-types
2 parents a04eeab + 401709b commit 20df1a9

File tree

4 files changed

+296
-232
lines changed

4 files changed

+296
-232
lines changed

‎rzk/ChangeLog.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,21 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
66
and this project adheres to the
77
[Haskell Package Versioning Policy](https://pvp.haskell.org/).
88

9+
## v0.7.7 — 2025-11-04
10+
11+
Important fixes:
12+
13+
- Fix subtyping (automatic coercion for extension types and tope disjunction elimination) (see [#207](https://github.com/rzk-lang/rzk/pull/207))
14+
15+
1. Do not assume variance for the argument of function/type family application (fixes #206).
16+
2. Separately check tope families and extension types (and $\Pi$-types), since, for tope families, variance of the argument is different.
17+
3. Fix `refl` to check for equality, not subtyping.
18+
4. Fix `inferAs` to perform `typecheck` instead (where appropriate).
19+
20+
Minor fix:
21+
22+
- Add version bounds for successful Hackage upload (see [`9aba39c`](https://github.com/rzk-lang/rzk/commit/9aba39c9d63799a00438774e947a986fe8bb9d69))
23+
924
## v0.7.6 — 2025-08-14
1025

1126
Minor fixes:

‎rzk/package.yaml‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
11
name: rzk
2-
version: 0.7.6
2+
version: 0.7.7
33
github: "rzk-lang/rzk"
44
license: BSD3
55
author: "Nikolai Kudasov"
66
maintainer: "[email protected]"
7-
copyright: "2023-2024 Nikolai Kudasov"
7+
copyright: "2023-2025 Nikolai Kudasov"
88

9-
extra-source-files:
9+
extra-doc-files:
1010
- README.md
1111
- ChangeLog.md
12+
13+
extra-source-files:
1214
- grammar/Syntax.cf
1315

1416
synopsis: An experimental proof assistant for synthetic ∞-categories
@@ -64,7 +66,9 @@ ghc-options:
6466
- -Wpartial-fields
6567
- -Wredundant-constraints
6668
- -optP-Wno-nonportable-include-path
67-
- -XDeriveDataTypeable
69+
70+
default-extensions:
71+
- DeriveDataTypeable
6872

6973
library:
7074
source-dirs: src
@@ -126,8 +130,8 @@ tests:
126130
main: doctests.hs
127131
other-modules: []
128132
dependencies:
129-
- base
130-
- doctest
131-
- Glob
132-
- QuickCheck
133-
- template-haskell
133+
base: ">= 4.11.0.0 && < 5.0"
134+
doctest: ">= 0.21.0"
135+
Glob: ">= 0.9.3"
136+
QuickCheck: ">= 2.14"
137+
template-haskell: ">= 2.14.0.0"

‎rzk/rzk.cabal‎

Lines changed: 22 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,27 @@
11
cabal-version: 1.24
22

3-
-- This file has been generated from package.yaml by hpack version 0.37.0.
3+
-- This file has been generated from package.yaml by hpack version 0.38.0.
44
--
55
-- see: https://github.com/sol/hpack
66

77
name: rzk
8-
version: 0.7.6
8+
version: 0.7.7
99
synopsis: An experimental proof assistant for synthetic ∞-categories
1010
description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme>
1111
category: Dependent Types
1212
homepage: https://github.com/rzk-lang/rzk#readme
1313
bug-reports: https://github.com/rzk-lang/rzk/issues
1414
author: Nikolai Kudasov
1515
maintainer: [email protected]
16-
copyright: 2023-2024 Nikolai Kudasov
16+
copyright: 2023-2025 Nikolai Kudasov
1717
license: BSD3
1818
license-file: LICENSE
1919
build-type: Custom
2020
extra-source-files:
21+
grammar/Syntax.cf
22+
extra-doc-files:
2123
README.md
2224
ChangeLog.md
23-
grammar/Syntax.cf
2425

2526
source-repository head
2627
type: git
@@ -57,7 +58,9 @@ library
5758
Paths_rzk
5859
hs-source-dirs:
5960
src
60-
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable
61+
default-extensions:
62+
DeriveDataTypeable
63+
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
6164
build-tools:
6265
alex >=3.2.4
6366
, happy >=1.19.9
@@ -101,7 +104,9 @@ executable rzk
101104
Paths_rzk
102105
hs-source-dirs:
103106
app
104-
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable -threaded -rtsopts -with-rtsopts=-N
107+
default-extensions:
108+
DeriveDataTypeable
109+
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
105110
build-tools:
106111
alex >=3.2.4
107112
, happy >=1.19.9
@@ -132,23 +137,25 @@ test-suite doctests
132137
main-is: doctests.hs
133138
hs-source-dirs:
134139
test
135-
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable
140+
default-extensions:
141+
DeriveDataTypeable
142+
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path
136143
build-tools:
137144
alex >=3.2.4
138145
, happy >=1.19.9
139146
build-tool-depends:
140147
BNFC:bnfc >=2.9.4.1
141148
build-depends:
142-
Glob
143-
, QuickCheck
149+
Glob >=0.9.3
150+
, QuickCheck >=2.14
144151
, array >=0.5.3.0
145-
, base
152+
, base >=4.11.0.0 && <5.0
146153
, bifunctors >=5.5.3
147154
, bytestring >=0.10.8.2
148155
, directory >=1.2.7.0
149-
, doctest
156+
, doctest >=0.21.0
150157
, mtl >=2.2.2
151-
, template-haskell
158+
, template-haskell >=2.14.0.0
152159
, text >=1.2.3.1
153160
, yaml >=0.11.0.0
154161
default-language: Haskell2010
@@ -163,7 +170,9 @@ test-suite rzk-test
163170
Paths_rzk
164171
hs-source-dirs:
165172
test
166-
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -XDeriveDataTypeable -threaded -rtsopts -with-rtsopts=-N
173+
default-extensions:
174+
DeriveDataTypeable
175+
ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -optP-Wno-nonportable-include-path -threaded -rtsopts -with-rtsopts=-N
167176
build-tools:
168177
alex >=3.2.4
169178
, happy >=1.19.9

0 commit comments

Comments
 (0)