Test Trac #7294

3 files changed, 35 insertions, 0 deletions

diff --git a/testsuite/tests/gadt/T7294.hs b/testsuite/tests/gadt/T7294.hs
new file mode 100644
index 0000000000..1c39a2a574
--- /dev/null
+++ b/testsuite/tests/gadt/T7294.hs
@@ -0,0 +1,25 @@
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+{-# 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/T7294.stderr b/testsuite/tests/gadt/T7294.stderr
new file mode 100644
index 0000000000..dc1eef1ca9
--- /dev/null
+++ b/testsuite/tests/gadt/T7294.stderr
@@ -0,0 +1,9 @@
+
+T7294.hs:25:5: Warning:
+    Couldn't match type 'False with 'True
+    Inaccessible code in
+      a pattern with constructor
+        Nil :: forall a. Vec a 'Zero,
+      in an equation for `nth'
+    In the pattern: Nil
+    In an equation for `nth': nth Nil _ = undefined
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 566afcbf5e..f28e28d96c 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -115,3 +115,4 @@ test('T5424',
 test('FloatEq', normal, compile, [''])
 test('T7205', normal, compile, [''])
 test('T7293', normal, compile_fail, [''])
+test('T7294', normal, compile, [''])