Testsuite error message changes
[ghc.git] / testsuite / tests / typecheck / should_compile / TcTypeNatSimple.hs
1 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
2 module TcTypeNatSimple where
3 import GHC.TypeLits
4 import Data.Proxy
5
6 --------------------------------------------------------------------------------
7 -- Test evaluation
8 e1 :: Proxy (2 + 3) -> Proxy 5
9 e1 = id
10
11 e2 :: Proxy (2 * 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 * 0) -> Proxy 0
24 e6 = id
25
26 e7 :: Proxy (0 * x) -> Proxy 0
27 e7 = id
28
29 e8 :: Proxy (x * 1) -> Proxy x
30 e8 = id
31
32 e9 :: Proxy (1 * 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 --------------------------------------------------------------------------------
63 -- Test interactions with inerts
64
65 -- ti1 :: Proxy (x + y) -> Proxy x -> ()
66 -- ti1 _ _ = ()
67
68 ti2 :: Proxy (y + x) -> Proxy x -> ()
69 ti2 _ _ = ()
70
71 ti3 :: Proxy (2 * y) -> ()
72 ti3 _ = ()
73
74 ti4 :: Proxy (y * 2) -> ()
75 ti4 _ = ()
76
77 ti5 :: Proxy (2 ^ y) -> ()
78 ti5 _ = ()
79
80 ti6 :: Proxy (y ^ 2) -> ()
81 ti6 _ = ()
82
83 ti8 :: Proxy (x - y) -> Proxy x -> ()
84 ti8 _ _ = ()
85
86 ti9 :: Proxy (y - x) -> Proxy x -> ()
87 ti9 _ _ = ()