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 da4fd8f4b9..c6a94302dd 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Positivity/Checker.hs @@ -89,8 +89,8 @@ checkPositivity noPositivityFlag mut = do markedPositive d = fromJust (find ((== d) . (^. inductiveName)) defs) ^. inductivePositive whenJust (nonEmpty (filter (not . markedPositive) neg)) $ \negTys -> throw $ - ErrNonStrictlyPositiveNew - NonStrictlyPositiveNew + ErrNonStrictlyPositive + NonStrictlyPositive { _nonStrictlyPositiveNewOccurrences = negTys } 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 3ed51dda37..8ead6846c4 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error.hs @@ -22,7 +22,7 @@ data TypeCheckerError | ErrTooManyArgumentsIndType WrongNumberArgumentsIndType | ErrTooFewArgumentsIndType WrongNumberArgumentsIndType | ErrInvalidPatternMatching InvalidPatternMatching - | ErrNonStrictlyPositiveNew NonStrictlyPositiveNew + | ErrNonStrictlyPositive NonStrictlyPositive | ErrUnsupportedTypeFunction UnsupportedTypeFunction | ErrInvalidInstanceType InvalidInstanceType | ErrInvalidCoercionType InvalidCoercionType @@ -69,7 +69,7 @@ instance ToGenericError TypeCheckerError where ErrDefaultArgLoop e -> genericError e ErrBadScope e -> genericError e ErrInvalidConstructorArgType e -> genericError e - ErrNonStrictlyPositiveNew e -> genericError e + ErrNonStrictlyPositive e -> genericError e instance Show TypeCheckerError where show = \case @@ -98,4 +98,4 @@ instance Show TypeCheckerError where ErrBuiltinNotDefined {} -> "ErrBuiltinNotDefined" ErrBadScope {} -> "ErrBadScope" ErrInvalidConstructorArgType {} -> "ErrInvalidConstructorArgType" - ErrNonStrictlyPositiveNew {} -> "ErrNonStrictlyPositiveNew" + 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 d8f355aada..d1dc75ec8c 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 @@ -691,15 +691,15 @@ instance ToGenericError InvalidConstructorArgType where <> line <> ppCode opts' ty -newtype NonStrictlyPositiveNew = NonStrictlyPositiveNew +newtype NonStrictlyPositive = NonStrictlyPositive { -- This list contains occurrences of the inductive types in non-strictly -- positive positions. Thus it may contain repeated names _nonStrictlyPositiveNewOccurrences :: NonEmpty InductiveName } -makeLenses ''NonStrictlyPositiveNew +makeLenses ''NonStrictlyPositive -instance ToGenericError NonStrictlyPositiveNew where +instance ToGenericError NonStrictlyPositive where genericError e = ask >>= generr where generr opts = diff --git a/test/Typecheck/Negative.hs b/test/Typecheck/Negative.hs index 1a192a374c..b4557189d0 100644 --- a/test/Typecheck/Negative.hs +++ b/test/Typecheck/Negative.hs @@ -284,5 +284,5 @@ negPositivityTests = mk :: String -> Path Rel File -> NegTest mk testname testfile = negTest testname $(mkRelDir "Internal/Positivity") testfile $ \case - ErrNonStrictlyPositiveNew NonStrictlyPositiveNew {} -> Nothing + ErrNonStrictlyPositive NonStrictlyPositive {} -> Nothing _ -> wrongError diff --git a/test/Typecheck/NegativeNew.hs b/test/Typecheck/NegativeNew.hs index 81f48e4c94..c705bd5ab9 100644 --- a/test/Typecheck/NegativeNew.hs +++ b/test/Typecheck/NegativeNew.hs @@ -148,14 +148,14 @@ arityTests = _ -> wrongError, negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $ \case - ErrNonStrictlyPositiveNew {} -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError, negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $ \case - ErrNonStrictlyPositiveNew {} -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError, negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $ \case - ErrNonStrictlyPositiveNew {} -> Nothing + ErrNonStrictlyPositive {} -> Nothing _ -> wrongError ]