[commit: testsuite] master: Test Trac #5591 (3aeae5f)

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

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/3aeae5f746e31a1e3f7541e9ee96fcd2cfc4af58

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

commit 3aeae5f746e31a1e3f7541e9ee96fcd2cfc4af58
Author: Simon Peyton Jones <[email protected]>
Date:   Tue Oct 2 16:32:54 2012 +0100

    Test Trac #5591

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

 tests/indexed-types/should_compile/T5591a.hs |   25 +++++++++++++++++++++++++
 tests/indexed-types/should_compile/T5591b.hs |   12 ++++++++++++
 tests/indexed-types/should_compile/all.T     |    3 +++
 3 files changed, 40 insertions(+), 0 deletions(-)

diff --git a/tests/indexed-types/should_compile/T5591a.hs b/tests/indexed-types/should_compile/T5591a.hs
new file mode 100644
index 0000000..9c1a2c7
--- /dev/null
+++ b/tests/indexed-types/should_compile/T5591a.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE GADTs, TypeOperators, TypeFamilies, ScopedTypeVariables #-}
+module T5591a where
+
+data a :=: b where 
+    Refl :: a :=: a
+
+subst :: a :=: b -> f a -> f b
+subst Refl = id 
+
+-- Then this doesn't work (error message at the bottom):
+
+inj1 :: forall f a b. f a :=: f b -> a :=: b
+inj1 Refl = Refl
+
+-- But one can still construct it with a trick that Oleg used in the context of 
+-- Leibniz equality:
+
+type family Arg fa
+
+type instance Arg (f a) = a
+
+newtype Helper fa fa' = Helper { runHelper :: Arg fa :=: Arg fa' }
+
+inj2 :: forall f a b. f a :=: f b -> a :=: b
+inj2 p = runHelper (subst p (Helper Refl :: Helper (f a) (f a)))
diff --git a/tests/indexed-types/should_compile/T5591b.hs b/tests/indexed-types/should_compile/T5591b.hs
new file mode 100644
index 0000000..20f4225
--- /dev/null
+++ b/tests/indexed-types/should_compile/T5591b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, 
+    GADTs, FlexibleInstances, FlexibleContexts #-}
+module T5591b where
+
+class Monad m => Effect p e r m | p e m -> r where
+  fin :: p e m -> e -> m r
+
+data ErrorEff :: * -> (* -> *) -> * where 
+  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m
+
+instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
+  fin (CatchError h) = \f -> f h
diff --git a/tests/indexed-types/should_compile/all.T b/tests/indexed-types/should_compile/all.T
index 9cdb7e5..b005962 100644
--- a/tests/indexed-types/should_compile/all.T
+++ b/tests/indexed-types/should_compile/all.T
@@ -197,4 +197,7 @@ test('T6152',
 test('T6088', normal, compile, [''])
 test('T7082', normal, compile, [''])
 test('T7156', normal, compile, [''])
+test('T5591a', normal, compile, [''])
+test('T5591b', normal, compile, [''])
+