Test Trac #7293

3 files changed, 26 insertions, 0 deletions

diff --git a/testsuite/tests/gadt/T7293.hs b/testsuite/tests/gadt/T7293.hs
new file mode 100644
index 0000000000..26d9188f81
--- /dev/null
+++ b/testsuite/tests/gadt/T7293.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
+             TypeOperators, RankNTypes #-}
+
+module T7294 where
+
+data Nat = Zero | Succ Nat
+
+data Vec :: * -> Nat -> * where
+  Nil :: Vec a Zero
+  Cons :: a -> Vec a n -> Vec a (Succ n)
+
+type family (m :: Nat) :< (n :: Nat) :: Bool
+type instance m :< Zero = False
+type instance Zero :< Succ n = True
+type instance Succ n :< Succ m = n :< m
+
+data SNat :: Nat -> * where
+  SZero :: SNat Zero
+  SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
+
+nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
+nth (Cons x _) SZero = x
+nth (Cons _ xs) (SSucc k) = nth xs k
+nth Nil _ = undefined
diff --git a/testsuite/tests/gadt/T7293.stderr b/testsuite/tests/gadt/T7293.stderr
new file mode 100644
index 0000000000..0519ecba6e
--- /dev/null
+++ b/testsuite/tests/gadt/T7293.stderr
@@ -0,0 +1 @@
+ 
\ No newline at end of file
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index ac560219a5..566afcbf5e 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -114,3 +114,4 @@ test('T5424',
 
 test('FloatEq', normal, compile, [''])
 test('T7205', normal, compile, [''])
+test('T7293', normal, compile_fail, [''])