Commit 31894278 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test Trac #5591

parent c99f3054
{-# 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)))
{-# 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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment