{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE MagicHash        #-}

module Main where

import Data.Elevator.Internal
import Test.Hspec
import Control.Exception (evaluate, SomeException (SomeException))
import GHC.Exts

main :: IO ()
main = hspec $ do
  describe "Strict" $ do
    it "strict" $ do
      evaluate
        (let a = Strict (error "boom" :: Int)
             konst :: a -> Strict b -> a
             konst x y = x
        in konst 42 a)
        `shouldThrow` \(SomeException e) -> True

  describe "Lazy" $ do
    it "lazy" $ do
      (let a = Lazy (error "boom" :: Array# Int)
           konst :: a -> Lazy b -> a
           konst x y = x
       in konst 42 a)
      `shouldBe` 42

  describe "levCoerce" $ do
    describe "Refl" $ do
      it "Int ~ Int" $ do
        levCoerce @Int @Int 42 `shouldBe` (42 :: Int)
      it "Strict Int ~ Strict Int" $ do
        case levCoerce# @_ @_ @(Strict Int) @(Strict Int) (Strict 42) of Strict x -> x  `shouldBe` (42 :: Int)
    describe "->" $ do
      it "even" $ do
        levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42) `shouldBe` True
      it "co,contra: Int -> Strict Int ~ Int -> Strict Int" $ do
        levCoerce @(Int -> Strict Int) @(Strict Int -> Int) (\x -> Strict (x+1)) (Strict 42) `shouldBe` (43 :: Int)
      it "rank2 co: (Int -> Int) -> Int ~ (Strict Int -> Int) -> Int" $ do
        levCoerce @((Strict Int -> Int) -> Int) @((Int -> Strict Int) -> Int) (\f -> f (Strict 42)) (\x -> Strict x) `shouldBe` (42 :: Int)