summaryrefslogtreecommitdiff
path: root/testsuite/tests/typecheck/should_compile/T19535.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/typecheck/should_compile/T19535.hs')
-rw-r--r--testsuite/tests/typecheck/should_compile/T19535.hs44
1 files changed, 44 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/T19535.hs b/testsuite/tests/typecheck/should_compile/T19535.hs
new file mode 100644
index 0000000000..e05b599b38
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19535.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module T19535 where
+
+import GHC.TypeNats (natVal)
+import GHC.TypeLits hiding (natVal)
+import Data.Type.Equality
+import Data.Proxy
+
+e1 :: CharToNat 'a' :~: 97
+e1 = Refl
+
+e2 :: NatToChar 120 :~: 'x'
+e2 = Refl
+
+ntc :: forall {n} c. (KnownNat n, NatToChar n ~ c) => Natural
+ntc = natVal (Proxy @n)
+
+ctn :: forall {c} n. (KnownChar c, CharToNat c ~ n) => Char
+ctn = charVal (Proxy @c)
+
+n1 :: Natural
+n1 = ntc @'z'
+
+c1 :: Char
+c1 = ctn @122
+
+ntc_ntc :: forall {n} m. (KnownNat n, NatToChar n ~ NatToChar (m + 1)) => Natural
+ntc_ntc = natVal (Proxy @n)
+
+ctn_ctn :: forall {c} d. (KnownChar c, CharToNat c ~ (CharToNat d + 1)) => Char
+ctn_ctn = charVal (Proxy @c)
+
+n2 :: Natural
+n2 = ntc_ntc @119
+
+c2 :: Char
+c2 = ctn_ctn @'w'