1 files changed, 29 insertions, 0 deletions
diff --git a/testsuite/tests/indexed-types/should_compile/Numerals.hs b/testsuite/tests/indexed-types/should_compile/Numerals.hs
new file mode 100644
index 0000000000..17fb30c3ca
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Numerals.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Numerals
+where
+
+data Z          -- empty data type
+data S a        -- empty data type
+
+data SNat n where  -- natural numbers as singleton type
+  Zero :: SNat Z
+  Succ :: SNat n -> SNat (S n)
+
+zero  = Zero
+one   = Succ zero
+two   = Succ one
+three = Succ two
+-- etc...we really would like some nicer syntax here
+
+type family (:+:) n m :: *
+type instance Z     :+: m = m
+type instance (S n) :+: m = S (n :+: m)
+
+add :: SNat n -> SNat m -> SNat (n :+: m)
+add Zero     m = m
+add (Succ n) m = Succ (add n m)
+