rzk 0.7.6 → 0.7.7
raw patch · 4 files changed
+253/−201 lines, 4 filesdep ~mtl
Dependency ranges changed: mtl
Files
- ChangeLog.md +15/−0
- rzk.cabal +6/−6
- src/Language/Rzk/VSCode/Handlers.hs +2/−1
- src/Rzk/TypeCheck.hs +230/−194
ChangeLog.md view
@@ -6,6 +6,21 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.7 — 2025-11-04++Important fixes:++- Fix subtyping (automatic coercion for extension types and tope disjunction elimination) (see [#207](https://github.com/rzk-lang/rzk/pull/207))++ 1. Do not assume variance for the argument of function/type family application (fixes #206).+ 2. Separately check tope families and extension types (and $\Pi$-types), since, for tope families, variance of the argument is different.+ 3. Fix `refl` to check for equality, not subtyping.+ 4. Fix `inferAs` to perform `typecheck` instead (where appropriate).++Minor fix:++- Add version bounds for successful Hackage upload (see [`9aba39c`](https://github.com/rzk-lang/rzk/commit/9aba39c9d63799a00438774e947a986fe8bb9d69))+ ## v0.7.6 — 2025-08-14 Minor fixes:
rzk.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.24 --- This file has been generated from package.yaml by hpack version 0.38.0.+-- This file has been generated from package.yaml by hpack version 0.38.1. -- -- see: https://github.com/sol/hpack name: rzk-version: 0.7.6+version: 0.7.7 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@@ -73,7 +73,7 @@ , bifunctors >=5.5.3 , bytestring >=0.10.8.2 , directory >=1.2.7.0- , mtl >=2.2.2+ , mtl >=2.3.1 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0@@ -119,7 +119,7 @@ , bifunctors >=5.5.3 , bytestring >=0.10.8.2 , directory >=1.2.7.0- , mtl >=2.2.2+ , mtl >=2.3.1 , rzk , template-haskell >=2.14.0.0 , text >=1.2.3.1@@ -154,7 +154,7 @@ , bytestring >=0.10.8.2 , directory >=1.2.7.0 , doctest >=0.21.0- , mtl >=2.2.2+ , mtl >=2.3.1 , template-haskell >=2.14.0.0 , text >=1.2.3.1 , yaml >=0.11.0.0@@ -187,7 +187,7 @@ , directory >=1.2.7.0 , hspec , hspec-discover- , mtl >=2.2.2+ , mtl >=2.3.1 , rzk , template-haskell >=2.14.0.0 , text >=1.2.3.1
src/Language/Rzk/VSCode/Handlers.hs view
@@ -21,7 +21,8 @@ import Control.Monad (forM_, when) import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError),- modifyError, runExceptT)+ runExceptT)+import Control.Monad.Error.Class (modifyError) import Control.Monad.IO.Class (MonadIO (..)) import Data.Default.Class import Data.List (isSuffixOf, sort, (\\))
src/Rzk/TypeCheck.hs view
@@ -523,9 +523,9 @@ , " " <> show (untyped term) ] ActionUnifyTerms expected actual ->- [ "unifying term"+ [ "unifying term (expected)" , " " <> show expected- , "with term"+ , "with term (actual)" , " " <> show actual ] ActionInfer term ->@@ -609,7 +609,8 @@ data Covariance = Covariant -- ^ Positive position.- | Contravariant -- ^ Negative position+ | Contravariant -- ^ Negative position.+ | Invariant -- ^ Unknown position. data RenderBackend = RenderSVG@@ -1328,7 +1329,12 @@ where switch Covariant = Contravariant switch Contravariant = Covariant+ switch Invariant = Invariant +setVariance :: Covariance -> TypeCheck var a -> TypeCheck var a+setVariance variance = local $ \Context{..} -> Context+ { covariance = variance, .. }+ enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var) enterScopeContext orig ty context = addVarInCurrentScope Z VarInfo@@ -1859,7 +1865,7 @@ unifyViaDecompose expected actual | expected == actual = return () unifyViaDecompose (AppT _ f x) (AppT _ g y) = do unify Nothing f g- unify Nothing x y+ setVariance Invariant $ unify Nothing x y unifyViaDecompose _ _ = issueTypeError (TypeErrorOther "cannot decompose") unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var ()@@ -1867,205 +1873,223 @@ unifyViaDecompose expected actual `catchError` \_ -> do -- NOTE: this gives a small, but noticeable speedup expectedVal <- whnfT expected actualVal <- whnfT actual- (expected', actual') <- asks covariance >>= \case- Covariant -> etaMatch mterm expectedVal actualVal- Contravariant -> swap <$> etaMatch mterm actualVal expectedVal- unless (expected' == actual') $ do -- NOTE: this gives a small, but noticeable speedup- case actual' of- RecBottomT{} -> return ()- RecOrT _ty rs' ->- case expected' of- RecOrT _ty rs -> sequence_ $- checkCoherence <$> rs <*> rs'- _ -> do- forM_ rs' $ \(tope, term) ->- localTope tope $- unifyTerms expected' term- _ -> typeOf expected' >>= typeOf >>= \case- UniverseCubeT{} -> contextEntails (topeEQT expected' actual')- _ -> do- let def = unless (expected' == actual') err- err =- case mterm of- Nothing -> issueTypeError (TypeErrorUnifyTerms expected' actual')- Just term -> issueTypeError (TypeErrorUnify term expected' actual')- errS = do- let expectedS = S <$> expected'- actualS = S <$> actual'- case mterm of- Nothing -> issueTypeError (TypeErrorUnifyTerms expectedS actualS)- Just term -> issueTypeError (TypeErrorUnify (S <$> term) expectedS actualS)- case expected' of- Pure{} -> def-- UniverseT{} -> def- UniverseCubeT{} -> def- UniverseTopeT{} -> def+ mea <- asks covariance >>= \case+ Covariant -> Just <$> etaMatch mterm expectedVal actualVal+ Contravariant -> Just . swap <$> etaMatch mterm actualVal expectedVal+ Invariant -> traceTypeCheck Debug "invariant" $ do+ -- FIXME: inefficient+ traceTypeCheck Debug "invariant->covariant" $ + setVariance Covariant $ unifyInCurrentContext mterm expectedVal actualVal+ traceTypeCheck Debug "invariant->contravariant" $ + setVariance Contravariant $ unifyInCurrentContext mterm expectedVal actualVal+ return Nothing+ case mea of+ Nothing -> return ()+ Just (expected', actual') ->+ unless (expected' == actual') $ do -- NOTE: this gives a small, but noticeable speedup+ case actual' of+ RecBottomT{} -> return ()+ RecOrT _ty rs' ->+ case expected' of+ RecOrT _ty rs -> sequence_ $+ checkCoherence <$> rs <*> rs'+ _ -> do+ forM_ rs' $ \(tope, term) ->+ localTope tope $+ unifyTerms expected' term+ _ -> typeOf expected' >>= typeOf >>= \case+ UniverseCubeT{} -> contextEntails (topeEQT expected' actual')+ _ -> do+ let def = unless (expected' == actual') err+ err =+ case mterm of+ Nothing -> issueTypeError (TypeErrorUnifyTerms expected' actual')+ Just term -> issueTypeError (TypeErrorUnify term expected' actual')+ errS = do+ let expectedS = S <$> expected'+ actualS = S <$> actual'+ case mterm of+ Nothing -> issueTypeError (TypeErrorUnifyTerms expectedS actualS)+ Just term -> issueTypeError (TypeErrorUnify (S <$> term) expectedS actualS)+ case expected' of+ Pure{} -> def - TypeUnitT{} -> def- UnitT{} -> return () -- Unit always unifies!+ UniverseT{} -> def+ UniverseCubeT{} -> def+ UniverseTopeT{} -> def - CubeUnitT{} -> def- CubeUnitStarT{} -> def- Cube2T{} -> def- Cube2_0T{} -> def- Cube2_1T{} -> def- CubeProductT _ l r ->- case actual' of- CubeProductT _ l' r' -> do- unifyTerms l l'- unifyTerms r r'- _ -> err+ TypeUnitT{} -> def+ UnitT{} -> return () -- Unit always unifies! - PairT _ty l r ->- case actual' of- PairT _ty' l' r' -> do- unifyTerms l l'- unifyTerms r r'+ CubeUnitT{} -> def+ CubeUnitStarT{} -> def+ Cube2T{} -> def+ Cube2_0T{} -> def+ Cube2_1T{} -> def+ CubeProductT _ l r ->+ case actual' of+ CubeProductT _ l' r' -> do+ unifyTerms l l'+ unifyTerms r r'+ _ -> err - -- one part of eta-expansion for pairs- -- FIXME: add symmetric version!- _ -> err+ PairT _ty l r ->+ case actual' of+ PairT _ty' l' r' -> do+ unifyTerms l l'+ unifyTerms r r' - FirstT _ty t ->- case actual' of- FirstT _ty' t' -> unifyTerms t t'- _ -> err+ -- one part of eta-expansion for pairs+ -- FIXME: add symmetric version!+ _ -> err - SecondT _ty t ->- case actual' of- SecondT _ty' t' -> unifyTerms t t'- _ -> err+ FirstT _ty t ->+ case actual' of+ FirstT _ty' t' -> unifyTerms t t'+ _ -> err - TopeTopT{} -> unifyTopes expected' actual'- TopeBottomT{} -> unifyTopes expected' actual'- TopeEQT{} -> unifyTopes expected' actual'- TopeLEQT{} -> unifyTopes expected' actual'- TopeAndT{} -> unifyTopes expected' actual'- TopeOrT{} -> unifyTopes expected' actual'+ SecondT _ty t ->+ case actual' of+ SecondT _ty' t' -> unifyTerms t t'+ _ -> err - RecBottomT{} -> return () -- unifies with anything- RecOrT _ty rs ->- case actual' of- -- ----------------------------------------------- -- IMPORTANT: this pattern matching is redundant,- -- but it is not obvious, so- -- take care when refactoring!- -- ----------------------------------------------- -- RecOrT _ty rs' -> sequence_ $- -- checkCoherence <$> rs <*> rs'- -- ----------------------------------------------- _ -> do- forM_ rs $ \(tope, term) ->- localTope tope $- unifyTerms term actual'+ TopeTopT{} -> unifyTopes expected' actual'+ TopeBottomT{} -> unifyTopes expected' actual'+ TopeEQT{} -> unifyTopes expected' actual'+ TopeLEQT{} -> unifyTopes expected' actual'+ TopeAndT{} -> unifyTopes expected' actual'+ TopeOrT{} -> unifyTopes expected' actual' - TypeFunT _ty _orig cube mtope ret ->- case actual' of- TypeFunT _ty' orig' cube' mtope' ret' -> do- switchVariance $ -- unifying in the negative position!- unifyTerms cube cube' -- FIXME: unifyCubes- enterScope orig' cube $ do- case ret' of- -- UniverseTopeT{} ->- -- (Just tope, Just tope') -> do- -- topeNF <- nfT tope- -- topeNF' <- nfT tope'- -- unifyTopes topeNF topeNF'- -- (Nothing, Nothing) -> return ()- -- (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)- -- (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT- _ -> case (mtope, mtope') of- (Just tope, Just tope') -> do- topeNF <- nfT tope- topeNF' <- nfT tope'- unifyTopes topeNF topeNF'- (Nothing, Nothing) -> return ()- (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)- (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT- case mterm of- Nothing -> unifyTerms ret ret'- Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'- _ -> err+ RecBottomT{} -> return () -- unifies with anything+ RecOrT _ty rs ->+ case actual' of+ -- ----------------------------------------------+ -- IMPORTANT: this pattern matching is redundant,+ -- but it is not obvious, so+ -- take care when refactoring!+ -- ----------------------------------------------+ -- RecOrT _ty rs' -> sequence_ $+ -- checkCoherence <$> rs <*> rs'+ -- ----------------------------------------------+ _ -> do+ forM_ rs $ \(tope, term) ->+ localTope tope $+ unifyTerms term actual' - TypeSigmaT _ty _orig a b ->- case actual' of- TypeSigmaT _ty' orig' a' b' -> do- unify Nothing a a'- enterScope orig' a $ unify Nothing b b'- _ -> err+ TypeFunT _ty _orig cube mtope ret ->+ case actual' of+ TypeFunT _ty' orig' cube' mtope' ret' -> do+ switchVariance $ -- unifying in the negative position!+ unifyTerms cube cube' -- FIXME: unifyCubes+ enterScope orig' cube $ do+ case ret' of+ UniverseTopeT{} -> do+ -- This is the case for tope families (shapes)+ --+ -- (Λ → TOPE) <: (Δ → TOPE)+ -- since if φ : Λ → TOPE+ -- then φ ⊢ Δ+ --+ -- we DO NOT take tope context Φ into account!+ expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope+ actualTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope'+ actualEntailsExpected <- [actualTopeNF] `entailM` expectedTopeNF+ unless actualEntailsExpected $+ issueTypeError (TypeErrorTopeNotSatisfied [actualTopeNF] expectedTopeNF)+ _ -> do+ -- this is the case for Π-types and extension types+ --+ -- Ξ | Φ | Γ ⊢ {t : I | φ} → A t <: {s : J | ψ} → B s+ -- when+ -- Ξ | Φ, ψ ⊢ φ+ expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope+ actualTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope'+ localTope expectedTopeNF $+ contextEntails actualTopeNF+ case mterm of+ Nothing -> unifyTerms ret ret'+ Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'+ _ -> err - TypeIdT _ty x _tA y ->- case actual' of- TypeIdT _ty' x' _tA' y' -> do- -- unify Nothing tA tA' -- TODO: do we need this check?- unify Nothing x x'- unify Nothing y y'- _ -> err+ TypeSigmaT _ty _orig a b ->+ case actual' of+ TypeSigmaT _ty' orig' a' b' -> do+ unify Nothing a a'+ enterScope orig' a' $ unify Nothing b b'+ _ -> err - AppT _ty f x ->- case actual' of- AppT _ty' f' x' -> do- unify Nothing f f'- unify Nothing x x'- _ -> err+ TypeIdT _ty x _tA y ->+ case actual' of+ TypeIdT _ty' x' _tA' y' -> do+ -- unify Nothing tA tA' -- TODO: do we need this check?+ unify Nothing x x'+ unify Nothing y y'+ _ -> err - LambdaT ty _orig _mparam body ->- case stripTypeRestrictions (infoType ty) of- TypeFunT _ty _origF param mtope _ret ->+ AppT _ty f x -> case actual' of- LambdaT ty' orig' _mparam' body' -> do- case stripTypeRestrictions (infoType ty') of- TypeFunT _ty' _origF' param' mtope' _ret' -> do- unify Nothing param param'- enterScope orig' param $ do- case (mtope, mtope') of- (Just tope, Just tope') -> do- unify Nothing tope tope'- localTope tope $ unify Nothing body body'- (Nothing, Nothing) -> do- unify Nothing body body'- _ -> errS+ AppT _ty' f' x' -> do+ unify Nothing f f'+ setVariance Invariant $+ unify Nothing x x'+ _ -> err++ LambdaT ty _orig _mparam body ->+ case stripTypeRestrictions (infoType ty) of+ TypeFunT _ty _origF param mtope _ret ->+ case actual' of+ LambdaT ty' orig' _mparam' body' -> do+ case stripTypeRestrictions (infoType ty') of+ TypeFunT _ty' _origF' param' mtope' _ret' -> do+ unify Nothing param param' -- we (should) have already checked this in types!+ enterScope orig' param $ do+ case (mtope, mtope') of+ (Just tope, Just tope') -> do+ unify Nothing tope tope' -- we (should) have already checked this in types!+ localTope tope $ unify Nothing body body'+ (Nothing, Nothing) -> do+ unify Nothing body body'+ _ -> errS+ _ -> err _ -> err _ -> err- _ -> err - ReflT ty _x | TypeIdT _ty x _tA y <- infoType ty ->- case actual' of- ReflT ty' _x' | TypeIdT _ty' x' _tA' y' <- infoType ty' -> do- -- unify Nothing tA tA' -- TODO: do we need this check?- unify Nothing x x'- unify Nothing y y'- _ -> err- ReflT{} -> panicImpossible "refl with a non-identity type!"+ ReflT ty _x | TypeIdT _ty x _tA y <- infoType ty ->+ case actual' of+ ReflT ty' _x' | TypeIdT _ty' x' _tA' y' <- infoType ty' -> do+ -- unify Nothing tA tA' -- TODO: do we need this check?+ unify Nothing x x'+ unify Nothing y y'+ _ -> err+ ReflT{} -> panicImpossible "refl with a non-identity type!" - IdJT _ty a b c d e f ->- case actual' of- IdJT _ty' a' b' c' d' e' f' -> do- unify Nothing a a'- unify Nothing b b'- unify Nothing c c'- unify Nothing d d'- unify Nothing e e'- unify Nothing f f'- _ -> err+ IdJT _ty a b c d e f ->+ case actual' of+ IdJT _ty' a' b' c' d' e' f' -> do+ unify Nothing a a'+ unify Nothing b b'+ unify Nothing c c'+ unify Nothing d d'+ unify Nothing e e'+ unify Nothing f f'+ _ -> err - TypeAscT{} -> panicImpossible "type ascription at the root of WHNF"+ TypeAscT{} -> panicImpossible "type ascription at the root of WHNF" - TypeRestrictedT _ty ty rs ->- case actual' of- TypeRestrictedT _ty' ty' rs' -> do- unify mterm ty ty'- sequence_- [ localTope tope $ do- -- FIXME: can do less entails checks?- contextEntails (foldr topeOrT topeBottomT (map fst rs')) -- expected is less specified than actual- forM_ rs' $ \(tope', term') -> do- localTope tope' $- unify Nothing term term'- | (tope, term) <- rs- ]- _ -> err -- FIXME: need better unification for restrictions+ TypeRestrictedT _ty ty rs ->+ case actual' of+ TypeRestrictedT _ty' ty' rs' -> do+ unify mterm ty ty'+ sequence_+ [ localTope tope $ do+ -- FIXME: can do less entails checks?+ contextEntails (foldr topeOrT topeBottomT (map fst rs')) -- expected is less specified than actual+ forM_ rs' $ \(tope', term') -> do+ localTope tope' $+ unify Nothing term term'+ | (tope, term) <- rs+ ]+ _ -> err -- FIXME: need better unification for restrictions where action = case mterm of@@ -2460,10 +2484,10 @@ xty' <- typecheck xty universeT unifyTerms tA xty' x' <- typecheck x tA- unifyTerms x' y- unifyTerms x' z+ unifyTerms x' y >> unifyTerms y x'+ unifyTerms x' z >> unifyTerms z x' when (isNothing mx) $- unifyTerms y z+ unifyTerms y z >> unifyTerms z y return (reflT ty' (Just (y, Just tA))) _ -> issueTypeError $ TypeErrorUnexpectedRefl term ty @@ -2517,7 +2541,15 @@ lt <- typeOf l' rt <- typeOf r' typeOf lt >>= \case+ -- Γ ⊢ l ⇒ (I : CUBE)+ -- Γ ⊢ r ⇒ (J : CUBE)+ -- ———————————————————————————+ -- Γ ⊢ (l, r) ⇒ (I × J : CUBE) UniverseCubeT{} -> return (pairT (cubeProductT lt rt) l' r')+ -- Γ ⊢ l ⇒ (A : U)+ -- Γ ⊢ r ⇒ (B : U)+ -- ———————————————————————————+ -- Γ ⊢ (l, r) ⇒ (A × B : U) where A × B = Σ (_ : A), B _ -> do -- NOTE: infer as a non-dependent pair! return (pairT (typeSigmaT Nothing lt (S <$> rt)) l' r')@@ -2573,6 +2605,11 @@ contextEntails topeBottomT return recBottomT + -- Γ ⊢ t ⇒ (T : K)+ -- Γ ⊢ K ≡ U+ -- —————————————+ -- Γ ⊢ t ⇒ T ⇐ U+ RecOr rs -> do ttts <- forM rs $ \(tope, term) -> do tope' <- typecheck tope topeT@@ -2598,12 +2635,12 @@ issueTypeError $ TypeErrorOther "tope params are illegal" _ -> do mapM_ checkNameShadowing orig- b' <- enterScope orig a' $ inferAs universeT b+ b' <- enterScope orig a' $ typecheck b universeT return (typeFunT orig a' Nothing b') -- an argument can be a cube UniverseCubeT{} -> do mapM_ checkNameShadowing orig- b' <- enterScope orig a' $ inferAs universeT b+ b' <- enterScope orig a' $ typecheck b universeT return (typeFunT orig a' Nothing b') -- an argument can be a shape TypeFunT _ty _orig cube mtope UniverseTopeT{} -> do@@ -2611,7 +2648,7 @@ enterScope orig cube $ do let tope' = appT topeT (S <$> a') (Pure Z) -- eta expand a' localTope tope' $ do- b' <- inferAs universeT b+ b' <- typecheck b universeT case mtope of Nothing -> return (typeFunT orig cube (Just tope') b') Just tope'' -> return (typeFunT orig cube (Just (topeAndT tope'' tope')) b')@@ -2623,13 +2660,13 @@ enterScope orig cube' $ do tope' <- typecheck tope topeT localTope tope' $ do- ret' <- inferAs universeT ret+ ret' <- typecheck ret universeT return (typeFunT orig cube' (Just tope') ret') TypeSigma orig a b -> do- a' <- inferAs universeT a -- FIXME: separate universe of universes from universe of types+ a' <- typecheck a universeT mapM_ checkNameShadowing orig- b' <- enterScope orig a' $ inferAs universeT b+ b' <- enterScope orig a' $ typecheck b universeT return (typeSigmaT orig a' b') TypeId x (Just tA) y -> do@@ -2647,7 +2684,6 @@ App f x -> do f' <- inferAs universeT f fmap stripTypeRestrictions (typeOf f') >>= \case- RecBottomT{} -> pure recBottomT -- FIXME: is this ok? TypeFunT _ty _orig a mtope b -> do x' <- typecheck x a let result = appT (substituteT x' b) f' x'@@ -2732,7 +2768,7 @@ return (idJT ret tA' a' tC' d' x' p') TypeAsc term ty -> do- ty' <- inferAs universeT ty+ ty' <- inferAs universeT ty -- this works on types AND cubes term' <- typecheck term ty' return (typeAscT term' ty')