git.iko.soy/typeable/ether
on master help sign in
Separate tag uniqueness constraint
commitdabd6598c91c3bdcd8cacecac2deeeaaf7a7af3c authorIndex Int <vlad.z.4096@gmail.com> dateTue 9 Jun 2015, 22:09 (11 years ago) parentd7cb7cd
3 files changed+28−10
compare with master
unifiedsplit
src/Control/Ether/Core.hs+8−4 src/Control/Monad/Ether/Reader.hs+3−6 test/Regression.hs+17
src/Control/Ether/Core.hs+8−4
@@ -5,8 +5,9 @@
55{-# LANGUAGE TypeOperators #-}
66{-# LANGUAGE UndecidableInstances #-}
77module Control.Ether.Core
8− ( EtherTagset
9− , EtherTags
8+ ( EtherTags
9+ , UniqueEtherTags
10+ , ensureUniqueEtherTags
1011 ) where
1112
1213import Data.Proxy (Proxy)
@@ -37,8 +38,11 @@ type family Unique (as :: [k]) :: Constraint where
3738 Unique '[] = ()
3839 Unique (a ': as) = (Elem a as ~ 'False, Unique as)
3940
40−type family EtherTagset (m :: * -> *) :: Constraint where
41− EtherTagset m = Unique (EtherTags m)
41+type family UniqueEtherTags (m :: * -> *) :: Constraint where
42+ UniqueEtherTags m = Unique (EtherTags m)
43+
44+ensureUniqueEtherTags :: UniqueEtherTags m => m a -> m a
45+ensureUniqueEtherTags = id
4246
4347type family EtherTags (m :: * -> *) :: [*]
4448
src/Control/Monad/Ether/Reader.hs+3−6
@@ -34,7 +34,6 @@ module Control.Monad.Ether.Reader
3434import Data.Proxy (Proxy(Proxy))
3535import Control.Monad.Trans (lift)
3636
37−import Control.Ether.Core
3837import Control.Monad.Trans.Ether.Reader
3938
4039-- for mtl instances
@@ -49,7 +48,7 @@ import qualified Control.Monad.Trans.State.Strict as Trans.Strict (StateT , m
4948import qualified Control.Monad.Trans.Writer.Lazy as Trans.Lazy (WriterT , mapWriterT)
5049import qualified Control.Monad.Trans.Writer.Strict as Trans.Strict (WriterT , mapWriterT)
5150
52−class (Monad m, EtherTagset m) => MonadEtherReader tag r m | m tag -> r where
51+class Monad m => MonadEtherReader tag r m | m tag -> r where
5352
5453 etherLocal :: proxy tag -> (r -> r) -> m a -> m a
5554
@@ -70,13 +69,11 @@ ask' = etherAsk (Proxy :: Proxy r)
7069reader' :: forall m r a . MonadReader' r m => (r -> a) -> m a
7170reader' = etherReader (Proxy :: Proxy r)
7271
73−instance {-# OVERLAPPING #-} (Monad m, EtherTagset (EtherReaderT tag r m))
74− => MonadEtherReader tag r (EtherReaderT tag r m) where
72+instance {-# OVERLAPPING #-} Monad m => MonadEtherReader tag r (EtherReaderT tag r m) where
7573 etherAsk proxy = etherReaderT proxy return
7674 etherLocal proxy f m = etherReaderT proxy (runEtherReaderT proxy m . f)
7775
78−instance (MonadEtherReader tag r m, EtherTagset (EtherReaderT tag' r' m))
79− => MonadEtherReader tag r (EtherReaderT tag' r' m) where
76+instance (MonadEtherReader tag r m) => MonadEtherReader tag r (EtherReaderT tag' r' m) where
8077 etherAsk proxy = lift (etherAsk proxy)
8178 etherLocal proxy = mapEtherReaderT Proxy . etherLocal proxy
8279
test/Regression.hs+17
@@ -75,3 +75,20 @@ inferCore = local' (succ :: Int -> Int) $ do
7575
7676wrapCore :: MonadEtherReader TagReader1 Int m => m Int
7777wrapCore = ethered r1 ask
78+
79+
80+-- Should not compile with `ensureUniqueEtherTags`
81+uniqueTagsCore :: IO ()
82+uniqueTagsCore = flip runReader1T (1 :: Int)
83+ . flip runReader1T (True :: Bool)
84+ . flip runReader1T (2 :: Int)
85+ . flip runReader1T (3 :: Integer)
86+ {- . ensureUniqueEtherTags -}
87+ $ do
88+ a :: Integer <- askReader1
89+ b :: Int <- askReader1
90+ c :: Bool <- askReader1
91+ liftIO $ do
92+ print a
93+ print b
94+ print c