Skip to content

Commit

Permalink
Fix test suite. Overlooked NegativeNew!!
Browse files Browse the repository at this point in the history
  • Loading branch information
jonaprieto committed Nov 29, 2023
1 parent fbcdfd4 commit 373b350
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 15 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,8 @@ instance Show TypeCheckerError where
ErrTooManyArgumentsIndType {} -> "ErrTooManyArgumentsIndType"
ErrTooFewArgumentsIndType {} -> "ErrTooFewArgumentsIndType"
ErrInvalidPatternMatching {} -> "ErrInvalidPatternMatching"
ErrNoPositivity {} -> "ErrNoPositivity"
ErrUnsupportedTypeFunction {} -> "ErrUnsupportedTypeFunction"
ErrNonStrictlyPositive {} -> "ErrNonStrictlyPositive"
ErrInvalidInstanceType {} -> "ErrInvalidInstanceType"
ErrInvalidCoercionType {} -> "ErrInvalidCoercionType"
ErrWrongCoercionArgument {} -> "ErrWrongCoercionArgument"
Expand Down
16 changes: 2 additions & 14 deletions test/Typecheck/Negative.hs
Original file line number Diff line number Diff line change
Expand Up @@ -298,24 +298,12 @@ negPositivityTests =
\case
ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
_ -> wrongError,
NegTest "E10 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E10.juvix") $
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") $
negTest "E11 uses type synonym" $(mkRelDir "Internal/Positivity") $(mkRelFile "E11.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeInNegativePosition {}) -> Nothing
_ -> wrongError,
NegTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError,
NegTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError,
NegTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError
]
13 changes: 13 additions & 0 deletions test/Typecheck/NegativeNew.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ 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 Juvix.Data.Effect.TaggedLock
import Typecheck.Negative qualified as Old
Expand Down Expand Up @@ -146,5 +147,17 @@ arityTests =
$(mkRelFile "DefaultArgCycleArity.juvix")
$ \case
ErrDefaultArgLoop {} -> Nothing
_ -> wrongError,
negTest "Evil: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "Evil.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError,
negTest "Evil: issue 2540 using Axiom" $(mkRelDir "Internal/Positivity") $(mkRelFile "EvilWithAxiom.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError,
negTest "FreeT: issue 2540" $(mkRelDir "Internal/Positivity") $(mkRelFile "FreeT.juvix") $
\case
ErrNonStrictlyPositive (ErrTypeAsArgumentOfBoundVar {}) -> Nothing
_ -> wrongError
]

0 comments on commit 373b350

Please sign in to comment.