Test case for #7961.
authorRichard Eisenberg <eir@cis.upenn.edu>
Sat, 12 Dec 2015 02:51:37 +0000 (21:51 -0500)
committerRichard Eisenberg <eir@cis.upenn.edu>
Sat, 12 Dec 2015 02:52:34 +0000 (21:52 -0500)
Test case: dependent/shoud_compile/TypeLevelVec

testsuite/tests/dependent/should_compile/TypeLevelVec.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/all.T

diff --git a/testsuite/tests/dependent/should_compile/TypeLevelVec.hs b/testsuite/tests/dependent/should_compile/TypeLevelVec.hs
new file mode 100644 (file)
index 0000000..19f605c
--- /dev/null
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeInType, UnicodeSyntax, GADTs, NoImplicitPrelude,
+             TypeOperators, TypeFamilies #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+module TypeLevelVec where
+
+import Data.Kind
+
+data ℕ ∷ Type where
+  O ∷ ℕ
+  S ∷ ℕ → ℕ
+
+type family x + y where
+  O   + n = n
+  S m + n = S (m + n)
+infixl 5 +
+
+data Vec ∷ ℕ → Type → Type where
+  Nil  ∷ Vec O a
+  (:>) ∷ a → Vec n a → Vec (S n) a
+infixr 8 :>
+
+type family (x ∷ Vec n a) ++ (y ∷ Vec m a) ∷ Vec (n + m) a where
+  Nil       ++ y = y
+  (x :> xs) ++ y = x :> (xs ++ y)
+infixl 5 ++
index 0f231db..1724ff6 100644 (file)
@@ -8,3 +8,4 @@ test('RAE_T32b', only_ways('normal'), compile, [''])
 test('KindLevels', normal, compile, [''])
 test('RaeBlogPost', normal, compile, [''])
 test('mkGADTVars', normal, compile, [''])
+test('TypeLevelVec',normal,compile, [''])