From 6b7ca8809af3aaf5c041d0fb67d4fc9d442762a0 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Fri, 5 Oct 2012 16:37:22 +0100 Subject: Test Trac #7294 --- testsuite/tests/gadt/T7294.hs | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 testsuite/tests/gadt/T7294.hs (limited to 'testsuite/tests/gadt/T7294.hs') 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 -- cgit v1.2.1