{-# LANGUAGE CPP #-}
{-# LANGUAGE QuasiQuotes #-}

module ShouldError (tests) where

import Data.String.Interpolate (i)
import ShouldError.Tasty (assertCompileError)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)

tests :: TestTree
tests = testGroup "ShouldError"
    [ test1
    , test2
    , test3
    , test4
    , test5
    , test6
    , test7
    , test8
    , test9
    , test10
    , test11
    , testIssue126
    , inequalityTests
    ]

preamble :: String
preamble = [i|
import Data.Kind (Constraint)
import Data.Proxy
import GHC.TypeLits
|] <> "\n"

source1 :: String
source1 = preamble <> [i|
test :: Proxy (x + 1) -> Proxy (2 + x)
test = id
|]

expected1 :: [String]
expected1 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy (2 + x)"
  ,"  Actual: Proxy (x + 1)"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy (x + 1) -> Proxy (2 + x)"
  ,"  Actual: Proxy (x + 1) -> Proxy (x + 1)"
  ]
#else
  ["Expected type: Proxy (x + 1) -> Proxy (2 + x)"
  ,"Actual type: Proxy (2 + x) -> Proxy (2 + x)"
  ]
#endif

test1 :: TestTree
test1 = testCase "x + 1 /~ 2 + x" $ assertCompileError source1 expected1

source2 :: String
source2 = preamble <> [i|
type family GCD (x :: Nat) (y :: Nat) :: Nat
type instance GCD 6 8 = 2
type instance GCD 9 6 = 3

test :: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)
test = id
|]

expected2 :: [String]
expected2 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy (x + GCD 9 6)"
  ,"  Actual: Proxy (2 + x)"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
  ,"  Actual: Proxy (2 + x) -> Proxy (2 + x)"
  ]
#else
  ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"
  ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"
  ]
#endif

test2 :: TestTree
test2 = testCase "GCD 6 8 + x /~ x + GCD 9 6" $ assertCompileError source2 expected2

source3 :: String
source3 = preamble <> [i|
proxyFun :: Proxy (x + x + x) -> ()
proxyFun = const ()

test :: Proxy 8 -> ()
test = proxyFun
|]

expected3 :: [String]
expected3 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy ((x0 + x0) + x0)"
  ,"  Actual: Proxy 8"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy 8 -> ()"
  ,"  Actual: Proxy ((x0 + x0) + x0) -> ()"
  ]
#else
  ["Expected type: Proxy 8 -> ()"
  ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"
  ]
#endif

test3 :: TestTree
test3 = testCase "Unify \"x + x + x\" with \"8\"" $ assertCompileError source3 expected3

source4 :: String
source4 = preamble <> [i|
proxyFun :: Proxy ((2*y)+4) -> ()
proxyFun = const ()

test :: Proxy 2 -> ()
test = proxyFun
|]

expected4 :: [String]
expected4 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy ((2 * y0) + 4)"
  ,"  Actual: Proxy 2"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy 2 -> ()"
  ,"  Actual: Proxy ((2 * y0) + 4) -> ()"
  ]
#else
  ["Expected type: Proxy 2 -> ()"
  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"
  ]
#endif

test4 :: TestTree
test4 = testCase "Unify \"(2*x)+4\" with \"2\"" $ assertCompileError source4 expected4

source5 :: String
source5 = preamble <> [i|
proxyFun :: Proxy ((2*y)+4) -> ()
proxyFun = const ()

test :: Proxy 7 -> ()
test = proxyFun
|]

expected5 :: [String]
expected5 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy ((2 * y"
  ,"Actual: Proxy 7"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy 7 -> ()"
  ,"Actual: Proxy ((2 * y"
  ]
#else
  ["Expected type: Proxy 7 -> ()"
  ,"Actual type: Proxy ((2 * y"
  ]
#endif

test5 :: TestTree
test5 = testCase "Unify \"(2*x)+4\" with \"7\"" $ assertCompileError source5 expected5

source6 :: String
source6 = preamble <> [i|
proxyFun :: Proxy (2^k) -> Proxy (2^k)
proxyFun = const Proxy

test :: Proxy 7
test = proxyFun (Proxy :: Proxy 7)
|]

expected6 :: [String]
expected6 =
#if __GLASGOW_HASKELL__ >= 902
  ["Expected: Proxy 7"
  ,"  Actual: Proxy (2 ^ k0)"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy (2 ^ k0)"
  ,"  Actual: Proxy 7"
  ]
#else
  ["Expected type: Proxy (2 ^ k0)"
  ,"Actual type: Proxy 7"
  ]
#endif

test6 :: TestTree
test6 = testCase "Unify \"2^k\" with \"7\"" $ assertCompileError source6 expected6

source7 :: String
source7 = preamble <> [i|
test :: Proxy x -> Proxy (y + x)
test = id
|]

expected7 :: [String]
expected7 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy (y + x)"
  ,"  Actual: Proxy x"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy x -> Proxy (y + x)"
  ,"  Actual: Proxy x -> Proxy x"
  ]
#else
  ["Expected type: Proxy x -> Proxy (y + x)"
  ,"Actual type: Proxy x -> Proxy x"
  ]
#endif

test7 :: TestTree
test7 = testCase "x /~ y + x" $ assertCompileError source7 expected7

source8 :: String
source8 = preamble <> [i|
type family CLog (b :: Nat) (x :: Nat) :: Nat
type instance CLog 2 2 = 1

test :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)
test = id
|]

expected8 :: [String]
expected8 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy (n + d)"
  ,"  Actual: Proxy n"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy n -> Proxy (n + d)"
  ,"  Actual: Proxy n -> Proxy n"
  ]
#else
  ["Expected type: Proxy n -> Proxy (n + d)"
  ,"Actual type: Proxy n -> Proxy n"
  ]
#endif

test8 :: TestTree
test8 = testCase "(CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => n /~ n + d" $
  assertCompileError source8 expected8

source9 :: String
source9 = preamble <> [i|
data Fin (n :: Nat) where
  FZ :: Fin (n + 1)
  FS :: Fin n -> Fin (n + 1)

test :: forall n . Integer -> Fin n
test n = case n of
  0 -> FZ
  x -> FS (test @(n-1) (x-1))
|]

expected9 :: [String]
expected9 =
#if __GLASGOW_HASKELL__ >= 904
  ["Cannot satisfy: 1 <= n"]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Couldn't match type Data.Type.Ord.OrdCond"
  , "(CmpNat 1 n) True True False"
  , "with True"
  ]
#else
  [ "Couldn't match type 1 <=? n with True" ]
#endif

test9 :: TestTree
test9 = testCase "(n - 1) + 1 ~ n implies (1 <= n)" $ assertCompileError source9 expected9

source10 :: String
source10 = preamble <> [i|
type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where
  Drop 0 xs = xs
  Drop n (x ': xs) = Drop (n-1) xs
  Drop n '[] = '[]

test :: Proxy ns -> Proxy (Drop 1 ns) -> Proxy (Drop 2 ns)
test _ px = px
|]

expected10 :: [String]
expected10 =
#if __GLASGOW_HASKELL__ >= 811
  [ "Couldn't match type: Drop 1 ns"
  , "               with: Drop 2 ns"
  , "Expected: Proxy (Drop 2 ns)"
  , "  Actual: Proxy (Drop 1 ns)"
  , "Drop is a non-injective type family"
  ]
#else
  [ "Couldn't match type Drop 1 ns with Drop 2 ns"
  , "Expected type: Proxy (Drop 2 ns)"
  , "  Actual type: Proxy (Drop 1 ns)"
  , "Drop is a non-injective type family"
  ]
#endif

test10 :: TestTree
test10 = testCase "Do not unify in non-injective positions" $ assertCompileError source10 expected10

source11 :: String
source11 = preamble <> [i|
test :: Proxy a -> Proxy b -> Proxy ((2 * a) + b) -> Proxy 5
test _ _ = id
|]

expected11 :: [String]
expected11 =
#if __GLASGOW_HASKELL__ >= 914
  ["Expected: Proxy 5"
  ,"  Actual: Proxy ((2 * a) + b)"
  ]
#elif __GLASGOW_HASKELL__ >= 900
  ["Expected: Proxy ((2 * a) + b) -> Proxy 5"
  ,"  Actual: Proxy 5 -> Proxy 5"
  ]
#else
  ["Expected type: Proxy ((2 * a) + b) -> Proxy 5"
  ,"Actual type: Proxy 5 -> Proxy 5"
  ]
#endif

test11 :: TestTree
test11 = testCase "Do not rewrite constraint to itself" $ assertCompileError source11 expected11

-- ((3 * (n - 1)) + 1) simplifies to (3 * n - 2), so
-- the equality would require b0 ~ -2, which is impossible at kind Nat.
sourceIssue126 :: String
sourceIssue126 = preamble <> [i|
data Index (n :: Nat) = Index

truncateB :: Index (a + b) -> Index a
truncateB = undefined

mul :: Index 4 -> Index n -> Index ((3 * (n - 1)) + 1)
mul _ _ = Index

zeroExtendTimesThree :: (1 <= n) => Index n -> Index (n * 3)
zeroExtendTimesThree = truncateB . (mul Index)
|]

expectedIssue126 :: [String]
expectedIssue126 =
#if __GLASGOW_HASKELL__ >= 906
  [ "Could not deduce ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"
#elif __GLASGOW_HASKELL__ >= 904
  [ "Could not deduce (((n * 3) + b0) ~ ((3 * (n - 1)) + 1))"
#elif __GLASGOW_HASKELL__ >= 902
  [ "Could not deduce: ((n * 3) + b0) ~ ((3 * (n - 1)) + 1)"
#else
  [ "Could not deduce: ((3 * (n - 1)) + 1) ~ ((n * 3) + b0)"
#endif
  , "from the context: 1 <= n"
  ]



testIssue126 :: TestTree
testIssue126 =
  testCase "Issue 126 regression reproducer" $
    assertCompileError sourceIssue126 expectedIssue126

proxyInEqDef :: String
proxyInEqDef =
#if __GLASGOW_HASKELL__ >= 904
  [i|
proxyInEq :: ((a <= b) ~ (() :: Constraint)) => Proxy (a :: Nat) -> Proxy b -> ()
proxyInEq _ _ = ()
|]
#else
  [i|
proxyInEq :: (a <= b) => Proxy (a :: Nat) -> Proxy b -> ()
proxyInEq _ _ = ()
|]
#endif

proxyInEq'Def :: String
proxyInEq'Def = [i|
proxyInEq' :: ((a <=? b) ~ 'False) => Proxy (a :: Nat) -> Proxy b -> ()
proxyInEq' _ _ = ()
|]

source12 :: String
source12 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (a + 1) -> Proxy a -> ()
test = proxyInEq
|]

expected12 :: [String]
expected12 =
#if __GLASGOW_HASKELL__ >= 904
  ["Cannot satisfy: a + 1 <= a"]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Couldn't match type Data.Type.Ord.OrdCond"
  , "(CmpNat (a + 1) a) True True False"
  , "with True"
  ]
#else
  [ "Couldn't match type (a + 1) <=? a with True" ]
#endif

test12 :: TestTree
test12 = testCase "a+1 <= a" $ assertCompileError source12 expected12

source13 :: String
source13 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (a :: Nat) -> Proxy (a + 2) -> ()
test = proxyInEq'
|]

expected13 :: [String]
expected13 =
#if __GLASGOW_HASKELL__ >= 902
  [ "Data.Type.Ord.OrdCond"
  , "(CmpNat a (a + 2)) True True False"
  , "with False"
  ]
#else
  [ "Couldn't match type a <=? (a + 2) with False" ]
#endif

test13 :: TestTree
test13 = testCase "(a <=? a+1) ~ False" $ assertCompileError source13 expected13

source14 :: String
source14 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (a :: Nat) -> Proxy a -> ()
test = proxyInEq'
|]

expected14 :: [String]
expected14 = [ "Couldn't match type True with False" ]

test14 :: TestTree
test14 = testCase "(a <=? a) ~ False" $ assertCompileError source14 expected14

source15 :: String
source15 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (a + b) -> Proxy (a + c) -> ()
test = proxyInEq
|]

expected15 :: [String]
expected15 =
#if __GLASGOW_HASKELL__ >= 904
  ["Cannot satisfy: a + b <= a + c"]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Couldn't match type Data.Type.Ord.OrdCond"
  , "(CmpNat (a + b) (a + c)) True True False"
  , "with True"
  ]
#else
  [ "Couldn't match type (a + b) <=? (a + c) with True" ]
#endif

test15 :: TestTree
test15 = testCase "() => (a+b <= a+c)" $ assertCompileError source15 expected15

source16 :: String
source16 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (4*a) -> Proxy (2*a) -> ()
test = proxyInEq
|]

expected16 :: [String]
expected16 =
#if __GLASGOW_HASKELL__ >= 904
  ["Cannot satisfy: 4 * a <= 2 * a"]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Couldn't match type Data.Type.Ord.OrdCond"
  , "(CmpNat (4 * a) (2 * a)) True True False"
  , "with True"
  ]
#else
  [ "Couldn't match type (4 * a) <=? (2 * a) with True" ]
#endif

test16 :: TestTree
test16 = testCase "4a <= 2a" $ assertCompileError source16 expected16

source17 :: String
source17 = preamble <> proxyInEqDef <> proxyInEq'Def <> [i|
test :: Proxy (2*a) -> Proxy (4*a) -> ()
test = proxyInEq'
|]

expected17 :: [String]
expected17 =
#if __GLASGOW_HASKELL__ >= 902
  [ "Data.Type.Ord.OrdCond"
  , "(CmpNat (2 * a) (4 * a)) True True False"
  , "with False"
  ]
#else
  [ "Couldn't match type (2 * a) <=? (4 * a) with False" ]
#endif

test17 :: TestTree
test17 = testCase "2a <=? 4a ~ False" $ assertCompileError source17 expected17

source18 :: String
source18 = preamble <> [i|
data Boo (n :: Nat) = Boo

test :: Show (Boo n) => Proxy n -> Boo (n - 1 + 1) -> String
test = const show
|]

expected18 :: [String]
expected18 = expected9

test18 :: TestTree
test18 = testCase "Show (Boo n) => Show (Boo (n - 1 + 1))" $ assertCompileError source18 expected18

test19fDef :: String
test19fDef =
#if __GLASGOW_HASKELL__ >= 904
  [i|
test19f :: ((1 <= n) ~ (() :: Constraint)) => Proxy n -> Proxy n
test19f = id
|]
#else
  [i|
test19f :: (1 <= n) => Proxy n -> Proxy n
test19f = id
|]
#endif

source19 :: String
source19 = preamble <> test19fDef <> [i|
test :: (1 <= m, m <= rp) => Proxy m -> Proxy rp -> Proxy (rp - m) -> Proxy (rp - m)
test _ _ = test19f
|]

expected19 :: [String]
expected19 =
#if __GLASGOW_HASKELL__ >= 904
  [ "Cannot satisfy: 1 <= rp - m" ]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Could not deduce: Data.Type.Ord.OrdCond"
  , "(CmpNat 1 (rp - m)) True True False"
  , "~ True"
  ]
#else
  [ "Could not deduce: (1 <=? (rp - m)) ~ True" ]
#endif

test19 :: TestTree
test19 = testCase "1 <= m, m <= rp implies 1 <= rp - m" $ assertCompileError source19 expected19

source20 :: String
source20 = preamble <> proxyInEqDef <> [i|
test :: Proxy 1 -> Proxy (m ^ 2) -> ()
test = proxyInEq
|]

expected20 :: [String]
expected20 =
#if __GLASGOW_HASKELL__ >= 904
  ["Cannot satisfy: 1 <= m ^ 2"]
#elif __GLASGOW_HASKELL__ >= 902
  [ "Couldn't match type Data.Type.Ord.OrdCond"
  , "(CmpNat 1 (m ^ 2)) True True False"
  , "with True"
  ]
#else
  [ "Couldn't match type 1 <=? (m ^ 2) with True" ]
#endif

test20 :: TestTree
test20 = testCase "Vacuously: 1 <= m ^ 2 ~ True" $ assertCompileError source20 expected20

inequalityTests :: TestTree
inequalityTests = testGroup "Inequality"
  [ test12
  , test13
  , test14
  , test15
  , test16
  , test17
  , test18
  , test19
  , test20
  ]