[commit: ghc] master: Test Trac #7908 (c34ef46)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/c34ef467429771edf0b2b18c05994c461c82df38/ghc

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

commit c34ef467429771edf0b2b18c05994c461c82df38
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Mon Dec 1 17:04:47 2014 +0000

    Test Trac #7908
    
    Fixed by e6a2050ebb6da316aecec66a6795715fbab355ca
    along with #9582, #9833


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

c34ef467429771edf0b2b18c05994c461c82df38
 testsuite/tests/polykinds/T7908.hs | 49 ++++++++++++++++++++++++++++++++++++++
 testsuite/tests/polykinds/all.T    |  2 +-
 2 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/testsuite/tests/polykinds/T7908.hs b/testsuite/tests/polykinds/T7908.hs
new file mode 100644
index 0000000..1bb4cc5
--- /dev/null
+++ b/testsuite/tests/polykinds/T7908.hs
@@ -0,0 +1,49 @@
+{-# LANGUAGE GADTs, InstanceSigs, DataKinds, PolyKinds, RankNTypes, LambdaCase #-}
+
+module T7908 where
+
+class Monad' (m :: (k -> *) -> *) where
+  return' :: c a -> m c
+  (>>>=) :: m c -> (forall a . c a -> m d) -> m d
+  (>>-) :: m c -> (forall a . c a -> d) -> d
+
+
+data Nat = Z' | S' Nat
+
+data Nat' (n :: Nat) where
+  Z :: Nat' Z'
+  S :: Nat' n -> Nat' (S' n)
+
+data Hidden :: (k -> *) -> * where
+  Hide :: m a -> Hidden m
+
+instance Monad' Hidden where
+  --return' :: forall (c :: k -> *) (a :: k) . c a -> Hidden c
+  return' = Hide
+  --(>>>=) :: forall (c :: k -> *) (d :: k -> *) . Hidden c -> (forall (a :: k) . c a -> Hidden d) -> Hidden d
+  Hide a >>>= f = f a
+  --(>>-) :: forall (c :: k -> *) d . Hidden c -> (forall (a :: k) . c a -> d) -> d
+  Hide a >>- f = f a
+
+
+int2nat' 0 = return' Z
+int2nat' i = (int2nat' $ i - 1) >>>= (\n -> return' $ S n)
+
+
+data Fin (m :: Nat)  (n :: Nat) where
+  Fz :: Fin (S' m) Z'
+  Fs :: Fin m n -> Fin (S' m) (S' n)
+
+-- N.B. not total!
+nat2fin :: Nat' f -> Hidden Nat' -> Hidden (Fin f)
+nat2fin (S _) (Hide Z) = return' Fz
+nat2fin (S f) n = n >>>= (\case S n -> (nat2fin f (return' n) >>>= (\fn -> return' $ Fs fn)))
+
+fin2int :: Hidden (Fin f) -> Int
+fin2int f = f >>- go
+  where go :: Fin f n -> Int
+        go Fz = 0
+        go (Fs f) = 1 + go f
+
+
+test = fin2int (nat2fin (S $ S Z) $ return' (S Z))
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 387e2bf..c86e317 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -113,4 +113,4 @@ test('T9569', normal, compile, [''])
 test('T9838', normal, multimod_compile, ['T9838.hs','-v0'])
 test('T9574', normal, compile_fail, [''])
 test('T9833', normal, compile, [''])
-
+test('T7908', normal, compile, [''])