{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
{-# OPTIONS_GHC -dcore-lint #-}
module Main where
-- base
import Data.Maybe
( mapMaybe )
import Data.Kind
( Constraint, Type )
import System.Exit
( exitFailure, exitSuccess )
#if MIN_VERSION_ghc(9,3,0)
import GHC.Exts
( withDict )
#endif
-- IfSat
import Data.Constraint.If
( IfSat(ifSat), IsSat )
--------------------------------------------------------------------------------
type BoolI :: Bool -> Constraint
class BoolI b where
boolI :: Bool
instance BoolI True where
boolI = True
instance BoolI False where
boolI = False
type MyShow :: Type -> Constraint
class MyShow a where
myShow :: a -> String
instance MyShow Int where
myShow = show
myShowAnything :: forall a. IfSat ( MyShow a ) => a -> String
myShowAnything = ifSat @( MyShow a ) yes no
where
yes :: MyShow a => a -> String
yes = myShow
no :: a -> String
no _ = "<<no MyShow instance>>"
-- Should use the "MyShow Int" instance.
test1 :: String
test1 = myShowAnything ( 123 :: Int )
test1b :: Bool
test1b = boolI @( IsSat ( MyShow Int ) )
-- No "MyShow ( Int -> Int -> Int )" instance.
test2 :: String
test2 = myShowAnything ( (+) :: Int -> Int -> Int )
test2b :: Bool
test2b = boolI @( IsSat ( MyShow ( Int -> Int -> Int ) ) )
data A = A
myShowA :: IfSat ( MyShow A ) => String
myShowA = myShowAnything A
#if MIN_VERSION_ghc(9,3,0)
-- Should use the instance locally provided by "withDict".
test3 :: String
test3 =
withDict @( A -> String ) @( MyShow A )
( \ _ -> "A" )
myShowA
test3b :: Bool
test3b =
withDict @( A -> String ) @( MyShow A )
( \ _ -> "A" )
( boolI @( IsSat ( MyShow A ) ) )
#endif
-- No "MyShow A" instance.
test4 :: String
test4 = myShowA
test4b :: Bool
test4b = boolI @( IsSat ( MyShow A ) )
--------------------------------------------------------------------------------
data Test where
Test
:: ( Show a, Eq a )
=> { testName :: String
, testActual :: a
, testExpected :: a
}
-> Test
runTest :: Test -> Maybe String
runTest ( Test { testName, testActual, testExpected } )
| testActual == testExpected
= Nothing
| otherwise
= Just $
"\n" <>
"Test '" <> testName <> "' failed.\n" <>
"Expected: " <> show testExpected <> "\n" <>
" Actual: " <> show testActual
tests :: [ Test ]
tests =
[ Test "test1" test1 "123"
, Test "test1b" test1b True
, Test "test2" test2 "<<no MyShow instance>>"
, Test "test2b" test2b False
#if MIN_VERSION_ghc(9,3,0)
, Test "test3" test3 "A"
, Test "test3b" test3b True
#endif
, Test "test4" test4 "<<no MyShow instance>>"
, Test "test4b" test4b False
]
main :: IO ()
main = do
let
results :: [ String ]
results = mapMaybe runTest tests
case results of
[] -> exitSuccess
_ -> putStrLn ( unlines results ) *> exitFailure