Test Trac #7294

1 files changed, 25 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