assertica / test /Test /Core /Positivity.hs

October 2026 main drop: mirror from GitHub

a10b189 verified about 1 month ago

13.1 kB

{-# LANGUAGE OverloadedStrings #-}

{-|
Module      : Test.Core.Positivity
Description : Tests for positivity checking (Agent 4B)
-}

module Test.Core.Positivity
  ( tests
  ) where

import Test.Tasty
import Test.Tasty.HUnit
import qualified Data.Set as Set
import qualified Data.Text as T

import Assertica.Core.AST
import Assertica.Core.Positivity

-- ============================================================================
-- TEST SUITE
-- ============================================================================

tests :: TestTree
tests = testGroup "Assertica.Core.Positivity"
  [ testGroup "Basic Positivity"
      [ testCase "Type with no parameters needs no checking" testNoParams
      , testCase "Strictly positive list type" testListPositive
      , testCase "Strictly positive tree type" testTreePositive
      ]

  , testGroup "Negative Position Detection"
      [ testCase "Function domain is negative position" testFunctionDomainNegative
      , testCase "Type parameter in function domain rejected" testParamInDomainRejected
      , testCase "Nested function domain rejected" testNestedFunctionNegative
      ]

  , testGroup "Constructor Analysis"
      [ testCase "Multiple constructors checked" testMultipleConstructors
      , testCase "Nested positive occurrences accepted" testNestedPositive
      , testCase "Mixed positive and negative rejected" testMixedPositiveNegative
      ]

  , testGroup "Type Parameter Tracking"
      [ testCase "Occurrence analysis finds type variables" testOccurrenceAnalysis
      , testCase "Analyze position context" testPositionContext
      , testCase "Nested type structures" testNestedTypeStructures
      ]

  , testGroup "Practical Examples"
      [ testCase "List a is strictly positive" testListStrictlyPositive
      , testCase "Tree a is strictly positive" testTreeStrictlyPositive
      , testCase "BadType (a -> Int) rejected" testBadTypeRejected
      , testCase "BadList with function in arg rejected" testBadListRejected
      ]

  , testGroup "Mutual/Recursive Inductive Types"
      [ testCase "Mutual positive types accepted" testMutualPositive
      , testCase "Mutual with negative occurrence rejected" testMutualWithNegative
      ]

  , testGroup "Error Messages"
      [ testCase "Non-positive occurrence message" testNonPositiveMessage
      , testCase "Function domain message" testFunctionDomainMessage
      , testCase "Nested negative message" testNestedNegativeMessage
      ]
  ]

-- ============================================================================
-- HELPER FUNCTIONS
-- ============================================================================

{-| Create a simple variable. -}
var :: Text -> Var
var name = Var name 0

{-| Create a qualified name. -}
qn :: Text -> QName
qn name = QName [] name

{-| Create a binder. -}
binder :: Text -> Maybe Type -> Binder
binder name mty = Binder (var name) mty

{-| Create a type variable. -}
tyVar :: Text -> Type
tyVar name = TyVar (var name)

{-| Create a type constructor application. -}
tyConst :: Text -> [Type] -> Type
tyConst name args = TyConst (qn name) args

{-| Create a function type. -}
tyFun :: Type -> Type -> Type
tyFun = TyFun

-- ============================================================================
-- BASIC POSITIVITY TESTS
-- ============================================================================

testNoParams :: Assertion
testNoParams = do
  -- data Nat = Zero | Succ Nat (no type parameters)
  let params = []
      ctors = [tyConst "Nat" []]

  case checkPositivity "Nat" params ctors of
    Right () -> return ()
    Left err -> assertFailure $ "Nat should be positive: " ++ prettyPosError err

testListPositive :: Assertion
testListPositive = do
  -- data List a = Nil | Cons a (List a)
  let a = var "a"
      params = [a]
      -- Cons argument types: [a, List a]
      ctors = [tyVar "a", tyConst "List" [tyVar "a"]]

  case checkPositivity "List" params ctors of
    Right () -> return ()
    Left err -> assertFailure $ "List should be positive: " ++ prettyPosError err

testTreePositive :: Assertion
testTreePositive = do
  -- data Tree a = Leaf a | Node (Tree a) (Tree a)
  let a = var "a"
      params = [a]
      -- Constructor args: [a] for Leaf, [Tree a, Tree a] for Node
      ctors = [tyVar "a", tyConst "Tree" [tyVar "a"], tyConst "Tree" [tyVar "a"]]

  case checkPositivity "Tree" params ctors of
    Right () -> return ()
    Left err -> assertFailure $ "Tree should be positive: " ++ prettyPosError err

-- ============================================================================
-- NEGATIVE POSITION DETECTION TESTS
-- ============================================================================

testFunctionDomainNegative :: Assertion
testFunctionDomainNegative = do
  -- Type parameter appears in function domain: a -> Int
  let a = var "a"
      params = [a]
      -- Argument type: a -> Int
      ctors = [tyFun (tyVar "a") (tyConst "Int" [])]

  case checkPositivity "Bad" params ctors of
    Left (TypeVarInFunctionDomain _) -> return ()  -- Should reject
    Left err -> assertFailure $ "Wrong error type: " ++ prettyPosError err
    Right () -> assertFailure "Function domain should be rejected"

testParamInDomainRejected :: Assertion
testParamInDomainRejected = do
  -- data BadType a = Bad (a -> Int)
  let a = var "a"
      params = [a]
      ctors = [tyFun (tyVar "a") (tyConst "Int" [])]

  case checkPositivity "BadType" params ctors of
    Left (TypeVarInFunctionDomain "a") -> return ()
    _ -> assertFailure "Should reject a in function domain"

testNestedFunctionNegative :: Assertion
testNestedFunctionNegative = do
  -- data BadList a = Cons a (List (a -> Int))
  let a = var "a"
      params = [a]
      -- (a -> Int) is in a positive position but contains a in negative
      listOfFunc = tyConst "List" [tyFun (tyVar "a") (tyConst "Int" [])]
      ctors = [tyVar "a", listOfFunc]

  case checkPositivity "BadList" params ctors of
    Left (NestedNegativeOccurrence "a" _) -> return ()
    _ -> assertFailure "Should detect nested negative occurrence"

-- ============================================================================
-- CONSTRUCTOR ANALYSIS TESTS
-- ============================================================================

testMultipleConstructors :: Assertion
testMultipleConstructors = do
  -- data List a = Nil | Cons a (List a)
  -- Both constructors must be checked
  let a = var "a"
      params = [a]
      -- Nil args, Cons args
      ctors = [tyConst "List" [tyVar "a"]]

  case checkPositivity "List" params ctors of
    Right () -> return ()
    Left err -> assertFailure $ "Multiple constructors should all pass: " ++ prettyPosError err

testNestedPositive :: Assertion
testNestedPositive = do
  -- Nested type constructor applications in positive positions
  -- data Okay a = OK (List (List a))
  let a = var "a"
      params = [a]
      nestedList = tyConst "List" [tyConst "List" [tyVar "a"]]
      ctors = [nestedList]

  case checkPositivity "Okay" params ctors of
    Right () -> return ()
    Left err -> assertFailure $ "Nested positive should pass: " ++ prettyPosError err

testMixedPositiveNegative :: Assertion
testMixedPositiveNegative = do
  -- data Mixed a = Good a | Bad (a -> Int)
  -- First constructor is fine, second violates positivity
  let a = var "a"
      params = [a]
      ctors = [tyVar "a", tyFun (tyVar "a") (tyConst "Int" [])]

  case checkPositivity "Mixed" params ctors of
    Left _ -> return ()  -- Should reject due to negative occurrence
    Right () -> assertFailure "Should reject negative occurrence"

-- ============================================================================
-- TYPE PARAMETER TRACKING TESTS
-- ============================================================================

testOccurrenceAnalysis :: Assertion
testOccurrenceAnalysis = do
  -- Analyze where a type variable appears
  let params = Set.singleton "a"
      ty = tyFun (tyVar "a") (tyConst "List" [tyVar "a"])

  let occs = analyzeTypeOccurrences params ty
  assertBool "Should find multiple occurrences of a" (length occs >= 1)
  let hasNeg = any (\o -> occPosition o == Negative) occs
  assertBool "Should find negative occurrence in domain" hasNeg

testPositionContext :: Assertion
testPositionContext = do
  -- Verify position tracking
  let params = Set.singleton "a"
      ty = tyConst "List" [tyVar "a"]

  let occs = analyzeTypeOccurrences params ty
  case occs of
    [TypeOccurrence _ pos _] ->
      assertEqual "Should be in positive position" pos Positive
    _ -> assertFailure "Should find exactly one occurrence"

testNestedTypeStructures :: Assertion
testNestedTypeStructures = do
  -- Complex nested type: List (Tree (a -> Int))
  let params = Set.singleton "a"
      negFunc = tyFun (tyVar "a") (tyConst "Int" [])
      tree = tyConst "Tree" [negFunc]
      list = tyConst "List" [tree]

  let occs = analyzeTypeOccurrences params list
  let hasNeg = any (\o -> occPosition o == Negative) occs
  assertBool "Should track nested negative position" hasNeg

-- ============================================================================
-- PRACTICAL EXAMPLE TESTS
-- ============================================================================

testListStrictlyPositive :: Assertion
testListStrictlyPositive = do
  -- data List a = Nil | Cons a (List a)
  let a = var "a"
      params = [a]
      nilCtors = []  -- Nil has no arguments
      consCtors = [tyVar "a", tyConst "List" [tyVar "a"]]
      allCtors = nilCtors ++ consCtors

  case checkPositivity "List" params allCtors of
    Right () -> return ()
    Left err -> assertFailure $ "List should be strictly positive: " ++ prettyPosError err

testTreeStrictlyPositive :: Assertion
testTreeStrictlyPositive = do
  -- data Tree a = Leaf a | Node (Tree a) (Tree a)
  let a = var "a"
      params = [a]
      leafCtors = [tyVar "a"]
      nodeCtors = [tyConst "Tree" [tyVar "a"], tyConst "Tree" [tyVar "a"]]
      allCtors = leafCtors ++ nodeCtors

  case checkPositivity "Tree" params allCtors of
    Right () -> return ()
    Left err -> assertFailure $ "Tree should be strictly positive: " ++ prettyPosError err

testBadTypeRejected :: Assertion
testBadTypeRejected = do
  -- data BadType a = Bad (a -> Int)
  let a = var "a"
      params = [a]
      badCtors = [tyFun (tyVar "a") (tyConst "Int" [])]

  case checkPositivity "BadType" params badCtors of
    Left _ -> return ()  -- Should be rejected
    Right () -> assertFailure "BadType should be rejected"

testBadListRejected :: Assertion
testBadListRejected = do
  -- data BadList a = Cons a (BadList (a -> Int))
  let a = var "a"
      params = [a]
      funcType = tyFun (tyVar "a") (tyConst "Int" [])
      badListArg = tyConst "BadList" [funcType]
      badCtors = [tyVar "a", badListArg]

  case checkPositivity "BadList" params badCtors of
    Left _ -> return ()  -- Should be rejected
    Right () -> assertFailure "BadList should be rejected"

-- ============================================================================
-- MUTUAL/RECURSIVE INDUCTIVE TYPES TESTS
-- ============================================================================

testMutualPositive :: Assertion
testMutualPositive = do
  -- data Even = Zero | SuccO Odd
  -- data Odd = SuccE Even
  let defs =
        [ ("Even", [], [tyConst "Odd" []])
        , ("Odd", [], [tyConst "Even" []])
        ]

  case checkPositivityMulti defs of
    Right () -> return ()
    Left err -> assertFailure $ "Mutual types should pass: " ++ prettyPosError err

testMutualWithNegative :: Assertion
testMutualWithNegative = do
  -- data Even = Zero | SuccO (Odd -> Int)  -- NEGATIVE!
  -- data Odd = SuccE Even
  let a = var "a"
      defs =
        [ ("Even", [a], [tyFun (tyConst "Odd" []) (tyConst "Int" [])])
        , ("Odd", [a], [tyConst "Even" []])
        ]

  case checkPositivityMulti defs of
    Left _ -> return ()  -- Should be rejected
    Right () -> assertFailure "Mutual with negative should be rejected"

-- ============================================================================
-- ERROR MESSAGE TESTS
-- ============================================================================

testNonPositiveMessage :: Assertion
testNonPositiveMessage = do
  let err = NonPositiveOccurrence "a" "in function domain"
  let msg = prettyPosError err
  assertBool "Error should mention type parameter" $ "a" `elem` words msg
  assertBool "Error should mention non-positive" $ "non-positive" `elem` words msg

testFunctionDomainMessage :: Assertion
testFunctionDomainMessage = do
  let err = TypeVarInFunctionDomain "a"
  let msg = prettyPosError err
  assertBool "Error should mention function domain" $ "domain" `elem` words msg
  assertBool "Error should mention parameter a" $ "a" `elem` words msg

testNestedNegativeMessage :: Assertion
testNestedNegativeMessage = do
  let err = NestedNegativeOccurrence "a" "in List (a -> Int)"
  let msg = prettyPosError err
  assertBool "Error should mention nested" $ "nested" `elem` words msg
  assertBool "Error should mention negative" $ "negative" `elem` words msg

	{-# LANGUAGE OverloadedStrings #-}

	{-\|
	Module : Test.Core.Positivity
	Description : Tests for positivity checking (Agent 4B)
	-}

	module Test.Core.Positivity
	( tests
	) where

	import Test.Tasty
	import Test.Tasty.HUnit
	import qualified Data.Set as Set
	import qualified Data.Text as T

	import Assertica.Core.AST
	import Assertica.Core.Positivity

	-- ============================================================================
	-- TEST SUITE
	-- ============================================================================

	tests :: TestTree
	tests = testGroup "Assertica.Core.Positivity"
	[ testGroup "Basic Positivity"
	[ testCase "Type with no parameters needs no checking" testNoParams
	, testCase "Strictly positive list type" testListPositive
	, testCase "Strictly positive tree type" testTreePositive
	]

	, testGroup "Negative Position Detection"
	[ testCase "Function domain is negative position" testFunctionDomainNegative
	, testCase "Type parameter in function domain rejected" testParamInDomainRejected
	, testCase "Nested function domain rejected" testNestedFunctionNegative
	]

	, testGroup "Constructor Analysis"
	[ testCase "Multiple constructors checked" testMultipleConstructors
	, testCase "Nested positive occurrences accepted" testNestedPositive
	, testCase "Mixed positive and negative rejected" testMixedPositiveNegative
	]

	, testGroup "Type Parameter Tracking"
	[ testCase "Occurrence analysis finds type variables" testOccurrenceAnalysis
	, testCase "Analyze position context" testPositionContext
	, testCase "Nested type structures" testNestedTypeStructures
	]

	, testGroup "Practical Examples"
	[ testCase "List a is strictly positive" testListStrictlyPositive
	, testCase "Tree a is strictly positive" testTreeStrictlyPositive
	, testCase "BadType (a -> Int) rejected" testBadTypeRejected
	, testCase "BadList with function in arg rejected" testBadListRejected
	]

	, testGroup "Mutual/Recursive Inductive Types"
	[ testCase "Mutual positive types accepted" testMutualPositive
	, testCase "Mutual with negative occurrence rejected" testMutualWithNegative
	]

	, testGroup "Error Messages"
	[ testCase "Non-positive occurrence message" testNonPositiveMessage
	, testCase "Function domain message" testFunctionDomainMessage
	, testCase "Nested negative message" testNestedNegativeMessage
	]
	]

	-- ============================================================================
	-- HELPER FUNCTIONS
	-- ============================================================================

	{-\| Create a simple variable. -}
	var :: Text -> Var
	var name = Var name 0

	{-\| Create a qualified name. -}
	qn :: Text -> QName
	qn name = QName [] name

	{-\| Create a binder. -}
	binder :: Text -> Maybe Type -> Binder
	binder name mty = Binder (var name) mty

	{-\| Create a type variable. -}
	tyVar :: Text -> Type
	tyVar name = TyVar (var name)

	{-\| Create a type constructor application. -}
	tyConst :: Text -> [Type] -> Type
	tyConst name args = TyConst (qn name) args

	{-\| Create a function type. -}
	tyFun :: Type -> Type -> Type
	tyFun = TyFun

	-- ============================================================================
	-- BASIC POSITIVITY TESTS
	-- ============================================================================

	testNoParams :: Assertion
	testNoParams = do
	-- data Nat = Zero \| Succ Nat (no type parameters)
	let params = []
	ctors = [tyConst "Nat" []]

	case checkPositivity "Nat" params ctors of
	Right () -> return ()
	Left err -> assertFailure $ "Nat should be positive: " ++ prettyPosError err

	testListPositive :: Assertion
	testListPositive = do
	-- data List a = Nil \| Cons a (List a)
	let a = var "a"
	params = [a]
	-- Cons argument types: [a, List a]
	ctors = [tyVar "a", tyConst "List" [tyVar "a"]]

	case checkPositivity "List" params ctors of
	Right () -> return ()
	Left err -> assertFailure $ "List should be positive: " ++ prettyPosError err

	testTreePositive :: Assertion
	testTreePositive = do
	-- data Tree a = Leaf a \| Node (Tree a) (Tree a)
	let a = var "a"
	params = [a]
	-- Constructor args: [a] for Leaf, [Tree a, Tree a] for Node
	ctors = [tyVar "a", tyConst "Tree" [tyVar "a"], tyConst "Tree" [tyVar "a"]]

	case checkPositivity "Tree" params ctors of
	Right () -> return ()
	Left err -> assertFailure $ "Tree should be positive: " ++ prettyPosError err

	-- ============================================================================
	-- NEGATIVE POSITION DETECTION TESTS
	-- ============================================================================

	testFunctionDomainNegative :: Assertion
	testFunctionDomainNegative = do
	-- Type parameter appears in function domain: a -> Int
	let a = var "a"
	params = [a]
	-- Argument type: a -> Int
	ctors = [tyFun (tyVar "a") (tyConst "Int" [])]

	case checkPositivity "Bad" params ctors of
	Left (TypeVarInFunctionDomain _) -> return () -- Should reject
	Left err -> assertFailure $ "Wrong error type: " ++ prettyPosError err
	Right () -> assertFailure "Function domain should be rejected"

	testParamInDomainRejected :: Assertion
	testParamInDomainRejected = do
	-- data BadType a = Bad (a -> Int)
	let a = var "a"
	params = [a]
	ctors = [tyFun (tyVar "a") (tyConst "Int" [])]

	case checkPositivity "BadType" params ctors of
	Left (TypeVarInFunctionDomain "a") -> return ()
	_ -> assertFailure "Should reject a in function domain"

	testNestedFunctionNegative :: Assertion
	testNestedFunctionNegative = do
	-- data BadList a = Cons a (List (a -> Int))
	let a = var "a"
	params = [a]
	-- (a -> Int) is in a positive position but contains a in negative
	listOfFunc = tyConst "List" [tyFun (tyVar "a") (tyConst "Int" [])]
	ctors = [tyVar "a", listOfFunc]

	case checkPositivity "BadList" params ctors of
	Left (NestedNegativeOccurrence "a" _) -> return ()
	_ -> assertFailure "Should detect nested negative occurrence"

	-- ============================================================================
	-- CONSTRUCTOR ANALYSIS TESTS
	-- ============================================================================

	testMultipleConstructors :: Assertion
	testMultipleConstructors = do
	-- data List a = Nil \| Cons a (List a)
	-- Both constructors must be checked
	let a = var "a"
	params = [a]
	-- Nil args, Cons args
	ctors = [tyConst "List" [tyVar "a"]]

	case checkPositivity "List" params ctors of
	Right () -> return ()
	Left err -> assertFailure $ "Multiple constructors should all pass: " ++ prettyPosError err

	testNestedPositive :: Assertion
	testNestedPositive = do
	-- Nested type constructor applications in positive positions
	-- data Okay a = OK (List (List a))
	let a = var "a"
	params = [a]
	nestedList = tyConst "List" [tyConst "List" [tyVar "a"]]
	ctors = [nestedList]

	case checkPositivity "Okay" params ctors of
	Right () -> return ()
	Left err -> assertFailure $ "Nested positive should pass: " ++ prettyPosError err

	testMixedPositiveNegative :: Assertion
	testMixedPositiveNegative = do
	-- data Mixed a = Good a \| Bad (a -> Int)
	-- First constructor is fine, second violates positivity
	let a = var "a"
	params = [a]
	ctors = [tyVar "a", tyFun (tyVar "a") (tyConst "Int" [])]

	case checkPositivity "Mixed" params ctors of
	Left _ -> return () -- Should reject due to negative occurrence
	Right () -> assertFailure "Should reject negative occurrence"

	-- ============================================================================
	-- TYPE PARAMETER TRACKING TESTS
	-- ============================================================================

	testOccurrenceAnalysis :: Assertion
	testOccurrenceAnalysis = do
	-- Analyze where a type variable appears
	let params = Set.singleton "a"
	ty = tyFun (tyVar "a") (tyConst "List" [tyVar "a"])

	let occs = analyzeTypeOccurrences params ty
	assertBool "Should find multiple occurrences of a" (length occs >= 1)
	let hasNeg = any (\o -> occPosition o == Negative) occs
	assertBool "Should find negative occurrence in domain" hasNeg

	testPositionContext :: Assertion
	testPositionContext = do
	-- Verify position tracking
	let params = Set.singleton "a"
	ty = tyConst "List" [tyVar "a"]

	let occs = analyzeTypeOccurrences params ty
	case occs of
	[TypeOccurrence _ pos _] ->
	assertEqual "Should be in positive position" pos Positive
	_ -> assertFailure "Should find exactly one occurrence"

	testNestedTypeStructures :: Assertion
	testNestedTypeStructures = do
	-- Complex nested type: List (Tree (a -> Int))
	let params = Set.singleton "a"
	negFunc = tyFun (tyVar "a") (tyConst "Int" [])
	tree = tyConst "Tree" [negFunc]
	list = tyConst "List" [tree]

	let occs = analyzeTypeOccurrences params list
	let hasNeg = any (\o -> occPosition o == Negative) occs
	assertBool "Should track nested negative position" hasNeg

	-- ============================================================================
	-- PRACTICAL EXAMPLE TESTS
	-- ============================================================================

	testListStrictlyPositive :: Assertion
	testListStrictlyPositive = do
	-- data List a = Nil \| Cons a (List a)
	let a = var "a"
	params = [a]
	nilCtors = [] -- Nil has no arguments
	consCtors = [tyVar "a", tyConst "List" [tyVar "a"]]
	allCtors = nilCtors ++ consCtors

	case checkPositivity "List" params allCtors of
	Right () -> return ()
	Left err -> assertFailure $ "List should be strictly positive: " ++ prettyPosError err

	testTreeStrictlyPositive :: Assertion
	testTreeStrictlyPositive = do
	-- data Tree a = Leaf a \| Node (Tree a) (Tree a)
	let a = var "a"
	params = [a]
	leafCtors = [tyVar "a"]
	nodeCtors = [tyConst "Tree" [tyVar "a"], tyConst "Tree" [tyVar "a"]]
	allCtors = leafCtors ++ nodeCtors

	case checkPositivity "Tree" params allCtors of
	Right () -> return ()
	Left err -> assertFailure $ "Tree should be strictly positive: " ++ prettyPosError err

	testBadTypeRejected :: Assertion
	testBadTypeRejected = do
	-- data BadType a = Bad (a -> Int)
	let a = var "a"
	params = [a]
	badCtors = [tyFun (tyVar "a") (tyConst "Int" [])]

	case checkPositivity "BadType" params badCtors of
	Left _ -> return () -- Should be rejected
	Right () -> assertFailure "BadType should be rejected"

	testBadListRejected :: Assertion
	testBadListRejected = do
	-- data BadList a = Cons a (BadList (a -> Int))
	let a = var "a"
	params = [a]
	funcType = tyFun (tyVar "a") (tyConst "Int" [])
	badListArg = tyConst "BadList" [funcType]
	badCtors = [tyVar "a", badListArg]

	case checkPositivity "BadList" params badCtors of
	Left _ -> return () -- Should be rejected
	Right () -> assertFailure "BadList should be rejected"

	-- ============================================================================
	-- MUTUAL/RECURSIVE INDUCTIVE TYPES TESTS
	-- ============================================================================

	testMutualPositive :: Assertion
	testMutualPositive = do
	-- data Even = Zero \| SuccO Odd
	-- data Odd = SuccE Even
	let defs =
	[ ("Even", [], [tyConst "Odd" []])
	, ("Odd", [], [tyConst "Even" []])
	]

	case checkPositivityMulti defs of
	Right () -> return ()
	Left err -> assertFailure $ "Mutual types should pass: " ++ prettyPosError err

	testMutualWithNegative :: Assertion
	testMutualWithNegative = do
	-- data Even = Zero \| SuccO (Odd -> Int) -- NEGATIVE!
	-- data Odd = SuccE Even
	let a = var "a"
	defs =
	[ ("Even", [a], [tyFun (tyConst "Odd" []) (tyConst "Int" [])])
	, ("Odd", [a], [tyConst "Even" []])
	]

	case checkPositivityMulti defs of
	Left _ -> return () -- Should be rejected
	Right () -> assertFailure "Mutual with negative should be rejected"

	-- ============================================================================
	-- ERROR MESSAGE TESTS
	-- ============================================================================

	testNonPositiveMessage :: Assertion
	testNonPositiveMessage = do
	let err = NonPositiveOccurrence "a" "in function domain"
	let msg = prettyPosError err
	assertBool "Error should mention type parameter" $ "a" `elem` words msg
	assertBool "Error should mention non-positive" $ "non-positive" `elem` words msg

	testFunctionDomainMessage :: Assertion
	testFunctionDomainMessage = do
	let err = TypeVarInFunctionDomain "a"
	let msg = prettyPosError err
	assertBool "Error should mention function domain" $ "domain" `elem` words msg
	assertBool "Error should mention parameter a" $ "a" `elem` words msg

	testNestedNegativeMessage :: Assertion
	testNestedNegativeMessage = do
	let err = NestedNegativeOccurrence "a" "in List (a -> Int)"
	let msg = prettyPosError err
	assertBool "Error should mention nested" $ "nested" `elem` words msg
	assertBool "Error should mention negative" $ "negative" `elem` words msg