[commit: testsuite] master: Test Trac #7967 (6432ecf)

[Simon Peyton Jones]

Repository : ssh://darcs.haskell.org//srv/darcs/testsuite

On branch  : master

https://github.com/ghc/testsuite/commit/6432ecf0ca638c2c0a346ecb0ad3b3a39a2b264f

>---------------------------------------------------------------

commit 6432ecf0ca638c2c0a346ecb0ad3b3a39a2b264f
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Wed Jun 12 12:03:27 2013 +0100

    Test Trac #7967

>---------------------------------------------------------------

 tests/indexed-types/should_fail/T7967.hs     |   31 ++++++++++++++++++++++++++
 tests/indexed-types/should_fail/T7967.stderr |    7 ++++++
 tests/indexed-types/should_fail/all.T        |    1 +
 3 files changed, 39 insertions(+), 0 deletions(-)

diff --git a/tests/indexed-types/should_fail/T7967.hs b/tests/indexed-types/should_fail/T7967.hs
new file mode 100644
index 0000000..093f133
--- /dev/null
+++ b/tests/indexed-types/should_fail/T7967.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}
+module T7967 where
+
+data Nat = Zero | Succ Nat
+
+data SNat :: Nat -> * where
+  SZero :: SNat Zero
+  SSucc :: SNat n -> SNat (Succ n)
+
+data HList :: [*] -> * where
+  HNil :: HList '[]
+  HCons :: h -> HList t -> HList (h ': t)
+
+data Index :: Nat -> [*] -> * where
+  IZero :: Index Zero (h ': t)
+  ISucc :: Index n l -> Index (Succ n) (h ': l)
+
+type family Lookup (n :: Nat) (l :: [*]) :: *
+type instance Lookup Zero (h ': t) = h
+type instance Lookup (Succ n) (h ': t) = Lookup n t
+
+hLookup :: Index n l -> HList l -> Lookup n l
+hLookup IZero (HCons h _) = h
+hLookup (ISucc n) (HCons _ t) = hLookup n t
+hLookup _ _ = undefined
+
+-- So far, so good. But, I wanted a way to convert `SNat`s to `Index`es. When
+-- I add the (wrong) code below, and got a bogus error above
+
+sNatToIndex :: SNat n -> HList l -> Index n l
+sNatToIndex SZero HNil = IZero
diff --git a/tests/indexed-types/should_fail/T7967.stderr b/tests/indexed-types/should_fail/T7967.stderr
new file mode 100644
index 0000000..57560fe
--- /dev/null
+++ b/tests/indexed-types/should_fail/T7967.stderr
@@ -0,0 +1,7 @@
+
+T7967.hs:31:26:
+    Couldn't match type ‛'[] *’ with ‛(':) * h0 t0’
+    Expected type: Index n l
+      Actual type: Index 'Zero ((':) * h0 t0)
+    In the expression: IZero
+    In an equation for ‛sNatToIndex’: sNatToIndex SZero HNil = IZero
diff --git a/tests/indexed-types/should_fail/all.T b/tests/indexed-types/should_fail/all.T
index 1ef4329..da6d4a1 100644
--- a/tests/indexed-types/should_fail/all.T
+++ b/tests/indexed-types/should_fail/all.T
@@ -98,3 +98,4 @@ test('T7560', normal, compile_fail, [''])
 test('T7729', normal, compile_fail, [''])
 test('T7729a', normal, compile_fail, [''])
 test('T7786', normal, compile_fail, [''])
+test('T7967', normal, compile_fail, [''])