Test Trac #10134

3 files changed, 31 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T10134.hs b/testsuite/tests/polykinds/T10134.hs
new file mode 100644
index 0000000000..0b64625f28
--- /dev/null
+++ b/testsuite/tests/polykinds/T10134.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds, TypeOperators, ConstraintKinds, TypeFamilies, NoMonoLocalBinds, NoMonomorphismRestriction #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+
+module T10134 where
+
+import GHC.TypeLits
+import T10134a
+import Prelude
+
+type Positive n = ((n-1)+1)~n
+
+data Dummy n d = Dummy { vec :: Vec n (Vec d Bool) }
+
+nextDummy :: Positive (2*(n+d)) => Dummy n d -> Dummy n d
+nextDummy d = Dummy { vec = vec dFst }
+   where (dFst,dSnd) = nextDummy' d
+
+nextDummy' :: Positive (2*(n+d)) => Dummy n d -> ( Dummy n d, Bool )
+nextDummy' _ = undefined
diff --git a/testsuite/tests/polykinds/T10134a.hs b/testsuite/tests/polykinds/T10134a.hs
new file mode 100644
index 0000000000..0d84d56b5e
--- /dev/null
+++ b/testsuite/tests/polykinds/T10134a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T10134a where
+
+import GHC.TypeLits
+
+data Vec :: Nat -> * -> * where
+  Nil  :: Vec 0 a
+  (:>) :: a -> Vec n a -> Vec (n + 1) a
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 3c8096cbcb..55041dcc4c 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -119,3 +119,4 @@ test('T10503', normal, compile_fail, [''])
 test('T10570', normal, compile_fail, [''])
 test('T10670', normal, compile, [''])
 test('T10670a', normal, compile, [''])
+test('T10134', normal, multimod_compile, ['T10134.hs','-v0'])