Membership proof rewrite, membership testing, compose effect

polysemy-plugin/src/Polysemy/Plugin/Fundep.hs

@@ -76,7 +76,7 @@ data FindConstraint = FindConstraint
 -- | Given a list of constraints, filter out the 'FindConstraint's.
 getFindConstraints :: PolysemyStuff 'Things -> [Ct] -> [FindConstraint]
 getFindConstraints (findClass -> cls) cts = do
-  cd@CDictCan{cc_class = cls', cc_tyargs = [_, r, eff]} <- cts
+  cd@CDictCan{cc_class = cls', cc_tyargs = [_, eff, r]} <- cts
   guard $ cls == cls'
   pure $ FindConstraint
     { fcLoc = ctLoc cd
@@ -163,7 +163,7 @@ extractRowFromSem (semTyCon -> sem) ty = do
 
 ------------------------------------------------------------------------------
 -- | Given a list of bogus @r@s, and the wanted constraints, produce bogus
--- evidence terms that will prevent @IfStuck (IndexOf r _) _ _@ error messsages.
+-- evidence terms that will prevent @IfStuck (LocateEffect _ r) _ _@ error messsages.
 solveBogusError :: PolysemyStuff 'Things -> [Ct] -> [(EvTerm, Ct)]
 solveBogusError stuff wanteds = do
   let splitTyConApp_list = maybeToList  . splitTyConApp_maybe
@@ -172,8 +172,8 @@ solveBogusError stuff wanteds = do
   ct@(CIrredCan ce _) <- wanteds
   (stuck, [_, _, expr, _, _]) <- splitTyConApp_list $ ctev_pred ce
   guard $ stuck == ifStuckTyCon stuff
-  (idx, [_, r, _]) <- splitTyConApp_list expr
-  guard $ idx == indexOfTyCon stuff
+  (idx, [_, _, r]) <- splitTyConApp_list expr
+  guard $ idx == locateEffectTyCon stuff
   guard $ elem @[] (OrdType r) $ coerce bogus
   pure (error "bogus proof for stuck type family", ct)
 

polysemy-plugin/src/Polysemy/Plugin/Fundep/Stuff.hs

@@ -23,21 +23,21 @@ import Outputable (pprPanic, empty, text, (<+>), ($$))
 -- When @l ~ 'Locations@, each of these is just a pair of strings. When @l
 -- ~ 'Things@, it's actually references to the stuff.
 data PolysemyStuff (l :: LookupState) = PolysemyStuff
-  { findClass    :: ThingOf l Class
-  , semTyCon     :: ThingOf l TyCon
-  , ifStuckTyCon :: ThingOf l TyCon
-  , indexOfTyCon :: ThingOf l TyCon
+  { findClass         :: ThingOf l Class
+  , semTyCon          :: ThingOf l TyCon
+  , ifStuckTyCon      :: ThingOf l TyCon
+  , locateEffectTyCon :: ThingOf l TyCon
   }
 
 
 ------------------------------------------------------------------------------
 -- | All of the things we need to lookup.
 polysemyStuffLocations :: PolysemyStuff 'Locations
 polysemyStuffLocations = PolysemyStuff
-  { findClass    = ("Polysemy.Internal.Union",                  "Find")
-  , semTyCon     = ("Polysemy.Internal",                        "Sem")
-  , ifStuckTyCon = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
-  , indexOfTyCon = ("Polysemy.Internal.Union",                  "IndexOf")
+  { findClass         = ("Polysemy.Internal.Union",                  "Find")
+  , semTyCon          = ("Polysemy.Internal",                        "Sem")
+  , ifStuckTyCon      = ("Polysemy.Internal.CustomErrors.Redefined", "IfStuck")
+  , locateEffectTyCon = ("Polysemy.Internal.Union",                  "LocateEffect")
   }
 
 

polysemy.cabal

@@ -4,7 +4,7 @@ cabal-version: 1.24
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: aac2227e71e3a98458fa5746be7fcbb87da0dc342cdd53913041c95c128871fe
+-- hash: 582807c5d69a34a9e991a77c6111532c05dbb54a5d7aa6662267b7af2d3047ee
 
 name:           polysemy
 version:        1.2.3.0
@@ -48,6 +48,7 @@ library
       Polysemy
       Polysemy.Async
       Polysemy.AtomicState
+      Polysemy.Bundle
       Polysemy.Embed
       Polysemy.Embed.Type
       Polysemy.Error
@@ -57,6 +58,7 @@ library
       Polysemy.Fixpoint
       Polysemy.Input
       Polysemy.Internal
+      Polysemy.Internal.Bundle
       Polysemy.Internal.Combinators
       Polysemy.Internal.CustomErrors
       Polysemy.Internal.CustomErrors.Redefined
@@ -72,6 +74,7 @@ library
       Polysemy.Internal.Writer
       Polysemy.IO
       Polysemy.Law
+      Polysemy.Membership
       Polysemy.NonDet
       Polysemy.Output
       Polysemy.Reader
@@ -134,6 +137,7 @@ test-suite polysemy-test
       HigherOrderSpec
       InspectorSpec
       InterceptSpec
+      KnownRowSpec
       LawsSpec
       OutputSpec
       ThEffectSpec

src/Polysemy/Bundle.hs

@@ -0,0 +1,71 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Polysemy.Bundle
+  ( -- * Effect
+    Bundle (..)
+    -- * Actions
+  , sendBundle
+  , injBundle
+    -- * Interpretations
+  , runBundle
+  , subsumeBundle
+    -- * Miscellaneous
+  , KnownList
+  ) where
+
+import Polysemy
+import Polysemy.Internal
+import Polysemy.Internal.Bundle
+import Polysemy.Internal.Union
+
+------------------------------------------------------------------------------
+-- | An effect for collecting multiple effects into one effect.
+--
+-- Useful for effect newtypes.
+data Bundle r m a where
+  Bundle :: ElemOf e r -> e m a -> Bundle r m a
+
+------------------------------------------------------------------------------
+-- | Injects an effect into a 'Bundle'. Useful together with 'transform'.
+injBundle :: forall e r m a. Member e r => e m a -> Bundle r m a
+injBundle = Bundle membership
+{-# INLINE injBundle #-}
+
+------------------------------------------------------------------------------
+-- | Send uses of an effect to a 'Bundle' containing that effect.
+sendBundle
+  :: forall e r' r a
+   . (Member e r', Member (Bundle r') r)
+  => Sem (e ': r) a
+  -> Sem r a
+sendBundle = hoistSem $ \u -> case decomp u of
+  Right (Weaving e s wv ex ins) ->
+    injWeaving $
+      Weaving (Bundle (membership @e @r') e) s (sendBundle @e @r' . wv) ex ins
+  Left g -> hoist (sendBundle @e @r') g
+{-# INLINE sendBundle #-}
+
+------------------------------------------------------------------------------
+-- | Run a @'Bundle' r@ by prepending @r@ to the effect stack.
+runBundle
+  :: forall r' r a
+   . KnownList r'
+  => Sem (Bundle r' ': r) a
+  -> Sem (Append r' r) a
+runBundle = hoistSem $ \u -> hoist runBundle $ case decomp u of
+  Right (Weaving (Bundle pr e) s wv ex ins) ->
+    Union (extendMembership @_ @r pr) $ Weaving e s wv ex ins
+  Left g -> weakenList @r' @r g
+{-# INLINE runBundle #-}
+
+------------------------------------------------------------------------------
+-- | Run a @'Bundle' r@ if the effect stack contains all effects of @r@.
+subsumeBundle
+  :: forall r' r a
+   . Members r' r
+  => Sem (Bundle r' ': r) a
+  -> Sem r a
+subsumeBundle = hoistSem $ \u -> hoist subsumeBundle $ case decomp u of
+  Right (Weaving (Bundle pr e) s wv ex ins) ->
+    Union (subsumeMembership pr) (Weaving e s wv ex ins)
+  Left g -> g
+{-# INLINE subsumeBundle #-}

src/Polysemy/Internal.hs

@@ -20,6 +20,9 @@ module Polysemy.Internal
   , raiseUnder2
   , raiseUnder3
   , subsume
+  , subsumeUsing
+  , expose
+  , exposeUsing
   , Embed (..)
   , usingSem
   , liftSem
@@ -36,6 +39,7 @@ import Control.Monad.Fix
 import Control.Monad.IO.Class
 import Data.Functor.Identity
 import Data.Kind
+import Data.Typeable
 import Polysemy.Embed.Type
 import Polysemy.Fail.Type
 import Polysemy.Internal.Fixpoint
@@ -351,8 +355,8 @@ raiseUnder :: ∀ e2 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': r) a
 raiseUnder = hoistSem $ hoist raiseUnder . weakenUnder
   where
     weakenUnder :: ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': r) m x
-    weakenUnder (Union SZ a) = Union SZ a
-    weakenUnder (Union (SS n) a) = Union (SS (SS n)) a
+    weakenUnder (Union Here a) = Union Here a
+    weakenUnder (Union (There n) a) = Union (There (There n)) a
     {-# INLINE weakenUnder #-}
 {-# INLINE raiseUnder #-}
 
@@ -366,23 +370,23 @@ raiseUnder2 :: ∀ e2 e3 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': r) a
 raiseUnder2 = hoistSem $ hoist raiseUnder2 . weakenUnder2
   where
     weakenUnder2 ::  ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': r) m x
-    weakenUnder2 (Union SZ a) = Union SZ a
-    weakenUnder2 (Union (SS n) a) = Union (SS (SS (SS n))) a
+    weakenUnder2 (Union Here a) = Union Here a
+    weakenUnder2 (Union (There n) a) = Union (There (There (There n))) a
     {-# INLINE weakenUnder2 #-}
 {-# INLINE raiseUnder2 #-}
 
 
 ------------------------------------------------------------------------------
--- | Like 'raise', but introduces two new effects underneath the head of the
+-- | Like 'raise', but introduces three new effects underneath the head of the
 -- list.
 --
 -- @since 1.2.0.0
 raiseUnder3 :: ∀ e2 e3 e4 e1 r a. Sem (e1 ': r) a -> Sem (e1 ': e2 ': e3 ': e4 ': r) a
 raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
   where
     weakenUnder3 ::  ∀ m x. Union (e1 ': r) m x -> Union (e1 ': e2 ': e3 ': e4 ': r) m x
-    weakenUnder3 (Union SZ a) = Union SZ a
-    weakenUnder3 (Union (SS n) a) = Union (SS (SS (SS (SS n)))) a
+    weakenUnder3 (Union Here a) = Union Here a
+    weakenUnder3 (Union (There n) a) = Union (There (There (There (There n)))) a
     {-# INLINE weakenUnder3 #-}
 {-# INLINE raiseUnder3 #-}
 
@@ -396,11 +400,72 @@ raiseUnder3 = hoistSem $ hoist raiseUnder3 . weakenUnder3
 --
 -- @since 1.2.0.0
 subsume :: Member e r => Sem (e ': r) a -> Sem r a
-subsume = hoistSem $ \u -> hoist subsume $ case decomp u of
-  Right w -> injWeaving w
-  Left  g -> g
+subsume = subsumeUsing membership
 {-# INLINE subsume #-}
 
+------------------------------------------------------------------------------
+-- | Interprets an effect in terms of another identical effect, given an
+-- explicit proof that the effect exists in @r@.
+--
+-- This is useful in conjunction with 'Polysemy.Internal.Union.tryMembership'.
+--
+-- @since TODO
+subsumeUsing :: forall e r a. ElemOf e r -> Sem (e ': r) a -> Sem r a
+subsumeUsing pr =
+  let
+    go :: forall x. Sem (e ': r) x -> Sem r x
+    go = hoistSem $ \u -> hoist go $ case decomp u of
+      Right w -> Union pr w
+      Left  g -> g
+    {-# INLINE go #-}
+  in
+    go
+{-# INLINE subsumeUsing #-}
+
+------------------------------------------------------------------------------
+-- | Moves all uses of an effect @e@ within the argument computation
+-- to a new @e@ placed on top of the effect stack. Note that this does not
+-- consume the inner @e@.
+--
+-- This can be used to replicate 'intercept'\/'interceptH':
+--
+-- @
+-- interceptH k = interpretH k . expose
+-- @
+--
+-- Typically, there's little reason to use 'expose' instead of
+-- 'intercept'\/'interceptH'. It's only offered for symmetry:
+-- 'subsume'\/'subsumeUsing' and 'expose'\/'exposeUsing'.
+--
+-- @since TODO
+expose :: Member e r => Sem r a -> Sem (e ': r) a
+expose = exposeUsing membership
+{-# INLINE expose #-}
+
+------------------------------------------------------------------------------
+-- | Given an explicit proof that @e@ exists in @r@, moves all uses of @e@
+-- within the argument computation to a new @e@ placed on top of the effect
+-- stack. Note that this does not consume the inner @e@.
+--
+-- This is useful in conjunction with 'Polysemy.Internal.Union.tryMembership'
+-- and 'interpret'\/'interpretH' in order to conditionally perform
+-- 'intercept'-like operations.
+--
+-- @since TODO
+exposeUsing :: forall e r a. ElemOf e r -> Sem r a -> Sem (e ': r) a
+exposeUsing pr =
+  let
+    go :: forall x. Sem r x -> Sem (e ': r) x
+    go = hoistSem $ \(Union pr' wav) -> hoist go $
+      case sameMember pr pr' of
+      Just Refl -> Union Here wav
+      _         -> Union (There pr') wav
+    {-# INLINE go #-}
+  in
+    go
+{-# INLINE exposeUsing #-}
+
+
 ------------------------------------------------------------------------------
 -- | Embed an effect into a 'Sem'. This is used primarily via
 -- 'Polysemy.makeSem' to implement smart constructors.

src/Polysemy/Internal/Bundle.hs

@@ -0,0 +1,52 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Polysemy.Internal.Bundle where
+
+import Data.Proxy
+import Polysemy
+import Polysemy.Internal.Union
+
+type family Append l r where
+  Append (a ': l) r = a ': (Append l r)
+  Append '[] r = r
+
+extendMembership :: forall r r' e. ElemOf e r -> ElemOf e (Append r r')
+extendMembership Here = Here
+extendMembership (There e) = There (extendMembership @_ @r' e)
+{-# INLINE extendMembership #-}
+
+subsumeMembership :: forall r r' e. Members r r' => ElemOf e r -> ElemOf e r'
+subsumeMembership Here = membership @e @r'
+subsumeMembership (There (pr :: ElemOf e r'')) = subsumeMembership @r'' @r' pr
+{-# INLINE subsumeMembership #-}
+
+weakenList :: forall r' r m a
+            . KnownList r'
+           => Union r m a
+           -> Union (Append r' r) m a
+weakenList u = unconsKnownList @_ @r' u (\_ (_ :: Proxy r'') -> weaken (weakenList @r'' u))
+{-# INLINE weakenList #-}
+
+
+------------------------------------------------------------------------------
+-- | A class for type-level lists with a known spine.
+--
+-- This constraint is eventually satisfied as @r@ is instantied to a
+-- concrete list.
+class KnownList (l :: [k]) where
+  unconsKnownList :: (l ~ '[] => a)
+                  -> (  forall x r
+                      . (l ~ (x ': r), KnownList r)
+                     => Proxy x
+                     -> Proxy r
+                     -> a
+                     )
+                  -> a
+
+instance KnownList '[] where
+  unconsKnownList b _ = b
+  {-# INLINE unconsKnownList #-}
+
+instance KnownList r => KnownList (x ': r) where
+  unconsKnownList _ b = b Proxy Proxy
+  {-# INLINE unconsKnownList #-}
+

src/Polysemy/Internal/CustomErrors.hs

@@ -76,7 +76,7 @@ type AmbigousEffectMessage (rstate :: EffectRowCtor)
   % "    " <> PrettyPrintList vs <> " directly, or activate polysemy-plugin which"
   % "      can usually infer the type correctly."
 
-type AmbiguousSend r e =
+type AmbiguousSend e r =
       (IfStuck r
         (AmbiguousSendError 'TyVarR r e)
         (Pure (AmbiguousSendError (UnstuckRState r) r e)))