Fixup basic type-lits test.

There is still one more test that needs fixing:

   indexed-types/should_fail  T7786 [stderr mismatch] (normal)

I need to understand what is going on there, as it appears to be
using the `Sing` constructors a bunch.

2 files changed, 46 insertions, 43 deletions

diff --git a/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
index 07f2957795..78661730cc 100644
--- a/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
+++ b/testsuite/tests/typecheck/should_compile/TcTypeNatSimple.hs
@@ -1,93 +1,94 @@
 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
 module TcTypeNatSimple where
 import GHC.TypeLits
+import Data.Proxy
 
 --------------------------------------------------------------------------------
 -- Test evaluation
-e1 :: Sing (2 + 3) -> Sing 5
+e1 :: Proxy (2 + 3) -> Proxy 5
 e1 = id
 
-e2 :: Sing (2 * 3) -> Sing 6
+e2 :: Proxy (2 * 3) -> Proxy 6
 e2 = id
 
-e3 :: Sing (2 ^ 3) -> Sing 8
+e3 :: Proxy (2 ^ 3) -> Proxy 8
 e3 = id
 
-e4 :: Sing (0 + x) -> Sing x
+e4 :: Proxy (0 + x) -> Proxy x
 e4 = id
 
-e5 :: Sing (x + 0) -> Sing x
+e5 :: Proxy (x + 0) -> Proxy x
 e5 = id
 
-e6 :: Sing (x * 0) -> Sing 0
+e6 :: Proxy (x * 0) -> Proxy 0
 e6 = id
 
-e7 :: Sing (0 * x) -> Sing 0
+e7 :: Proxy (0 * x) -> Proxy 0
 e7 = id
 
-e8 :: Sing (x * 1) -> Sing x
+e8 :: Proxy (x * 1) -> Proxy x
 e8 = id
 
-e9 :: Sing (1 * x) -> Sing x
+e9 :: Proxy (1 * x) -> Proxy x
 e9 = id
 
-e10 :: Sing (x ^ 1) -> Sing x
+e10 :: Proxy (x ^ 1) -> Proxy x
 e10 = id
 
-e11 :: Sing (1 ^ x) -> Sing 1
+e11 :: Proxy (1 ^ x) -> Proxy 1
 e11 = id
 
-e12 :: Sing (x ^ 0) -> Sing 1
+e12 :: Proxy (x ^ 0) -> Proxy 1
 e12 = id
 
-e13 :: Sing (1 <=? 2) -> Sing True
+e13 :: Proxy (1 <=? 2) -> Proxy True
 e13 = id
 
-e14 :: Sing (2 <=? 1) -> Sing False
+e14 :: Proxy (2 <=? 1) -> Proxy False
 e14 = id
 
-e15 :: Sing (x <=? x) -> Sing True
+e15 :: Proxy (x <=? x) -> Proxy True
 e15 = id
 
-e16 :: Sing (0 <=? x) -> Sing True
+e16 :: Proxy (0 <=? x) -> Proxy True
 e16 = id
 
-e17 :: Sing (3 - 2) -> Sing 1
+e17 :: Proxy (3 - 2) -> Proxy 1
 e17 = id
 
-e18 :: Sing (a - 0) -> Sing a
+e18 :: Proxy (a - 0) -> Proxy a
 e18 = id
 
 --------------------------------------------------------------------------------
 -- Test interactions with inerts
 
-ti1 :: Sing (x + y) -> Sing x -> ()
+ti1 :: Proxy (x + y) -> Proxy x -> ()
 ti1 _ _ = ()
 
-ti2 :: Sing (y + x) -> Sing x -> ()
+ti2 :: Proxy (y + x) -> Proxy x -> ()
 ti2 _ _ = ()
 
-ti3 :: Sing (2 * y) -> ()
+ti3 :: Proxy (2 * y) -> ()
 ti3 _ = ()
 
-ti4 :: Sing (y * 2) -> ()
+ti4 :: Proxy (y * 2) -> ()
 ti4 _ = ()
 
-ti5 :: Sing (2 ^ y) -> ()
+ti5 :: Proxy (2 ^ y) -> ()
 ti5 _ = ()
 
-ti6 :: Sing (y ^ 2) -> ()
+ti6 :: Proxy (y ^ 2) -> ()
 ti6 _ = ()
 
 type family SomeFun (n :: Nat)
 
-ti7 :: (x <= y, y <= x) => Sing (SomeFun x) -> Sing y -> ()
+ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()
 ti7 _ _ = ()
 
-ti8 :: Sing (x - y) -> Sing x -> ()
+ti8 :: Proxy (x - y) -> Proxy x -> ()
 ti8 _ _ = ()
 
-ti9 :: Sing (y - x) -> Sing x -> ()
+ti9 :: Proxy (y - x) -> Proxy x -> ()
 ti9 _ _ = ()
 
 
diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
index 22ad315089..4098b3c667 100644
--- a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
+++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
@@ -1,32 +1,34 @@
 {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
 module Main(main) where
 import GHC.TypeLits
+import Data.Proxy
 
 --------------------------------------------------------------------------------
 -- Test top-reactions
 
-tsub :: SingI x => Sing (x + y) -> Sing y -> Sing x
-tsub _ _ = sing
+tsub :: Proxy (x + y) -> Proxy y -> Proxy x
+tsub _ _ = Proxy
 
-tdiv :: SingI x => Sing (x * y) -> Sing y -> Sing x
-tdiv _ _ = sing
+tdiv :: Proxy (x * y) -> Proxy y -> Proxy x
+tdiv _ _ = Proxy
 
-troot :: SingI x => Sing (x ^ y) -> Sing y -> Sing x
-troot _ _ = sing
+troot :: Proxy (x ^ y) -> Proxy y -> Proxy x
+troot _ _ = Proxy
 
-tlog :: SingI y => Sing (x ^ y) -> Sing x -> Sing y
-tlog _ _ = sing
+tlog :: Proxy (x ^ y) -> Proxy x -> Proxy y
+tlog _ _ = Proxy
 
-tleq :: (SingI x, (x <=? y) ~ True) => Sing y -> Sing x
-tleq _ = sing
+tleq :: ((x <=? y) ~ True) => Proxy y -> Proxy x
+tleq _ = Proxy
 
 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"
+main = print [ sh (tsub  (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
+             , sh (tdiv  (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "4"
+             , sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
+             , sh (tlog  (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
+             , sh (tleq  (Proxy :: Proxy 0))                    == "0"
              ]
-
+  where
+  sh x = show (natVal x)