testsuite: Assert that testsuite ways are known
[ghc.git] / testsuite / tests / typecheck / should_compile / TcTypeNatSimple.hs
1 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
2 module TcTypeNatSimple where
3 import GHC.TypeLits as L
4 import Data.Proxy
5
6 --------------------------------------------------------------------------------
7 -- Test evaluation
8 e1 :: Proxy (2 + 3) -> Proxy 5
9 e1 = id
10
11 e2 :: Proxy (2 L.* 3) -> Proxy 6
12 e2 = id
13
14 e3 :: Proxy (2 ^ 3) -> Proxy 8
15 e3 = id
16
17 e4 :: Proxy (0 + x) -> Proxy x
18 e4 = id
19
20 e5 :: Proxy (x + 0) -> Proxy x
21 e5 = id
22
23 e6 :: Proxy (x L.* 0) -> Proxy 0
24 e6 = id
25
26 e7 :: Proxy (0 L.* x) -> Proxy 0
27 e7 = id
28
29 e8 :: Proxy (x L.* 1) -> Proxy x
30 e8 = id
31
32 e9 :: Proxy (1 L.* x) -> Proxy x
33 e9 = id
34
35 e10 :: Proxy (x ^ 1) -> Proxy x
36 e10 = id
37
38 e11 :: Proxy (1 ^ x) -> Proxy 1
39 e11 = id
40
41 e12 :: Proxy (x ^ 0) -> Proxy 1
42 e12 = id
43
44 e13 :: Proxy (1 <=? 2) -> Proxy True
45 e13 = id
46
47 e14 :: Proxy (2 <=? 1) -> Proxy False
48 e14 = id
49
50 e15 :: Proxy (x <=? x) -> Proxy True
51 e15 = id
52
53 e16 :: Proxy (0 <=? x) -> Proxy True
54 e16 = id
55
56 e17 :: Proxy (3 - 2) -> Proxy 1
57 e17 = id
58
59 e18 :: Proxy (a - 0) -> Proxy a
60 e18 = id
61
62 e19 :: Proxy (Div 10 3) -> Proxy 3
63 e19 = id
64
65 e20 :: Proxy (Div x 1) -> Proxy x
66 e20 = id
67
68 e21 :: Proxy (Mod 10 3) -> Proxy 1
69 e21 = id
70
71 e22 :: Proxy (Mod x 1) -> Proxy 0
72 e22 = id
73
74 e23 :: Proxy (Log2 10) -> Proxy 3
75 e23 = id
76
77 --------------------------------------------------------------------------------
78 -- Test interactions with inerts
79
80 -- ti1 :: Proxy (x + y) -> Proxy x -> ()
81 -- ti1 _ _ = ()
82
83 ti2 :: Proxy (y + x) -> Proxy x -> ()
84 ti2 _ _ = ()
85
86 ti3 :: Proxy (2 L.* y) -> ()
87 ti3 _ = ()
88
89 ti4 :: Proxy (y L.* 2) -> ()
90 ti4 _ = ()
91
92 ti5 :: Proxy (2 ^ y) -> ()
93 ti5 _ = ()
94
95 ti6 :: Proxy (y ^ 2) -> ()
96 ti6 _ = ()
97
98 ti8 :: Proxy (x - y) -> Proxy x -> ()
99 ti8 _ _ = ()
100
101 ti9 :: Proxy (y - x) -> Proxy x -> ()
102 ti9 _ _ = ()