diff options
5 files changed, 116 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs new file mode 100644 index 0000000000..e30656a0fc --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-} +module TcTypeNatSimple where +import GHC.TypeLits + +-------------------------------------------------------------------------------- +-- Test evaluation +e1 :: Sing (2 + 3) -> Sing 5 +e1 = id + +e2 :: Sing (2 * 3) -> Sing 6 +e2 = id + +e3 :: Sing (2 ^ 3) -> Sing 8 +e3 = id + +e4 :: Sing (0 + x) -> Sing x +e4 = id + +e5 :: Sing (x + 0) -> Sing x +e5 = id + +e6 :: Sing (x * 0) -> Sing 0 +e6 = id + +e7 :: Sing (0 * x) -> Sing 0 +e7 = id + +e8 :: Sing (x * 1) -> Sing x +e8 = id + +e9 :: Sing (1 * x) -> Sing x +e9 = id + +e10 :: Sing (x ^ 1) -> Sing x +e10 = id + +e11 :: Sing (1 ^ x) -> Sing 1 +e11 = id + +e12 :: Sing (x ^ 0) -> Sing 1 +e12 = id + +e13 :: Sing (1 <=? 2) -> Sing True +e13 = id + +e14 :: Sing (2 <=? 1) -> Sing False +e14 = id + +e15 :: Sing (x <=? x) -> Sing True +e15 = id + +e16 :: Sing (0 <=? x) -> Sing True +e16 = id + +-------------------------------------------------------------------------------- +-- Test interactions with inerts + +ti1 :: Sing (x + y) -> Sing x -> () +ti1 _ _ = () + +ti2 :: Sing (y + x) -> Sing x -> () +ti2 _ _ = () + +ti3 :: Sing (2 * y) -> () +ti3 _ = () + +ti4 :: Sing (y * 2) -> () +ti4 _ = () + +ti5 :: Sing (2 ^ y) -> () +ti5 _ = () + +ti6 :: Sing (y ^ 2) -> () +ti6 _ = () + +type family SomeFun (n :: Nat) + +ti7 :: (x <= y, y <= x) => Sing (SomeFun x) -> Sing y -> () +ti7 _ _ = () + + diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index e28e597eee..f2880710aa 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -408,3 +408,4 @@ test('T7268', normal, compile, ['']) test('T7888', normal, compile, ['']) test('T7891', normal, compile, ['']) test('T7903', normal, compile, ['']) +test('TcTypeNatSimple', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs new file mode 100644 index 0000000000..22ad315089 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-} +module Main(main) where +import GHC.TypeLits + +-------------------------------------------------------------------------------- +-- Test top-reactions + +tsub :: SingI x => Sing (x + y) -> Sing y -> Sing x +tsub _ _ = sing + +tdiv :: SingI x => Sing (x * y) -> Sing y -> Sing x +tdiv _ _ = sing + +troot :: SingI x => Sing (x ^ y) -> Sing y -> Sing x +troot _ _ = sing + +tlog :: SingI y => Sing (x ^ y) -> Sing x -> Sing y +tlog _ _ = sing + +tleq :: (SingI x, (x <=? y) ~ True) => Sing y -> Sing x +tleq _ = sing + +main :: IO () +main = print [ show (tsub (sing :: Sing 5) (sing :: Sing 3)) == "2" + , show (tdiv (sing :: Sing 8) (sing :: Sing 2)) == "4" + , show (troot (sing :: Sing 9) (sing :: Sing 2)) == "3" + , show (tlog (sing :: Sing 8) (sing :: Sing 2)) == "3" + , show (tleq (sing :: Sing 0)) == "0" + ] + + + diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout new file mode 100644 index 0000000000..9adb27b5bc --- /dev/null +++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout @@ -0,0 +1 @@ +[True,True,True,True,True] diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T index 1d714a2757..b566c33f70 100755 --- a/testsuite/tests/typecheck/should_run/all.T +++ b/testsuite/tests/typecheck/should_run/all.T @@ -110,3 +110,4 @@ test('T5913', normal, compile_and_run, ['']) test('T7748', normal, compile_and_run, ['']) test('TcNullaryTC', when(compiler_lt('ghc', '7.7'), skip), compile_and_run, ['']) test('T7861', exit_code(1), compile_and_run, ['']) +test('TcTypeNatSimpleRun', normal, compile_and_run, ['']) |