summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/gadt-dim7.hs
diff options
context:
space:
mode:
Diffstat (limited to 'testsuite/tests/gadt/gadt-dim7.hs')
-rw-r--r--testsuite/tests/gadt/gadt-dim7.hs24
1 files changed, 24 insertions, 0 deletions
diff --git a/testsuite/tests/gadt/gadt-dim7.hs b/testsuite/tests/gadt/gadt-dim7.hs
new file mode 100644
index 0000000000..0ea3633fa3
--- /dev/null
+++ b/testsuite/tests/gadt/gadt-dim7.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE GADTs #-}
+
+module ShouldSucceed4 where
+
+data Z
+data S a
+
+
+data Add n m r where
+ PZero :: Add Z m m
+ PSucc :: Add n m p -> Add (S n) m (S p)
+
+
+data XList n a where
+ XNil :: XList Z a
+ XCons :: a -> XList n a -> XList (S n) a
+
+
+-- simple safe append function
+append :: (Add n m r) -> XList n a -> XList m a -> XList r a
+append PZero XNil l = l
+append (PSucc prf) (XCons x xs) l = XCons x (append prf xs l)
+
+