Test Trac #10134
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 3 Aug 2015 12:39:56 +0000 (13:39 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 3 Aug 2015 12:41:58 +0000 (13:41 +0100)
testsuite/tests/polykinds/T10134.hs [new file with mode: 0644]
testsuite/tests/polykinds/T10134a.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T

diff --git a/testsuite/tests/polykinds/T10134.hs b/testsuite/tests/polykinds/T10134.hs
new file mode 100644 (file)
index 0000000..0b64625
--- /dev/null
@@ -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 (file)
index 0000000..0d84d56
--- /dev/null
@@ -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
index 3c8096c..55041dc 100644 (file)
@@ -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'])