From a1926547a29eb4f531735b645f41c6b9367d3709 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 1 Oct 2024 13:39:28 +0200 Subject: [PATCH] Reimplement positivity checker (#3057) - Fixes #3048 - Fixes #3058 Due to #3071 I had to change the order of two lines in tests/Compilation/positive/test079.juvix. --- src/Juvix/Compiler/Internal/Data/Name.hs | 4 + src/Juvix/Compiler/Internal/Language.hs | 2 + src/Juvix/Compiler/Internal/Pretty/Base.hs | 40 ++ .../FromInternal/Analysis/Positivity.hs | 2 - .../Analysis/Positivity/Checker.hs | 498 ++++++++++-------- .../Analysis/Positivity/ConstructorArg.hs | 67 +++ .../Positivity/ConstructorArg/Base.hs | 27 + .../FromInternal/Analysis/Positivity/Error.hs | 18 - .../Analysis/Positivity/Occurrences.hs | 87 +++ .../Analysis/TypeChecking/CheckerNew.hs | 44 +- .../Analysis/TypeChecking/Data/Inference.hs | 1 + .../TypeChecking/Data/ResultBuilder.hs | 16 +- .../Analysis/TypeChecking/Error.hs | 10 +- .../Analysis/TypeChecking/Error/Types.hs | 64 +++ .../Analysis/TypeChecking/Traits/Resolver.hs | 7 +- .../Store/Internal/Data/PolarityTable.hs | 18 + .../Store/Internal/Data/TypeCheckingTables.hs | 5 + src/Juvix/Compiler/Store/Internal/Language.hs | 26 +- src/Juvix/Data.hs | 2 + src/Juvix/Data/Polarity.hs | 30 ++ src/Juvix/Prelude/Base/Foundation.hs | 17 + test/Typecheck/Negative.hs | 61 +-- test/Typecheck/NegativeNew.hs | 7 +- test/Typecheck/Positive.hs | 11 +- tests/Compilation/positive/test079.juvix | 4 +- tests/negative/Internal/Positivity/box.juvix | 5 + .../Internal/Positivity2/Package.juvix | 9 + .../positive/Internal/Positivity2/main.juvix | 58 ++ tests/positive/issue3048/Other.juvix | 5 + tests/positive/issue3048/Package.juvix | 10 + tests/positive/issue3048/main.juvix | 16 + 31 files changed, 821 insertions(+), 350 deletions(-) create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs delete mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs create mode 100644 src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs create mode 100644 src/Juvix/Data/Polarity.hs create mode 100644 tests/negative/Internal/Positivity/box.juvix create mode 100644 tests/positive/Internal/Positivity2/Package.juvix create mode 100644 tests/positive/Internal/Positivity2/main.juvix create mode 100644 tests/positive/issue3048/Other.juvix create mode 100644 tests/positive/issue3048/Package.juvix create mode 100644 tests/positive/issue3048/main.juvix diff --git a/src/Juvix/Compiler/Internal/Data/Name.hs b/src/Juvix/Compiler/Internal/Data/Name.hs index 1d2596358c..5060a270ab 100644 --- a/src/Juvix/Compiler/Internal/Data/Name.hs +++ b/src/Juvix/Compiler/Internal/Data/Name.hs @@ -103,6 +103,10 @@ type ConstrName = Name type InductiveName = Name +type InductiveId = NameId + +type InductiveParam = Name + fromConcreteSymbol :: Interval -> S.Symbol -> Name fromConcreteSymbol loc s = fromConcreteSymbolPretty loc (S.symbolText s) s diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 662c691513..4f080319b8 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -484,6 +484,8 @@ data NormalizedExpression = NormalizedExpression } makePrisms ''Expression +makePrisms ''MutualStatement + makeLenses ''SideIfBranch makeLenses ''SideIfs makeLenses ''CaseBranchRhs diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 40b10142eb..490ae9305b 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -11,11 +11,13 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo import Juvix.Compiler.Internal.Data.TypedHole import Juvix.Compiler.Internal.Language import Juvix.Compiler.Internal.Pretty.Options +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity qualified as New import Juvix.Compiler.Store.Internal.Data.InfoTable import Juvix.Data.CodeAnn import Juvix.Data.Keyword.All qualified as Kw import Juvix.Prelude +import Prettyprinter qualified as PP doc :: (PrettyCode c) => Options -> c -> Doc Ann doc opts = @@ -407,6 +409,35 @@ instance PrettyCode TypedHole where vars <- ppCode _typedHoleLocalVars return (h <+> kwColon <+> ty <> kwAt <> vars) +instance PrettyCode Polarity where + ppCode = return . annotate AnnKeyword . pretty + +instance (PrettyCode k, PrettyCode v) => PrettyCode (HashMap k v) where + ppCode m = do + res <- forM (HashMap.toList m) $ \(k, v) -> do + k' <- ppCode k + v' <- ppCode v + return (k' <+> "↦" <+> v') + return (bracesEncloseIndent res) + +instance PrettyCode AppLhs where + ppCode = \case + AppVar v -> ppCode v + AppAxiom v -> ppCode v + AppInductive v -> ppCode v + +instance PrettyCode FunctionSide where + ppCode = return . annotate AnnKeyword . pretty + +instance PrettyCode Occurrences where + ppCode Occurrences {..} = do + ps <- ppCode _occurrences + return + ( bracesEncloseIndent + [ header "occurrences" <+> kwAssign <+> ps + ] + ) + instance PrettyCode InfoTable where ppCode tbl = do inds <- ppCode (HashMap.keys (tbl ^. infoInductives)) @@ -463,6 +494,15 @@ instance (PrettyCode a) => PrettyCode (Maybe a) where Nothing -> return "Nothing" Just p -> ("Just" <+>) <$> ppCode p +bracesEncloseIndent :: forall l ann. (Foldable l) => l (Doc ann) -> Doc ann +bracesEncloseIndent ls = + PP.group $ + "{" + <> line' + <> indent' (concatWith (\x y -> x <> ";" <> line <> y) ls) + <> line' + <> "}" + tuple :: [Doc ann] -> Doc ann tuple = encloseSep "(" ")" ", " diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs index 98c2a83dc7..d7b22f9cf7 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity.hs @@ -1,8 +1,6 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error, ) where import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs index c319a4fb11..34ff4ea98b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -1,251 +1,283 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker where +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker + ( checkPositivity, + ) +where import Data.HashMap.Strict qualified as HashMap import Data.HashSet qualified as HashSet import Juvix.Compiler.Internal.Data.InfoTable import Juvix.Compiler.Internal.Extra -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error +import Juvix.Compiler.Internal.Pretty +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Inference +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.ResultBuilder import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error -import Juvix.Compiler.Pipeline.EntryPoint qualified as E import Juvix.Prelude hiding (fromEither) -type NegativeTypeParameters = HashSet VarName - -type CheckPositivityEffects r = - Members - '[ Reader E.EntryPoint, - Reader InfoTable, - Error TypeCheckerError, - Inference, - State NegativeTypeParameters - ] - r - -data CheckPositivityArgs = CheckPositivityArgs - { _checkPositivityArgsInductive :: InductiveInfo, - _checkPositivityArgsConstructorName :: Name, - _checkPositivityArgsInductiveName :: Name, - _checkPositivityArgsRecursionLimit :: Int, - _checkPositivityArgsErrorReference :: Maybe Expression, - _checkPositivityArgsTypeOfConstructorArg :: Expression +data Builder = Builder + { _builderPolarities :: HashMap InductiveParam Polarity, + _builderBlocking :: [Blocking] } -makeLenses ''CheckPositivityArgs +data Blocking = Blocking + { _blockingContext :: Polarity, + _blockingUnblocker :: InductiveParam, + -- | The unblocker has to have at least this polarity to unblock + _blockingUnblockerMinimum :: Polarity, + _blockingOccurrences :: Occurrences + } + +makeLenses ''Blocking +makeLenses ''Builder + +emptyBuilder :: Builder +emptyBuilder = + Builder + { _builderPolarities = mempty, + _builderBlocking = mempty + } + +functionSidePolarity :: FunctionSide -> Polarity +functionSidePolarity = \case + FunctionLeft -> PolarityNonStrictlyPositive + FunctionRight -> PolarityStrictlyPositive checkPositivity :: forall r. - (CheckPositivityEffects r) => - InductiveInfo -> + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + ResultBuilder, + Inference + ] + r + ) => + Bool -> + MutualBlock -> Sem r () -checkPositivity indInfo = do - unlessM (asks (^. E.entryPointNoPositivity)) $ - forM_ (indInfo ^. inductiveInfoConstructors) $ \ctorName -> do - ctor <- asks (fromJust . HashMap.lookup ctorName . (^. infoConstructors)) - unless (indInfo ^. inductiveInfoPositive) $ do - numInductives <- HashMap.size <$> asks (^. infoInductives) - forM_ - (constructorArgs (ctor ^. constructorInfoType)) - $ \typeOfConstr -> - checkStrictlyPositiveOccurrences - ( CheckPositivityArgs - { _checkPositivityArgsInductive = indInfo, - _checkPositivityArgsConstructorName = ctorName, - _checkPositivityArgsInductiveName = indInfo ^. inductiveInfoName, - _checkPositivityArgsRecursionLimit = numInductives, - _checkPositivityArgsErrorReference = Nothing, - _checkPositivityArgsTypeOfConstructorArg = typeOfConstr ^. paramType - } - ) - -checkStrictlyPositiveOccurrences :: - forall r. - (CheckPositivityEffects r) => - CheckPositivityArgs -> - Sem r () -checkStrictlyPositiveOccurrences p = do - typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg) - goExpression False typeOfConstrArg +checkPositivity noPositivityFlag mut = do + let ldefs :: [InductiveDef] = + mut + ^.. mutualStatements + . each + . _StatementInductive + + whenJust (nonEmpty ldefs) $ \defs -> do + args :: [ConstructorArg] <- + concatMapM + (strongNormalize >=> mkConstructorArg) + ( defs + ^.. each + . inductiveConstructors + . each + . inductiveConstructorType + ) + poltab <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables + let occ :: Occurrences = mkOccurrences args + inferredPolarities = computePolarities poltab defs occ + forM_ defs $ \def -> do + let params :: [InductiveParam] = def ^.. inductiveParameters . each . inductiveParamName + getPol p = fromMaybe PolarityUnused (inferredPolarities ^. at p) + polarities :: [Polarity] = map getPol params + defName = def ^. inductiveName + addPolarities (defName ^. nameId) polarities + poltab' <- (^. typeCheckingTablesPolarityTable) <$> getCombinedTables + let names :: NonEmpty InductiveName = (^. inductiveName) <$> defs + unless noPositivityFlag $ do + let neg = checkStrictlyPositive poltab' names occ + markedPositive d = fromJust (find ((== d) . (^. inductiveName)) defs) ^. inductivePositive + whenJust (nonEmpty (filter (not . markedPositive) neg)) $ \negTys -> + throw $ + ErrNonStrictlyPositive + NonStrictlyPositive + { _nonStrictlyPositiveOccurrences = negTys + } + +-- NOTE we conservatively assume that axioms have all variables in negative positions +axiomPolarity :: Polarity +axiomPolarity = PolarityNonStrictlyPositive + +-- | Returns the list of non-strictly positive types +checkStrictlyPositive :: + PolarityTable -> + NonEmpty InductiveName -> + Occurrences -> + [InductiveName] +checkStrictlyPositive tbl mutual = + run + . execOutputList + . runReader PolarityStrictlyPositive + . go where - indInfo = p ^. checkPositivityArgsInductive - ctorName = p ^. checkPositivityArgsConstructorName - name = p ^. checkPositivityArgsInductiveName - recLimit = p ^. checkPositivityArgsRecursionLimit - ref = p ^. checkPositivityArgsErrorReference - - indName :: Name - indName = indInfo ^. inductiveInfoName - - {- The following `go` function determines if there is any negative - occurrence of the symbol `name` in the given expression. The `inside` flag - used below indicates whether the current search is performed on the left of - an inner arrow or not. - -} - goExpression :: Bool -> Expression -> Sem r () - goExpression inside expr = case expr of - ExpressionApplication tyApp -> goApp tyApp - ExpressionCase l -> goCase l - ExpressionFunction (Function l r) -> goLeft (l ^. paramType) >> go r - ExpressionHole {} -> return () - ExpressionInstanceHole {} -> return () - ExpressionIden i -> goIden i - ExpressionLambda l -> goLambda l - ExpressionLet l -> goLet l - ExpressionLiteral {} -> return () - ExpressionSimpleLambda l -> goSimpleLambda l - ExpressionUniverse {} -> return () + go :: forall r'. (Members '[Output InductiveName, Reader Polarity] r') => Occurrences -> Sem r' () + go occ = forM_ (HashMap.toList (occ ^. occurrences)) (uncurry goApp) + + mutualSet :: HashSet InductiveName + mutualSet = hashSet mutual + + isMutual :: InductiveName -> Bool + isMutual d = HashSet.member d mutualSet + + goArg :: + forall r'. + (Members '[Output InductiveName, Reader Polarity] r') => + Polarity -> + Occurrences -> + Sem r' () + goArg p occ = localPolarity p (go occ) + + goApp :: + forall r'. + (Members '[Output InductiveName, Reader Polarity] r') => + (FunctionSide, AppLhs) -> + [Occurrences] -> + Sem r' () + goApp (side, lhs) occ = local (functionSidePolarity side <>) $ case lhs of + AppVar {} -> local (const PolarityNonStrictlyPositive) (mapM_ go occ) + AppAxiom {} -> local (<> axiomPolarity) (mapM_ go occ) + AppInductive d -> do + ctx <- ask + let pols = getPolarities d + case ctx of + PolarityUnused -> impossible + PolarityStrictlyPositive -> return () + PolarityNonStrictlyPositive -> when (isMutual d) (output d) + mapM_ (uncurry goArg) (zip pols occ) where - go :: Expression -> Sem r () - go = goExpression inside - - goLeft :: Expression -> Sem r () - goLeft = goExpression True - - goCase :: Case -> Sem r () - goCase l = do - go (l ^. caseExpression) - mapM_ goCaseBranch (l ^. caseBranches) - - goSideIfBranch :: SideIfBranch -> Sem r () - goSideIfBranch b = do - go (b ^. sideIfBranchCondition) - go (b ^. sideIfBranchBody) - - goSideIfs :: SideIfs -> Sem r () - goSideIfs s = do - mapM_ goSideIfBranch (s ^. sideIfBranches) - mapM_ go (s ^. sideIfElse) - - goCaseBranchRhs :: CaseBranchRhs -> Sem r () - goCaseBranchRhs = \case - CaseBranchRhsExpression e -> go e - CaseBranchRhsIf s -> goSideIfs s - - goCaseBranch :: CaseBranch -> Sem r () - goCaseBranch b = goCaseBranchRhs (b ^. caseBranchRhs) - - goLet :: Let -> Sem r () - goLet l = do - go (l ^. letExpression) - mapM_ goLetClause (l ^. letClauses) - - goLetClause :: LetClause -> Sem r () - goLetClause = \case - LetFunDef f -> goFunctionDef f - LetMutualBlock b -> goMutualBlockLet b - - goMutualBlockLet :: MutualBlockLet -> Sem r () - goMutualBlockLet b = mapM_ goFunctionDef (b ^. mutualLet) - - goFunctionDef :: FunctionDef -> Sem r () - goFunctionDef d = do - go (d ^. funDefType) - go (d ^. funDefBody) - - goSimpleLambda :: SimpleLambda -> Sem r () - goSimpleLambda (SimpleLambda (SimpleBinder _ lamVarTy) lamBody) = do - go lamVarTy - go lamBody - - goLambda :: Lambda -> Sem r () - goLambda l = mapM_ goClause (l ^. lambdaClauses) + getPolarities :: InductiveName -> [Polarity] + getPolarities n = fromMaybe err (tbl ^. polarityTable . at (n ^. nameId)) where - goClause :: LambdaClause -> Sem r () - goClause (LambdaClause _ b) = go b - - goIden :: Iden -> Sem r () - goIden = \case - IdenInductive ty' -> - when (inside && name == ty') (throwNegativePositonError expr) - IdenVar name' - | not inside -> return () - | name == name' -> throwNegativePositonError expr - | name' `elem` indInfo ^.. inductiveInfoParameters . each . inductiveParamName -> modify (HashSet.insert name') - | otherwise -> return () - _ -> return () - - goApp :: Application -> Sem r () - goApp tyApp = do - let (hdExpr, args) = unfoldApplication tyApp - case hdExpr of - ax@(ExpressionIden IdenAxiom {}) -> do - when (isJust $ find (varOrInductiveInExpression name) args) $ - throwTypeAsArgumentOfBoundVarError ax - var@(ExpressionIden IdenVar {}) -> do - when (isJust $ find (varOrInductiveInExpression name) args) $ - throwTypeAsArgumentOfBoundVarError var - ExpressionIden (IdenInductive ty') -> do - when (inside && name == ty') (throwNegativePositonError expr) - indInfo' <- lookupInductive ty' - {- We now need to know whether `name` negatively occurs at - `indTy'` or not. The way to know is by checking that the type ty' - preserves the positivity condition, i.e., its type parameters are - no negative. - -} - let paramsTy' = indInfo' ^. inductiveInfoParameters - goInductiveApp indInfo' (zip paramsTy' (toList args)) - _ -> return () - - goInductiveApp :: InductiveInfo -> [(InductiveParameter, Expression)] -> Sem r () - goInductiveApp indInfo' = \case - [] -> return () - (InductiveParameter pName' _ty', tyArg) : ps -> do - negParms :: NegativeTypeParameters <- get - when (varOrInductiveInExpression name tyArg) $ do - when - (HashSet.member pName' negParms) - (throwNegativePositonError tyArg) - when (recLimit > 0) $ - forM_ (indInfo' ^. inductiveInfoConstructors) $ \ctorName' -> do - ctorType' <- lookupConstructorType ctorName' - let errorRef = fromMaybe tyArg ref - args = constructorArgs ctorType' - mapM_ - ( \tyConstr' -> - checkStrictlyPositiveOccurrences - CheckPositivityArgs - { _checkPositivityArgsInductive = indInfo', - _checkPositivityArgsConstructorName = ctorName', - _checkPositivityArgsInductiveName = pName', - _checkPositivityArgsRecursionLimit = recLimit - 1, - _checkPositivityArgsErrorReference = Just errorRef, - _checkPositivityArgsTypeOfConstructorArg = tyConstr' ^. paramType - } - ) - args - goInductiveApp indInfo' ps - - throwNegativePositonError :: Expression -> Sem r () - throwNegativePositonError expr = do - let errLoc = fromMaybe expr ref - throw - . ErrNonStrictlyPositive - . ErrTypeInNegativePosition - $ TypeInNegativePosition - { _typeInNegativePositionType = indName, - _typeInNegativePositionConstructor = ctorName, - _typeInNegativePositionArgument = errLoc - } - - throwTypeAsArgumentOfBoundVarError :: Expression -> Sem r () - throwTypeAsArgumentOfBoundVarError expr = do - let errLoc = fromMaybe expr ref - throw - . ErrNonStrictlyPositive - . ErrTypeAsArgumentOfBoundVar - $ TypeAsArgumentOfBoundVar - { _typeAsArgumentOfBoundVarType = indName, - _typeAsArgumentOfBoundVarConstructor = ctorName, - _typeAsArgumentOfBoundVarReference = errLoc - } - -varOrInductiveInExpression :: Name -> Expression -> Bool -varOrInductiveInExpression n = \case - ExpressionIden (IdenVar var) -> n == var - ExpressionIden (IdenInductive ty) -> n == ty - ExpressionApplication (Application l r _) -> - varOrInductiveInExpression n l || varOrInductiveInExpression n r - ExpressionFunction (Function l r) -> - varOrInductiveInExpression n (l ^. paramType) - || varOrInductiveInExpression n r - _ -> False + err :: a + err = impossibleError ("Didn't find polarities for inductive " <> ppTrace n) + +localPolarity :: (Members '[Reader Polarity] r) => Polarity -> Sem r () -> Sem r () +localPolarity p = case p of + PolarityUnused -> const (return ()) + PolarityNonStrictlyPositive -> local (p <>) + PolarityStrictlyPositive -> local (p <>) + +computePolarities :: + PolarityTable -> + NonEmpty InductiveDef -> + Occurrences -> + HashMap InductiveParam Polarity +computePolarities tab defs topOccurrences = + (^. builderPolarities) + . run + . runReader PolarityStrictlyPositive + . execState emptyBuilder + $ go topOccurrences + where + defsByName :: HashMap InductiveName InductiveDef + defsByName = indexedByHash (^. inductiveName) defs + + getDef :: InductiveName -> InductiveDef + getDef d = fromJust (defsByName ^. at d) + + -- Gets the current polarities of an inductive definition in the current mutual block + getInductivePolarities :: + (Members '[State Builder] r) => + InductiveName -> + Sem r [(InductiveParam, Maybe Polarity)] + getInductivePolarities d = do + b <- get + let params = getDef d ^. inductiveParameters + return + [ (name, b ^. builderPolarities . at name) + | p :: InductiveParameter <- params, + let name = p ^. inductiveParamName + ] + + go :: forall r. (Members '[State Builder, Reader Polarity] r) => Occurrences -> Sem r () + go o = do + sequence_ + [ addPolarity param (functionSidePolarity side) + | ((side, AppVar param), _) <- HashMap.toList (o ^. occurrences) + ] + forM_ (HashMap.toList (o ^. occurrences)) (uncurry goApp) + where + addPolarity :: InductiveParam -> Polarity -> Sem r () + addPolarity var p = do + newPol <- (p <>) <$> ask + modify (over (builderPolarities . at var) (Just . maybe newPol (newPol <>))) + unblock var newPol + + unblock :: forall r. (Members '[State Builder] r) => InductiveParam -> Polarity -> Sem r () + unblock p newPol = unblockGo + where + unblockGo :: Sem r () + unblockGo = do + b <- gets (^. builderBlocking) + whenJust (findAndRemove isTriggered b) $ \(triggered, rest) -> do + modify (set builderBlocking (maybeToList (increaseMinimum triggered) ++ rest)) + runBlocking triggered + unblockGo + + increaseMinimum :: Blocking -> Maybe Blocking + increaseMinimum = case newPol of + PolarityNonStrictlyPositive -> const Nothing + PolarityStrictlyPositive -> Just . set blockingUnblockerMinimum PolarityNonStrictlyPositive + PolarityUnused -> impossible + + isTriggered :: Blocking -> Bool + isTriggered b = (b ^. blockingUnblockerMinimum <= newPol) && (b ^. blockingUnblocker == p) + + runBlocking :: Blocking -> Sem r () + runBlocking b = runReader (b ^. blockingContext) (go (b ^. blockingOccurrences)) + + goApp :: + forall r. + (Members '[State Builder, Reader Polarity] r) => + (FunctionSide, AppLhs) -> + [Occurrences] -> + Sem r () + goApp (side, lhs) os = local (functionSidePolarity side <>) $ case lhs of + AppVar {} -> goVarArgs os + AppAxiom {} -> goAxiomArgs os + AppInductive a -> goInductive a os + + goAxiomArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () + goAxiomArgs os = local (<> axiomPolarity) (mapM_ go os) + + goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () + goVarArgs os = local (const PolarityNonStrictlyPositive) (mapM_ go os) + + block :: + (Members '[State Builder, Reader Polarity] r) => + Polarity -> + InductiveParam -> + Occurrences -> + Sem r () + block minPol param o = do + ctx <- ask + let b = + Blocking + { _blockingContext = ctx, + _blockingUnblocker = param, + _blockingOccurrences = o, + _blockingUnblockerMinimum = minPol + } + modify (over builderBlocking (b :)) + + goInductive :: + (Members '[State Builder, Reader Polarity] r) => + InductiveName -> + [Occurrences] -> + Sem r () + goInductive d os = do + case tab ^. polarityTable . at (d ^. nameId) of + Just (pols :: [Polarity]) -> + forM_ (zip pols os) $ \(pol :: Polarity, o :: Occurrences) -> do + localPolarity pol (go o) + Nothing -> do + pols :: [(InductiveParam, Maybe Polarity)] <- getInductivePolarities d + forM_ (zip pols os) $ \((p :: InductiveParam, mpol :: Maybe Polarity), o :: Occurrences) -> + case mpol of + Nothing -> block PolarityStrictlyPositive p o + Just pol -> case pol of + PolarityUnused -> impossible + PolarityStrictlyPositive -> do + block PolarityNonStrictlyPositive p o + localPolarity PolarityStrictlyPositive (go o) + PolarityNonStrictlyPositive -> localPolarity PolarityNonStrictlyPositive (go o) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs new file mode 100644 index 0000000000..fb37227581 --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs @@ -0,0 +1,67 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg + ( mkConstructorArg, + module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base, + ) +where + +import Juvix.Compiler.Internal.Extra.Base +import Juvix.Compiler.Internal.Language +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error +import Juvix.Prelude + +mkConstructorArg :: (Members '[Error TypeCheckerError] r) => NormalizedExpression -> Sem r [ConstructorArg] +mkConstructorArg = mapM (goArg . (^. paramType)) . fst . unfoldFunType . (^. normalizedExpression) + +goArg :: forall r. (Members '[Error TypeCheckerError] r) => Expression -> Sem r ConstructorArg +goArg ty = case ty of + ExpressionIden i -> goApplicationHelper (ExpressionIden i, []) + ExpressionApplication i -> goApplication i + ExpressionUniverse {} -> return ConstructorArgType + ExpressionFunction i -> goFunction i + ExpressionLiteral {} -> invalid + ExpressionHole {} -> invalid + ExpressionInstanceHole {} -> invalid + ExpressionLet {} -> invalid + ExpressionSimpleLambda {} -> invalid + ExpressionLambda {} -> invalid + ExpressionCase {} -> invalid + where + invalid :: forall a. Sem r a + invalid = + throw $ + ErrInvalidConstructorArgType + InvalidConstructorArgType + { _invalidConstructorArgType = ty + } + + getIden :: Expression -> Sem r Iden + getIden = \case + ExpressionIden i -> return i + _ -> invalid + + goFunction :: Function -> Sem r ConstructorArg + goFunction fun = do + l <- goArg (fun ^. functionLeft . paramType) + r <- goArg (fun ^. functionRight) + return $ + ConstructorArgFun + Fun + { _funLeft = l, + _funRight = r + } + + goApplication :: Application -> Sem r ConstructorArg + goApplication = goApplicationHelper . second toList . unfoldApplication + + goApplicationHelper :: (Expression, [Expression]) -> Sem r ConstructorArg + goApplicationHelper (f, args) = do + i <- getIden f + cargs <- mapM goArg args + lhs :: AppLhs <- case i of + IdenFunction {} -> invalid + IdenConstructor {} -> invalid + IdenVar v -> return (AppVar v) + IdenAxiom v -> return (AppAxiom v) + IdenInductive v -> return (AppInductive v) + return (ConstructorArgApp (App lhs cargs)) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs new file mode 100644 index 0000000000..08aa4b093e --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs @@ -0,0 +1,27 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base where + +import Juvix.Compiler.Internal.Language +import Juvix.Prelude + +data ConstructorArg + = ConstructorArgFun Fun + | ConstructorArgApp App + | ConstructorArgType + +data Fun = Fun + { _funLeft :: ConstructorArg, + _funRight :: ConstructorArg + } + +data AppLhs + = AppVar VarName + | AppAxiom AxiomName + | AppInductive InductiveName + deriving stock (Eq, Show, Generic) + +instance Hashable AppLhs + +data App = App + { _appLhs :: AppLhs, + _appArgs :: [ConstructorArg] + } diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs deleted file mode 100644 index 64d00e1f16..0000000000 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Error.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types, - ) -where - -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error.Types -import Juvix.Prelude - -data NonStrictlyPositiveError - = ErrTypeInNegativePosition TypeInNegativePosition - | ErrTypeAsArgumentOfBoundVar TypeAsArgumentOfBoundVar - -instance ToGenericError NonStrictlyPositiveError where - genericError :: (Member (Reader GenericOptions) r) => NonStrictlyPositiveError -> Sem r GenericError - genericError = \case - ErrTypeInNegativePosition e -> genericError e - ErrTypeAsArgumentOfBoundVar e -> genericError e diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs new file mode 100644 index 0000000000..b8bd3d8ea8 --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs @@ -0,0 +1,87 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences + ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base, + Occurrences (..), + FunctionSide (..), + mkOccurrences, + occurrences, + ) +where + +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base +import Juvix.Prelude +import Juvix.Prelude.Pretty + +data FunctionSide + = FunctionLeft + | FunctionRight + deriving stock (Show, Eq, Generic) + +instance Pretty FunctionSide where + pretty = \case + FunctionLeft -> "left" + FunctionRight -> "right" + +instance Hashable FunctionSide + +instance Semigroup FunctionSide where + a <> b = case (a, b) of + (FunctionLeft, _) -> FunctionLeft + (_, FunctionLeft) -> FunctionLeft + (FunctionRight, FunctionRight) -> FunctionRight + +instance Monoid FunctionSide where + mempty = FunctionRight + +newtype Occurrences = Occurrences + { _occurrences :: HashMap (FunctionSide, AppLhs) [Occurrences] + } + deriving stock (Show) + +makeLenses ''Occurrences + +emptyOccurrences :: Occurrences +emptyOccurrences = + Occurrences + { _occurrences = mempty + } + +mkOccurrences :: [ConstructorArg] -> Occurrences +mkOccurrences = + run + . runReader FunctionRight + . execState emptyOccurrences + . mapM_ addArg + where + addArg :: forall r'. (Members '[Reader FunctionSide, State Occurrences] r') => ConstructorArg -> Sem r' () + addArg = \case + ConstructorArgFun fun -> goFun fun + ConstructorArgApp a -> goApp a + ConstructorArgType -> return () + where + goApp :: App -> Sem r' () + goApp (App lhs args) = case lhs of + AppVar {} -> goArgs (<> FunctionLeft) + AppAxiom {} -> goArgs id + AppInductive {} -> goArgs id + where + goArgs :: (FunctionSide -> FunctionSide) -> Sem r' () + goArgs recurModif = do + side <- ask + let numArgs = length args + iniOccs = replicate numArgs emptyOccurrences + k = (side, lhs) + occs :: [Occurrences] <- fromMaybe iniOccs <$> gets (^. occurrences . at k) + st :: Occurrences <- get + occs' :: [Occurrences] <- local recurModif . for (zipExact occs args) $ \(occ, arg) -> do + put occ + addArg arg + get + put (set (occurrences . at k) (Just occs') st) + + goFun :: Fun -> Sem r' () + goFun (Fun funl funr) = do + onSide FunctionLeft (addArg funl) + onSide FunctionRight (addArg funr) + where + onSide :: FunctionSide -> Sem r' () -> Sem r' () + onSide side = local (side <>) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs index 987471e72b..1989a3c98e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -131,7 +131,7 @@ checkCoercionCycles :: (Members '[ResultBuilder, Error TypeCheckerError] r) => Sem r () checkCoercionCycles = do - ctab <- getCombinedCoercionTable + ctab <- (^. typeCheckingTablesCoercionTable) <$> getCombinedTables let s = toList $ cyclicCoercions ctab whenJust (nonEmpty s) $ throw @@ -151,10 +151,7 @@ checkModule :: Module -> Sem r Module checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do - _moduleBody' <- - evalState (mempty :: NegativeTypeParameters) - . checkModuleBody - $ _moduleBody + _moduleBody' <- checkModuleBody _moduleBody return Module { _moduleBody = _moduleBody', @@ -164,7 +161,7 @@ checkModule Module {..} = runReader (mempty @InsertedArgsStack) $ do } checkModuleBody :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => ModuleBody -> Sem r ModuleBody checkModuleBody ModuleBody {..} = do @@ -180,14 +177,14 @@ checkImport :: Import -> Sem r Import checkImport = return checkMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkMutualBlock s = runReader emptyLocalVars (checkTopMutualBlock s) checkInductiveDef :: forall r. - (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, State NegativeTypeParameters, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Termination, Output TypedHole, Output CastHole, Reader InsertedArgsStack, Reader LocalVars] r) => InductiveDef -> Sem r InductiveDef checkInductiveDef InductiveDef {..} = runInferenceDef $ do @@ -209,7 +206,6 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do _inductivePragmas, _inductiveDocComment } - checkPositivity (inductiveInfoFromInductiveDef d) return d where checkParams :: Sem (Inference ': r) [(Name, Expression)] @@ -249,11 +245,33 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do ) checkTopMutualBlock :: - (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock checkTopMutualBlock (MutualBlock ds) = - MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds) + MutualBlock + <$> runInferenceDefs + ( do + ls <- mapM checkMutualStatement ds + checkBlockPositivity (MutualBlock ls) + return ls + ) + +checkBlockPositivity :: + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + ResultBuilder, + Reader EntryPoint, + Inference + ] + r + ) => + MutualBlock -> + Sem r () +checkBlockPositivity m = do + noPos <- asks (^. entryPointNoPositivity) + checkPositivity noPos m resolveCastHoles :: forall a r. @@ -286,7 +304,7 @@ resolveCastHoles s = do getNatTy = mkBuiltinInductive BuiltinNat checkMutualStatement :: - (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => + (Members '[HighlightBuilder, Reader BuiltinsTable, Reader EntryPoint, Inference, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualStatement -> Sem r MutualStatement checkMutualStatement = \case @@ -395,7 +413,7 @@ checkInstanceType FunctionDef {..} = do tab <- ask unless (isTrait tab _instanceInfoInductive) $ throw (ErrTargetNotATrait (TargetNotATrait _funDefType)) - itab <- getCombinedInstanceTable + itab <- (^. typeCheckingTablesInstanceTable) <$> getCombinedTables is <- subsumingInstances itab ii unless (null is) $ throw (ErrSubsumedInstance (SubsumedInstance ii is (getLoc _funDefName))) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs index b9b61a98ed..175852f6ea 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs @@ -622,6 +622,7 @@ strongNormalize'' ty = do { _typeCheckingTablesCoercionTable = mempty, _typeCheckingTablesInstanceTable = mempty, _typeCheckingTablesTypesTable = mempty, + _typeCheckingTablesPolarityTable = mempty, _typeCheckingTablesFunctionsTable = ftab } } diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs index ea35c7a3a6..e4f5fc730e 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/ResultBuilder.hs @@ -13,10 +13,10 @@ data ResultBuilder :: Effect where AddIdenTypes :: TypesTable -> ResultBuilder m () AddInstanceInfo :: InstanceInfo -> ResultBuilder m () AddCoercionInfo :: CoercionInfo -> ResultBuilder m () + AddPolarities :: InductiveId -> [Polarity] -> ResultBuilder m () LookupFunctionDef :: FunctionName -> ResultBuilder m (Maybe Expression) LookupIdenType :: NameId -> ResultBuilder m (Maybe Expression) - GetCombinedInstanceTable :: ResultBuilder m InstanceTable - GetCombinedCoercionTable :: ResultBuilder m CoercionTable + GetCombinedTables :: ResultBuilder m TypeCheckingTables makeSem ''ResultBuilder @@ -42,6 +42,8 @@ runResultBuilder' :: Sem (ResultBuilder ': r) a -> Sem r (ResultBuilderState, a) runResultBuilder' inis = reinterpret (runState inis) $ \case + AddPolarities name pol -> + overBothTables (set (typeCheckingTablesPolarityTable . polarityTable . at name) (Just pol)) AddFunctionDef name def -> overBothTables (set (typeCheckingTablesFunctionsTable . functionsTable . at name) (Just def)) AddIdenType nid ty -> @@ -56,10 +58,8 @@ runResultBuilder' inis = reinterpret (runState inis) $ \case gets (^. resultBuilderStateCombinedTables . typeCheckingTablesFunctionsTable . functionsTable . at name) LookupIdenType nid -> gets (^. resultBuilderStateCombinedTables . typeCheckingTablesTypesTable . typesTable . at nid) - GetCombinedInstanceTable -> - gets (^. resultBuilderStateCombinedTables . typeCheckingTablesInstanceTable) - GetCombinedCoercionTable -> - gets (^. resultBuilderStateCombinedTables . typeCheckingTablesCoercionTable) + GetCombinedTables -> + gets (^. resultBuilderStateCombinedTables) where overBothTables :: (Members '[State ResultBuilderState] r') => (TypeCheckingTables -> TypeCheckingTables) -> Sem r' () overBothTables f = modify $ \res -> @@ -70,12 +70,12 @@ runResultBuilder' inis = reinterpret (runState inis) $ \case lookupInstanceInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [InstanceInfo]) lookupInstanceInfo name = do - tab <- getCombinedInstanceTable + tab <- (^. typeCheckingTablesInstanceTable) <$> getCombinedTables return $ lookupInstanceTable tab name lookupCoercionInfo :: (Members '[ResultBuilder] r) => Name -> Sem r (Maybe [CoercionInfo]) lookupCoercionInfo name = do - tab <- getCombinedCoercionTable + tab <- (^. typeCheckingTablesCoercionTable) <$> getCombinedTables return $ lookupCoercionTable tab name runResultBuilder :: ImportContext -> Sem (ResultBuilder ': r) a -> Sem r (ResultBuilderState, a) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs index 2f38e57bc3..8ead6846c4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -8,7 +8,6 @@ where import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Types (BuiltinNotDefined) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error.Types import Juvix.Prelude @@ -23,7 +22,7 @@ data TypeCheckerError | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType | ErrInvalidPatternMatching InvalidPatternMatching - | ErrNonStrictlyPositive NonStrictlyPositiveError + | ErrNonStrictlyPositive NonStrictlyPositive | ErrUnsupportedTypeFunction UnsupportedTypeFunction | ErrInvalidInstanceType InvalidInstanceType | ErrInvalidCoercionType InvalidCoercionType @@ -40,6 +39,7 @@ data TypeCheckerError | ErrArityCheckerError ArityCheckerError | ErrDefaultArgLoop DefaultArgLoop | ErrBadScope BadScope + | ErrInvalidConstructorArgType InvalidConstructorArgType instance ToGenericError TypeCheckerError where genericError :: (Member (Reader GenericOptions) r) => TypeCheckerError -> Sem r GenericError @@ -52,7 +52,6 @@ instance ToGenericError TypeCheckerError where ErrTooManyArgumentsIndType e -> genericError e ErrTooFewArgumentsIndType e -> genericError e ErrInvalidPatternMatching e -> genericError e - ErrNonStrictlyPositive e -> genericError e ErrUnsupportedTypeFunction e -> genericError e ErrInvalidInstanceType e -> genericError e ErrInvalidCoercionType e -> genericError e @@ -69,6 +68,8 @@ instance ToGenericError TypeCheckerError where ErrArityCheckerError e -> genericError e ErrDefaultArgLoop e -> genericError e ErrBadScope e -> genericError e + ErrInvalidConstructorArgType e -> genericError e + ErrNonStrictlyPositive e -> genericError e instance Show TypeCheckerError where show = \case @@ -81,7 +82,6 @@ instance Show TypeCheckerError where ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType" ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching" ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction" - ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive" ErrInvalidInstanceType {} -> "ErrInvalidInstanceType" ErrInvalidCoercionType {} -> "ErrInvalidCoercionType" ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument" @@ -97,3 +97,5 @@ instance Show TypeCheckerError where ErrDefaultArgLoop {} -> "ErrDefaultArgLoop" ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined" ErrBadScope {} -> "ErrBadScope" + ErrInvalidConstructorArgType {} -> "ErrInvalidConstructorArgType" + ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive" diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs index 30156e4141..e42e6835c8 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs @@ -665,3 +665,67 @@ instance ToGenericError BadScope where <> "As a workaround, explicitly provide a type in the place where you think the variable got inserted." <> line <> "More information at https://github.com/anoma/juvix/issues/2247" + +newtype InvalidConstructorArgType = InvalidConstructorArgType + { _invalidConstructorArgType :: Expression + } + +makeLenses ''InvalidConstructorArgType + +instance ToGenericError InvalidConstructorArgType where + genericError e = ask >>= generr + where + generr opts = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = [i] + } + where + opts' = fromGenericOptions opts + ty = e ^. invalidConstructorArgType + i = getLoc ty + msg :: Doc Ann = + "The type of this constructor argument is not valid:" + <> line + <> ppCode opts' ty + +newtype NonStrictlyPositive = NonStrictlyPositive + { -- This list contains occurrences of the inductive types in non-strictly + -- positive positions. Thus it may contain repeated names + _nonStrictlyPositiveOccurrences :: NonEmpty InductiveName + } + +makeLenses ''NonStrictlyPositive + +instance ToGenericError NonStrictlyPositive where + genericError e = ask >>= generr + where + generr opts = + return + GenericError + { _genericErrorLoc = i, + _genericErrorMessage = ppOutput msg, + _genericErrorIntervals = map getLoc (toList occs) + } + where + opts' = fromGenericOptions opts + occs :: NonEmpty InductiveName = e ^. nonStrictlyPositiveOccurrences + tys = nubHashableNonEmpty occs + i = getLoc (tys ^. _head1) + msg :: Doc Ann = + "The positivity checker failed because the inductive" + <+> ( case tys of + d :| [] -> "type" <+> ppCode opts' d <+> "is" + _ -> "types" <> line <> itemize (ppCode opts' <$> tys) <> line <> "are" + ) + <+> "not strictly positive." + <> line + <> line + <> "A type D is strictly positive iff two conditions hold:" + <> line + <> itemize + [ "D does not appear applied to a bound variable", + "D does not appear on the left of an arrow in any argument type of its constructors" + ] diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs index bb7c1a1517..4260821ee6 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Traits/Resolver.hs @@ -34,10 +34,11 @@ resolveTraitInstance :: resolveTraitInstance TypedHole {..} = do vars <- overM localTypes (mapM strongNormalize_) _typedHoleLocalVars infoTab <- ask - tab0 <- getCombinedInstanceTable - let tab = foldr (flip updateInstanceTable) tab0 (varsToInstances infoTab vars) + combtabs <- getCombinedTables + let tab0 = combtabs ^. typeCheckingTablesInstanceTable + tab = foldr (flip updateInstanceTable) tab0 (varsToInstances infoTab vars) + ctab = combtabs ^. typeCheckingTablesCoercionTable ty <- strongNormalize _typedHoleType - ctab <- getCombinedCoercionTable is <- lookupInstance ctab tab (ty ^. normalizedExpression) case is of [(cs, ii, subs)] -> diff --git a/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs new file mode 100644 index 0000000000..450809a4a5 --- /dev/null +++ b/src/Juvix/Compiler/Store/Internal/Data/PolarityTable.hs @@ -0,0 +1,18 @@ +module Juvix.Compiler.Store.Internal.Data.PolarityTable where + +import Juvix.Compiler.Internal.Language +import Juvix.Extra.Serialize +import Juvix.Prelude + +newtype PolarityTable = PolarityTable + { -- | The value should have the same length as the length of _inductiveParameters + _polarityTable :: HashMap InductiveId [Polarity] + } + deriving newtype (Semigroup, Monoid) + deriving stock (Generic) + +instance Serialize PolarityTable + +instance NFData PolarityTable + +makeLenses ''PolarityTable diff --git a/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs b/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs index 010d95ac70..d9fef9ae63 100644 --- a/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs +++ b/src/Juvix/Compiler/Store/Internal/Data/TypeCheckingTables.hs @@ -3,6 +3,7 @@ module Juvix.Compiler.Store.Internal.Data.TypeCheckingTables module Juvix.Compiler.Store.Internal.Data.CoercionInfo, module Juvix.Compiler.Store.Internal.Data.FunctionsTable, module Juvix.Compiler.Store.Internal.Data.InstanceInfo, + module Juvix.Compiler.Store.Internal.Data.PolarityTable, module Juvix.Compiler.Store.Internal.Data.TypesTable, ) where @@ -10,6 +11,7 @@ where import Juvix.Compiler.Store.Internal.Data.CoercionInfo import Juvix.Compiler.Store.Internal.Data.FunctionsTable import Juvix.Compiler.Store.Internal.Data.InstanceInfo +import Juvix.Compiler.Store.Internal.Data.PolarityTable import Juvix.Compiler.Store.Internal.Data.TypesTable import Juvix.Extra.Serialize import Juvix.Prelude @@ -17,6 +19,7 @@ import Juvix.Prelude data TypeCheckingTables = TypeCheckingTables { _typeCheckingTablesTypesTable :: TypesTable, _typeCheckingTablesFunctionsTable :: FunctionsTable, + _typeCheckingTablesPolarityTable :: PolarityTable, _typeCheckingTablesInstanceTable :: InstanceTable, _typeCheckingTablesCoercionTable :: CoercionTable } @@ -34,6 +37,7 @@ instance Monoid TypeCheckingTables where { _typeCheckingTablesTypesTable = mempty, _typeCheckingTablesFunctionsTable = mempty, _typeCheckingTablesInstanceTable = mempty, + _typeCheckingTablesPolarityTable = mempty, _typeCheckingTablesCoercionTable = mempty } @@ -42,6 +46,7 @@ instance Semigroup TypeCheckingTables where TypeCheckingTables { _typeCheckingTablesTypesTable = mappendField' typeCheckingTablesTypesTable, _typeCheckingTablesFunctionsTable = mappendField' typeCheckingTablesFunctionsTable, + _typeCheckingTablesPolarityTable = mappendField' typeCheckingTablesPolarityTable, _typeCheckingTablesInstanceTable = mappendField' typeCheckingTablesInstanceTable, _typeCheckingTablesCoercionTable = mappendField' typeCheckingTablesCoercionTable } diff --git a/src/Juvix/Compiler/Store/Internal/Language.hs b/src/Juvix/Compiler/Store/Internal/Language.hs index 1c9e5ff204..3a0b407b1b 100644 --- a/src/Juvix/Compiler/Store/Internal/Language.hs +++ b/src/Juvix/Compiler/Store/Internal/Language.hs @@ -53,23 +53,13 @@ computeCombinedInfoTable = mconcatMap (^. internalModuleInfoTable) . HashMap.ele computeTypeCheckingTables :: InternalModuleTable -> TypeCheckingTables computeTypeCheckingTables itab = TypeCheckingTables - { _typeCheckingTablesTypesTable = computeTypesTable, - _typeCheckingTablesInstanceTable = computeInstanceTable, - _typeCheckingTablesFunctionsTable = computeFunctionsTable, - _typeCheckingTablesCoercionTable = computeCoercionTable + { _typeCheckingTablesTypesTable = computeTable typeCheckingTablesTypesTable, + _typeCheckingTablesInstanceTable = computeTable typeCheckingTablesInstanceTable, + _typeCheckingTablesFunctionsTable = computeTable typeCheckingTablesFunctionsTable, + _typeCheckingTablesPolarityTable = computeTable typeCheckingTablesPolarityTable, + _typeCheckingTablesCoercionTable = computeTable typeCheckingTablesCoercionTable } where - computeTypesTable :: TypesTable - computeTypesTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesTypesTable) (itab ^. internalModuleTable) - - computeFunctionsTable :: FunctionsTable - computeFunctionsTable = - mconcatMap - (^. internalModuleTypeCheckingTables . typeCheckingTablesFunctionsTable) - (itab ^. internalModuleTable) - - computeInstanceTable :: InstanceTable - computeInstanceTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesInstanceTable) (itab ^. internalModuleTable) - - computeCoercionTable :: CoercionTable - computeCoercionTable = mconcatMap (^. internalModuleTypeCheckingTables . typeCheckingTablesCoercionTable) (itab ^. internalModuleTable) + computeTable :: (Monoid tbl) => Lens' TypeCheckingTables tbl -> tbl + computeTable l = + mconcatMap (^. internalModuleTypeCheckingTables . l) (itab ^. internalModuleTable) diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs index 80d71a58cc..dad143f1c7 100644 --- a/src/Juvix/Data.hs +++ b/src/Juvix/Data.hs @@ -23,6 +23,7 @@ module Juvix.Data module Juvix.Data.DependencyInfo, module Juvix.Data.TopModulePathKey, module Juvix.Data.Keyword, + module Juvix.Data.Polarity, ) where @@ -41,6 +42,7 @@ import Juvix.Data.Loc import Juvix.Data.Logger import Juvix.Data.NameId qualified import Juvix.Data.NumThreads +import Juvix.Data.Polarity import Juvix.Data.Pragmas import Juvix.Data.Processed import Juvix.Data.ProjectionKind diff --git a/src/Juvix/Data/Polarity.hs b/src/Juvix/Data/Polarity.hs new file mode 100644 index 0000000000..ca68cc61e7 --- /dev/null +++ b/src/Juvix/Data/Polarity.hs @@ -0,0 +1,30 @@ +module Juvix.Data.Polarity where + +import Juvix.Extra.Serialize +import Juvix.Prelude.Base +import Juvix.Prelude.Pretty + +-- | NOTE that Order of constructors is relevant for the derived instances +data Polarity + = PolarityUnused + | PolarityStrictlyPositive + | PolarityNonStrictlyPositive + deriving stock (Ord, Enum, Bounded, Eq, Generic, Data, Show) + +instance Hashable Polarity + +instance Serialize Polarity + +instance NFData Polarity + +instance Semigroup Polarity where + a <> b = max a b + +instance Monoid Polarity where + mempty = PolarityUnused + +instance Pretty Polarity where + pretty = \case + PolarityNonStrictlyPositive -> "non-strictly-positive" + PolarityStrictlyPositive -> "strictly-positive" + PolarityUnused -> "unused" diff --git a/src/Juvix/Prelude/Base/Foundation.hs b/src/Juvix/Prelude/Base/Foundation.hs index 23dc232e1e..bb84182627 100644 --- a/src/Juvix/Prelude/Base/Foundation.hs +++ b/src/Juvix/Prelude/Base/Foundation.hs @@ -447,6 +447,20 @@ zip4Exact [] [] [] [] = [] zip4Exact (x1 : t1) (x2 : t2) (x3 : t3) (x4 : t4) = (x1, x2, x3, x4) : zip4Exact t1 t2 t3 t4 zip4Exact _ _ _ _ = error "zip4Exact" +-- | Returns the first element that returns Just and the list with the remaining elements +findJustAndRemove :: forall a b. (a -> Maybe b) -> [a] -> Maybe (b, [a]) +findJustAndRemove p = go [] + where + go :: [a] -> [a] -> Maybe (b, [a]) + go acc = \case + [] -> Nothing + x : xs -> case p x of + Just b -> Just (b, reverse acc ++ xs) + Nothing -> go (x : acc) xs + +findAndRemove :: (a -> Bool) -> [a] -> Maybe (a, [a]) +findAndRemove p = findJustAndRemove (\a -> guard (p a) $> a) + -------------------------------------------------------------------------------- -- NonEmpty -------------------------------------------------------------------------------- @@ -598,6 +612,9 @@ massert b = assert b (pure ()) iterateN :: Int -> (a -> a) -> a -> a iterateN n f = (!! n) . iterate f +nubHashableNonEmpty :: (Hashable a) => NonEmpty a -> NonEmpty a +nubHashableNonEmpty = nonEmpty' . HashSet.toList . HashSet.fromList . toList + nubHashable :: (Hashable a) => [a] -> [a] nubHashable = HashSet.toList . HashSet.fromList diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 9c957268ba..b4557189d0 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -1,7 +1,6 @@ module Typecheck.Negative where import Base -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error type FailMsg = String @@ -268,48 +267,22 @@ tests = negPositivityTests :: [NegTest] negPositivityTests = - [ negTest "E1" $(mkRelDir "Internal/Positivity") $(mkRelFile "E1.juvix") $ - \case - ErrNonStrictlyPositive ErrTypeInNegativePosition {} -> Nothing - _ -> wrongError, - negTest "E2" $(mkRelDir "Internal/Positivity") $(mkRelFile "E2.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E3" $(mkRelDir "Internal/Positivity") $(mkRelFile "E3.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E4" $(mkRelDir "Internal/Positivity") $(mkRelFile "E4.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E5" $(mkRelDir "Internal/Positivity") $(mkRelFile "E5.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E6" $(mkRelDir "Internal/Positivity") $(mkRelFile "E6.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E7" $(mkRelDir "Internal/Positivity") $(mkRelFile "E7.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E8" $(mkRelDir "Internal/Positivity") $(mkRelFile "E8.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E9" $(mkRelDir "Internal/Positivity") $(mkRelFile "E9.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E10 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E10.juvix") $ - \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing - _ -> wrongError, - negTest "E11 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E11.juvix") $ + [ mk "E1" $(mkRelFile "E1.juvix"), + mk "E2" $(mkRelFile "E2.juvix"), + mk "E3" $(mkRelFile "E3.juvix"), + mk "E4" $(mkRelFile "E4.juvix"), + mk "E5" $(mkRelFile "E5.juvix"), + mk "E6" $(mkRelFile "E6.juvix"), + mk "E7" $(mkRelFile "E7.juvix"), + mk "E8" $(mkRelFile "E8.juvix"), + mk "E9" $(mkRelFile "E9.juvix"), + mk "E10 uses type synonym" $(mkRelFile "E10.juvix"), + mk "E11 uses type synonym" $(mkRelFile "E11.juvix"), + mk "Box left hand side" $(mkRelFile "box.juvix") + ] + where + mk :: String -> Path Rel File -> NegTest + mk testname testfile = negTest testname $(mkRelDir "Internal/Positivity") testfile $ \case - ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing + ErrNonStrictlyPositive NonStrictlyPositive {} -> Nothing _ -> wrongError - ] diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 3fcfb9a8a0..c705bd5ab9 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -2,7 +2,6 @@ module Typecheck.NegativeNew where import Base import Data.HashSet qualified as HashSet -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Error import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Error import Typecheck.Negative qualified as Old @@ -149,14 +148,14 @@ arityTests = _ -> wrongError, negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $ \case - ErrNonStrictlyPositive ErrTypeAsArgumentOfBoundVar {} -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError, negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError, negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $ \case - ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError ] diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 55928a82c8..459f51f881 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -57,12 +57,21 @@ testNoPositivityFlag N.NegTest {..} = negPositivityTests :: [N.NegTest] negPositivityTests = N.negPositivityTests +-- | Positive tests for the positivity checker testWellDefinedInductiveDefs :: [PosTest] testWellDefinedInductiveDefs = [ posTest "Rose tree definition is well-defined" $(mkRelDir "Internal/Positivity") - $(mkRelFile "RoseTree.juvix") + $(mkRelFile "RoseTree.juvix"), + posTest + "Mutually recursive types and phantom types" + $(mkRelDir "Internal/Positivity2") + $(mkRelFile "main.juvix"), + posTest + "Issue 3048" + $(mkRelDir "issue3048") + $(mkRelFile "main.juvix") ] testPositivityKeyword :: [PosTest] diff --git a/tests/Compilation/positive/test079.juvix b/tests/Compilation/positive/test079.juvix index 0c09c285da..0520475b28 100644 --- a/tests/Compilation/positive/test079.juvix +++ b/tests/Compilation/positive/test079.juvix @@ -7,10 +7,10 @@ type Nat := | zero | suc Nat; -type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B}; - type Box := mkBox {unbox : Nat}; +type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B}; + one : Nat := zero; open Foldable public; diff --git a/tests/negative/Internal/Positivity/box.juvix b/tests/negative/Internal/Positivity/box.juvix new file mode 100644 index 0000000000..d1085aed02 --- /dev/null +++ b/tests/negative/Internal/Positivity/box.juvix @@ -0,0 +1,5 @@ +module box; + +type Box (A : Type) := mkBox A; + +type P (A : Type) := mkP : (Box (P A) -> P A) -> P A; diff --git a/tests/positive/Internal/Positivity2/Package.juvix b/tests/positive/Internal/Positivity2/Package.juvix new file mode 100644 index 0000000000..dc768cdde3 --- /dev/null +++ b/tests/positive/Internal/Positivity2/Package.juvix @@ -0,0 +1,9 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := + defaultPackage@?{ + name := "positivity2"; + dependencies := [] + }; diff --git a/tests/positive/Internal/Positivity2/main.juvix b/tests/positive/Internal/Positivity2/main.juvix new file mode 100644 index 0000000000..d46d62baec --- /dev/null +++ b/tests/positive/Internal/Positivity2/main.juvix @@ -0,0 +1,58 @@ +module main; + +type T := mkT; + +type Phantom (H : Type) := phantom; + +type Phantom2 (H : Type) := phantom2 (Phantom H); + +type Box (A : Type) := box A; + +module M1; + type T1 (x y : Type) := mkT1 y (x -> x) x; + type T2 (x : (Type -> Type) -> Type) := mkT2 (x (T1 T)); +end; + +module M2; + type T1 (x : Type) := mkT1 (T2 x); + + type T2 (x : Type) := mkT2 (x -> T); + + -- type T3 := mkT3 (T1 T3); +end; + +module M3; + type List (x : Type) := + | nil + | cons x (List x); +end; + +module E1; + type Alice (A : Type) := alice (Phantom2 (Alice A) -> Alice A); + + type Bob (C : Type) := bob (Carol C) (Bob C) (Phantom (Bob C) -> T); + + type Carol (C : Type) := carol (Alice C); +end; + +module E3; + type NotBad (A : Type) := notBad (A -> NotBad A); +end; + +module E5; + type Ghost1 (A : Type) := ghost1 (Ghost2 ((Ghost1 (A -> A)) -> Ghost2 A)); + + type Ghost2 (B : Type) := ghost2 Ok (Ghost1 B); + + type Ok := mkOk (Ghost1 (Ok -> Ok)); +end; + +module E6; + type Nat := + | zero + | suc Nat; + + type Box := mkBox {unbox : Nat}; + + type Foldable := mkFoldable {for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B}; +end; diff --git a/tests/positive/issue3048/Other.juvix b/tests/positive/issue3048/Other.juvix new file mode 100644 index 0000000000..e947739e98 --- /dev/null +++ b/tests/positive/issue3048/Other.juvix @@ -0,0 +1,5 @@ +module Other; + +type T1 := mkT1; +type T2 := mkT2; +type T3 := mkT3; diff --git a/tests/positive/issue3048/Package.juvix b/tests/positive/issue3048/Package.juvix new file mode 100644 index 0000000000..6e4702c194 --- /dev/null +++ b/tests/positive/issue3048/Package.juvix @@ -0,0 +1,10 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := + defaultPackage@?{ + name := "issue3048"; + dependencies := + [github "anoma" "juvix-stdlib" "v0.7.0"; github "anoma" "juvix-containers" "v0.15.0"] + }; diff --git a/tests/positive/issue3048/main.juvix b/tests/positive/issue3048/main.juvix new file mode 100644 index 0000000000..4681b7ecb9 --- /dev/null +++ b/tests/positive/issue3048/main.juvix @@ -0,0 +1,16 @@ +module main; + +import Other; + +type AVLTree (A : Type) := + node (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A) + (AVLTree A); + +type Foo := mkFoo (AVLTree Foo);