From 018253c84cf73a260ff75032bd3330c39f586729 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Fri, 27 Sep 2024 19:32:50 +0200 Subject: [PATCH] computing polarities --- src/Juvix/Compiler/Internal/Data/Name.hs | 2 + src/Juvix/Compiler/Internal/Language.hs | 2 + src/Juvix/Compiler/Internal/Pretty/Base.hs | 32 +++ .../Analysis/Positivity/Checker.hs | 2 +- .../Analysis/Positivity/CheckerNew.hs | 186 ++++++++++++++++++ .../Analysis/Positivity/ConstructorArg.hs | 75 ++++--- .../Positivity/ConstructorArg/Base.hs | 26 +++ .../Analysis/Positivity/Occurrences.hs | 32 ++- .../Analysis/TypeChecking/CheckerNew.hs | 43 ++-- .../Analysis/TypeChecking/Data/Inference.hs | 1 + .../TypeChecking/Data/ResultBuilder.hs | 16 +- .../Analysis/TypeChecking/Error.hs | 3 + .../Analysis/TypeChecking/Error/Types.hs | 25 +++ .../Analysis/TypeChecking/Traits/Resolver.hs | 7 +- .../Store/Internal/Data/TypeCheckingTables.hs | 5 + src/Juvix/Compiler/Store/Internal/Language.hs | 26 +-- src/Juvix/Data/Polarity.hs | 16 +- test/Typecheck/Negative.hs | 2 +- tests/negative/Internal/Positivity/box.juvix | 5 + 19 files changed, 391 insertions(+), 115 deletions(-) create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs create mode 100644 src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs create mode 100644 tests/negative/Internal/Positivity/box.juvix diff --git a/src/Juvix/Compiler/Internal/Data/Name.hs b/src/Juvix/Compiler/Internal/Data/Name.hs index 63fcc46af8..5060a270ab 100644 --- a/src/Juvix/Compiler/Internal/Data/Name.hs +++ b/src/Juvix/Compiler/Internal/Data/Name.hs @@ -105,6 +105,8 @@ 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..2dc9868ca3 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -11,6 +11,7 @@ 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 @@ -407,6 +408,34 @@ 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 (bracesEnclose res) + +instance PrettyCode AppLhs where + ppCode = \case + AppVar v -> ppCode v + AppAxiom v -> ppCode v + AppInductive v -> ppCode v + +instance PrettyCode Occurrences where + ppCode Occurrences {..} = do + ps <- ppCode _occurrencesPolarity + args <- ppCode _occurrencesTree + return + ( bracesEnclose + [ header "occurrences" <+> kwAssign <+> ps, + header "recursive-args" <+> kwAssign <+> args + ] + ) + instance PrettyCode InfoTable where ppCode tbl = do inds <- ppCode (HashMap.keys (tbl ^. infoInductives)) @@ -463,6 +492,9 @@ instance (PrettyCode a) => PrettyCode (Maybe a) where Nothing -> return "Nothing" Just p -> ("Just" <+>) <$> ppCode p +bracesEnclose :: (Foldable l) => l (Doc ann) -> Doc ann +bracesEnclose = encloseSep "{" "}" "; " . toList + tuple :: [Doc ann] -> Doc ann tuple = encloseSep "(" ")" ", " 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 556ccea620..621089b2cb 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -63,7 +63,7 @@ checkStrictlyPositiveOccurrences :: CheckPositivityArgs -> Sem r () checkStrictlyPositiveOccurrences p = do - traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName)) + -- traceM (prettyText (p ^. checkPositivityArgsInductiveName) <> " # " <> prettyText (p ^. checkPositivityArgsConstructorName)) typeOfConstrArg <- strongNormalize_ (p ^. checkPositivityArgsTypeOfConstructorArg) goExpression False typeOfConstrArg where diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs new file mode 100644 index 0000000000..93dfdbf085 --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/CheckerNew.hs @@ -0,0 +1,186 @@ +module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Internal.Data.InfoTable +import Juvix.Compiler.Internal.Extra +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.Prelude hiding (fromEither) + +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] + } + +data Blocking = Blocking + { _blockingContext :: Polarity, + _blockingUnblocker :: InductiveParam, + -- | The unblocker has to have at least this polarity to unblock + _blockingUnblockerMinimum :: Polarity, + _blockingOccurrences :: Occurrences + } + +makeLenses ''CheckPositivityArgs +makeLenses ''Builder + +emptyBuilder :: Builder +emptyBuilder = + Builder + { _builderPolarities = mempty, + _builderBlocking = mempty + } + +checkPositivity :: + forall r. + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + ResultBuilder, + Inference + ] + r + ) => + MutualBlock -> + Sem r () +checkPositivity 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 + traceM ("add polarities " <> ppTrace defName <> ": " <> prettyText polarities) + addPolarities (defName ^. nameId) polarities + +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 + forM_ (HashMap.toList (o ^. occurrencesPolarity)) (uncurry addPolarity) + forM_ (HashMap.toList (o ^. occurrencesTree)) (uncurry goApp) + where + addPolarity :: InductiveParam -> Polarity -> Sem r () + addPolarity var p = do + modif <- ask + b <- get + let old :: Maybe Polarity = b ^. builderPolarities . at var + new :: Polarity = maybe id (<>) old (p <> modif) + modify (set (builderPolarities . at var) (Just new)) + when (old < Just new) (unblock var new) + + unblock :: InductiveParam -> Polarity -> Sem r () + unblock p newPol = undefined + + goApp :: forall r. (Members '[State Builder, Reader Polarity] r) => AppLhs -> [Occurrences] -> Sem r () + goApp lhs os = case lhs of + AppVar {} -> goVarArgs os + AppAxiom {} -> goAxiomArgs os + AppInductive a -> goInductive a os + + localPolarity :: (Members '[Reader Polarity] r) => Polarity -> Sem r () -> Sem r () + localPolarity = \case + PolarityUnused -> const (return ()) + PolarityNegative -> local (const PolarityNegative) + PolarityStrictlyPositive -> local (const PolarityStrictlyPositive) + + -- NOTE we assume that axioms have all variables in strictly positive positions + goAxiomArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () + goAxiomArgs os = mapM_ go os + + goVarArgs :: (Members '[State Builder, Reader Polarity] r) => [Occurrences] -> Sem r () + goVarArgs os = mapM_ go os + + blockOn :: + (Members '[State Builder, Reader Polarity] r) => + Polarity -> + InductiveParam -> + Occurrences -> + Sem r () + blockOn 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 = + case tab ^. polarityTable . at (d ^. nameId) of + Just pols -> + forM_ (zipExact pols os) $ \(pol :: Polarity, o :: Occurrences) -> do + localPolarity pol (go o) + Nothing -> do + pols :: [(InductiveParam, Maybe Polarity)] <- getInductivePolarities d + traceM ("mutually recursive TODO" <> ppTrace d <> "\n" <> ppTrace topOccurrences <> "\n" <> ppTrace pols) + forM_ (zipExact pols os) $ \((p :: InductiveParam, mpol :: Maybe Polarity), o :: Occurrences) -> do + traceM ("mpol " <> ppTrace mpol) + case mpol of + Nothing -> blockOn PolarityStrictlyPositive p o + Just pol -> case pol of + PolarityNegative -> localPolarity pol (go o) + PolarityStrictlyPositive -> do + blockOn (succ pol) p o + localPolarity pol (go o) + PolarityUnused -> impossible diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs index 984ea7628d..511771a667 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg.hs @@ -1,58 +1,49 @@ -module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg where +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 -data ConstructorArg - = ConstructorArgFun Fun - | ConstructorArgApp App +mkConstructorArg :: (Members '[Error TypeCheckerError] r) => NormalizedExpression -> Sem r [ConstructorArg] +mkConstructorArg = mapM (goArg . (^. paramType)) . fst . unfoldFunType . (^. normalizedExpression) -data Fun = Fun - { _funLeft :: ConstructorArg, - _funRight :: ConstructorArg - } - -data AppLhs - = AppVar VarName - | AppAxiom AxiomName - | AppInductive InductiveName - deriving stock (Eq, Generic) - -instance Hashable AppLhs - -data App = App - { _appLhs :: AppLhs, - _appArgs :: [ConstructorArg] - } - --- | The -mkConstructorArg :: (Members '[Error ()] r) => NormalizedExpression -> Sem r ConstructorArg -mkConstructorArg = mkConstructorArg' . (^. normalizedExpression) - -mkConstructorArg' :: forall r. (Members '[Error ()] r) => Expression -> Sem r ConstructorArg -mkConstructorArg' = \case +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 ExpressionFunction i -> goFunction i - ExpressionLiteral {} -> throw () - ExpressionHole {} -> throw () - ExpressionInstanceHole {} -> throw () - ExpressionLet {} -> throw () - ExpressionUniverse {} -> throw () - ExpressionSimpleLambda {} -> throw () - ExpressionLambda {} -> throw () - ExpressionCase {} -> throw () + ExpressionLiteral {} -> invalid + ExpressionHole {} -> invalid + ExpressionInstanceHole {} -> invalid + ExpressionLet {} -> invalid + ExpressionUniverse {} -> 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 - _ -> throw () + _ -> invalid goFunction :: Function -> Sem r ConstructorArg goFunction fun = do - l <- mkConstructorArg' (fun ^. functionLeft . paramType) - r <- mkConstructorArg' (fun ^. functionRight) + l <- goArg (fun ^. functionLeft . paramType) + r <- goArg (fun ^. functionRight) return $ ConstructorArgFun Fun @@ -66,10 +57,10 @@ mkConstructorArg' = \case goApplicationHelper :: (Expression, [Expression]) -> Sem r ConstructorArg goApplicationHelper (f, args) = do i <- getIden f - cargs <- mapM mkConstructorArg' args + cargs <- mapM goArg args lhs :: AppLhs <- case i of - IdenFunction {} -> throw () - IdenConstructor {} -> throw () + IdenFunction {} -> invalid + IdenConstructor {} -> invalid IdenVar v -> return (AppVar v) IdenAxiom v -> return (AppAxiom v) IdenInductive v -> return (AppInductive v) 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..6cff9fc2e9 --- /dev/null +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/ConstructorArg/Base.hs @@ -0,0 +1,26 @@ +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 + +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/Occurrences.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs index 6fdc0996f6..16d7151546 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Occurrences.hs @@ -1,11 +1,16 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences - ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Occurrences, - module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg, + ( module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base, + Occurrences (..), + mkOccurrences, + occurrencesPolarity, + occurrencesTree, + occurrencesAggregatePolarities, ) where +import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Internal.Language -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.ConstructorArg.Base import Juvix.Prelude data FunctionSide @@ -22,9 +27,10 @@ instance Monoid FunctionSide where mempty = FunctionRight data Occurrences = Occurrences - { _occurrencesPolarity :: HashMap VarName Polarity, + { _occurrencesPolarity :: HashMap InductiveParam Polarity, _occurrencesTree :: HashMap AppLhs [Occurrences] } + deriving stock (Show) makeLenses ''Occurrences @@ -35,6 +41,14 @@ emptyOccurrences = _occurrencesTree = mempty } +occurrencesAggregatePolarities :: Occurrences -> HashMap InductiveParam Polarity +occurrencesAggregatePolarities = run . execState mempty . go + where + go :: Occurrences -> Sem '[State (HashMap InductiveParam Polarity)] () + go o = do + modify (HashMap.unionWith (<>) (o ^. occurrencesPolarity)) + mapM_ go (concat (toList (o ^. occurrencesTree))) + mkOccurrences :: [ConstructorArg] -> Occurrences mkOccurrences = run @@ -44,16 +58,16 @@ mkOccurrences = where getPolarity :: forall r'. (Members '[Reader FunctionSide] r') => Sem r' Polarity getPolarity = - ask <&> \case - FunctionLeft -> PolarityNegative - FunctionRight -> PolarityStrictlyPositive + ask <&> \case + FunctionLeft -> PolarityNegative + FunctionRight -> PolarityStrictlyPositive addArg :: forall r'. (Members '[Reader FunctionSide, State Occurrences] r') => ConstructorArg -> Sem r' () addArg = \case ConstructorArgFun fun -> goFun fun ConstructorArgApp a -> goApp a where - registerOccurrence :: VarName -> Sem r' () + registerOccurrence :: InductiveParam -> Sem r' () registerOccurrence v = do pol <- getPolarity modify (over (occurrencesPolarity . at v) (Just . maybe pol (<> pol))) @@ -64,7 +78,7 @@ mkOccurrences = AppAxiom {} -> goArgs AppInductive {} -> goArgs where - goVar :: VarName -> Sem r' () + goVar :: InductiveParam -> Sem r' () goVar v = do registerOccurrence v goArgs 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 c24f4e48c7..1fa0708b8b 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs @@ -20,6 +20,7 @@ import Juvix.Compiler.Internal.Extra.CoercionInfo import Juvix.Compiler.Internal.Extra.InstanceInfo import Juvix.Compiler.Internal.Pretty import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.Checker +import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Positivity.CheckerNew qualified as New import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker (Termination) import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.CheckerNew.Arity import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context @@ -131,7 +132,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 @@ -251,31 +252,27 @@ checkTopMutualBlock :: (Members '[HighlightBuilder, Reader BuiltinsTable, State NegativeTypeParameters, Reader EntryPoint, Reader LocalVars, Reader InfoTable, Error TypeCheckerError, NameIdGen, ResultBuilder, Termination, Reader InsertedArgsStack] r) => MutualBlock -> Sem r MutualBlock -checkTopMutualBlock (MutualBlock ds) = do - m <- MutualBlock <$> runInferenceDefs (mapM checkMutualStatement ds) - checkBlockPositivity m - return m +checkTopMutualBlock (MutualBlock ds) = + MutualBlock + <$> runInferenceDefs + ( do + ls <- mapM checkMutualStatement ds + checkBlockPositivity (MutualBlock ls) -- TODO uncomment + return ls + ) checkBlockPositivity :: - -- ( Members - -- '[ - -- HighlightBuilder, - -- Reader BuiltinsTable, - -- State NegativeTypeParameters, - -- Reader EntryPoint, - -- Reader LocalVars, - -- Reader InfoTable, - -- Error TypeCheckerError, - -- NameIdGen, - -- ResultBuilder, - -- Termination, - -- Reader InsertedArgsStack - -- ] - -- r - -- ) => + ( Members + '[ Reader InfoTable, + Error TypeCheckerError, + ResultBuilder, + Inference + ] + r + ) => MutualBlock -> Sem r () -checkBlockPositivity _ = return () +checkBlockPositivity = New.checkPositivity resolveCastHoles :: forall a r. @@ -417,7 +414,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..007f922c6c 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -40,6 +40,7 @@ data TypeCheckerError | ErrArityCheckerError ArityCheckerError | ErrDefaultArgLoop DefaultArgLoop | ErrBadScope BadScope + | ErrInvalidConstructorArgType InvalidConstructorArgType instance ToGenericError TypeCheckerError where genericError :: (Member (Reader GenericOptions) r) => TypeCheckerError -> Sem r GenericError @@ -69,6 +70,7 @@ instance ToGenericError TypeCheckerError where ErrArityCheckerError e -> genericError e ErrDefaultArgLoop e -> genericError e ErrBadScope e -> genericError e + ErrInvalidConstructorArgType e -> genericError e instance Show TypeCheckerError where show = \case @@ -97,3 +99,4 @@ instance Show TypeCheckerError where ErrDefaultArgLoop {} -> "ErrDefaultArgLoop" ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined" ErrBadScope {} -> "ErrBadScope" + ErrInvalidConstructorArgType {} -> "ErrInvalidConstructorArgType" 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..e16f85f00e 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,28 @@ 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 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/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/Polarity.hs b/src/Juvix/Data/Polarity.hs index 1c6d6e6e5e..fca7f414cd 100644 --- a/src/Juvix/Data/Polarity.hs +++ b/src/Juvix/Data/Polarity.hs @@ -4,12 +4,13 @@ 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 - = -- TODO rename PolarityNegative to PolarityNotStrictlyPositive - PolarityNegative + = PolarityUnused | PolarityStrictlyPositive - | PolarityUnused - deriving stock (Eq, Generic, Data, Show) + | -- TODO rename PolarityNegative to PolarityNotStrictlyPositive + PolarityNegative + deriving stock (Ord, Enum, Bounded, Eq, Generic, Data, Show) instance Hashable Polarity @@ -18,12 +19,7 @@ instance Serialize Polarity instance NFData Polarity instance Semigroup Polarity where - a <> b = case (a, b) of - (PolarityUnused, p) -> p - (p, PolarityUnused) -> p - (PolarityNegative, _) -> PolarityNegative - (_, PolarityNegative) -> PolarityNegative - (PolarityStrictlyPositive, PolarityStrictlyPositive) -> PolarityStrictlyPositive + a <> b = max a b instance Monoid Polarity where mempty = PolarityUnused diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 54528419ae..210f00cf8d 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -279,7 +279,7 @@ negPositivityTests = mk "E9" $(mkRelFile "E9.juvix"), mk "E10 uses type synonym" $(mkRelFile "E10.juvix"), mk "E11 uses type synonym" $(mkRelFile "E11.juvix"), - mk "Phantom parameter" $(mkRelFile "phantom.juvix") + mk "Box left hand side" $(mkRelFile "box.juvix") ] where mk :: String -> Path Rel File -> NegTest 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;