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, ['']) + _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
