{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE QuantifiedConstraints #-}

-- | This module defines the main indexed monad hierarchy and some standard
-- indexed monad combinators. This is meant to look familiar to Haskell
-- programmers. Notice how there is no indexed functor class as, thanks to
-- quantified constraints, this role is played by the Prelude's 'Functor' class.
-- Notice also how some traditional classes like 'MonadPlus' and 'Alternative'
-- are synonyms thanks to the 'Additive' type class.
module Control.Monad.Indexed
  ( -- * Indexed monad hierarchy
    Applicative (..),
    Monad (..),
    Alternative,
    MonadPlus,
    guard,
    Fail (..),
    MonadFail,
    guardF,

    -- ** Deriving-via combinators
    FromIndexed (..),

    -- * Index monad combinators

    -- ** Product of indexed gadgets
    (:*:) (..),
    fst_star,
    snd_star,

    -- ** Lift non-indexed gadgets to indexed
    IgnoreIndices (..),

    -- * Additional technical definitions
    (>>),
  )
where

import Control.Additive
import Control.Applicative qualified as Applicative
import Control.Monad qualified as Monad
import Prelude hiding (Applicative (..), Monad (..), MonadFail (..))
import Prelude qualified

class (forall i j. Functor (f i j), forall i. Prelude.Applicative (f i i)) => Applicative f where
  pure :: a -> f i i a

  (<*>) :: f i j (a -> b) -> f j k a -> f i k b
  default (<*>) :: (Monad f) => f i j (a -> b) -> f j k a -> f i k b
  f i j (a -> b)
ff <*> f j k a
aa = f i j (a -> b)
ff f i j (a -> b) -> ((a -> b) -> f j k b) -> f i k b
forall (i :: k) (j :: k) a (k :: k) b.
f i j a -> (a -> f j k b) -> f i k b
forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Monad m =>
m i j a -> (a -> m j k b) -> m i k b
>>= \a -> b
f -> f j k a
aa f j k a -> (a -> f k k b) -> f j k b
forall (i :: k) (j :: k) a (k :: k) b.
f i j a -> (a -> f j k b) -> f i k b
forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Monad m =>
m i j a -> (a -> m j k b) -> m i k b
>>= \a
a -> b -> f k k b
forall a (i :: k). a -> f i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure (a -> b
f a
a)
  infixl 4 <*>

  liftA2 :: (a -> b -> c) -> f i j a -> f j k b -> f i k c
  liftA2 a -> b -> c
f f i j a
x = f i j (b -> c) -> f j k b -> f i k c
forall (i :: k) (j :: k) a b (k :: k).
f i j (a -> b) -> f j k a -> f i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Applicative f =>
f i j (a -> b) -> f j k a -> f i k b
(<*>) ((a -> b -> c) -> f i j a -> f i j (b -> c)
forall a b. (a -> b) -> f i j a -> f i j b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b -> c
f f i j a
x)

  (*>) :: f i j a -> f j k b -> f i k b
  f i j a
a1 *> f j k b
a2 = (b -> b
forall a. a -> a
id (b -> b) -> f i j a -> f i j (b -> b)
forall a b. a -> f i j b -> f i j a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f i j a
a1) f i j (b -> b) -> f j k b -> f i k b
forall (i :: k) (j :: k) a b (k :: k).
f i j (a -> b) -> f j k a -> f i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Applicative f =>
f i j (a -> b) -> f j k a -> f i k b
<*> f j k b
a2
  infixl 4 *>

  (<*) :: f i j a -> f j k b -> f i k a
  (<*) = (a -> b -> a) -> f i j a -> f j k b -> f i k a
forall a b c (i :: k) (j :: k) (k :: k).
(a -> b -> c) -> f i j a -> f j k b -> f i k c
forall {k} (f :: k -> k -> * -> *) a b c (i :: k) (j :: k)
       (k :: k).
Applicative f =>
(a -> b -> c) -> f i j a -> f j k b -> f i k c
liftA2 a -> b -> a
forall a b. a -> b -> a
const
  infixl 4 <*

class (Applicative m, forall i. Prelude.Monad (m i i)) => Monad m where
  (>>=) :: m i j a -> (a -> m j k b) -> m i k b

-- | This class is mainly used for the qualified `do`-notation, as described in
-- the documentation for 'Prelude.MonadFail'. Occasionally used to fail with an
-- error message in monads which support it, see for instance 'guardF' below.
class Fail m where
  fail :: String -> m i j a

type MonadFail m = (Monad m, Fail m)

guardF :: (Applicative m, Fail m) => Bool -> String -> m i i ()
guardF :: forall {k} (m :: k -> k -> * -> *) (i :: k).
(Applicative m, Fail m) =>
Bool -> String -> m i i ()
guardF Bool
True String
_ = () -> m i i ()
forall a (i :: k). a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure ()
guardF Bool
False String
msg = String -> m i i ()
forall (i :: k) (j :: k) a. String -> m i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
Fail m =>
String -> m i j a
fail String
msg

type Alternative m = (Applicative m, forall r r' a. Additive (m r r' a))

guard :: (Alternative m) => Bool -> m i i ()
guard :: forall {k} (m :: k -> k -> * -> *) (i :: k).
Alternative m =>
Bool -> m i i ()
guard Bool
True = () -> m i i ()
forall a (i :: k). a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure ()
guard Bool
False = m i i ()
forall a. Additive a => a
empty

type MonadPlus m = (Monad m, forall r r' a. Additive (m r r' a))

-- | Synonym of '*>' used for `QualifiedDo` notation.
(>>) :: (Applicative m) => m i j () -> m j k a -> m i k a
>> :: forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) (k :: k) a.
Applicative m =>
m i j () -> m j k a -> m i k a
(>>) = m i j () -> m j k a -> m i k a
forall (i :: k) (j :: k) a (k :: k) b.
m i j a -> m j k b -> m i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Applicative f =>
f i j a -> f j k b -> f i k b
(*>)

data (:*:) f g i j a = (:*:) (f i j a) (g i j a)
  deriving stock ((forall a b. (a -> b) -> (:*:) f g i j a -> (:*:) f g i j b)
-> (forall a b. a -> (:*:) f g i j b -> (:*:) f g i j a)
-> Functor ((:*:) f g i j)
forall a b. a -> (:*:) f g i j b -> (:*:) f g i j a
forall a b. (a -> b) -> (:*:) f g i j a -> (:*:) f g i j b
forall k k (f :: k -> k -> * -> *) (g :: k -> k -> * -> *) (i :: k)
       (j :: k) a b.
(Functor (f i j), Functor (g i j)) =>
a -> (:*:) f g i j b -> (:*:) f g i j a
forall k k (f :: k -> k -> * -> *) (g :: k -> k -> * -> *) (i :: k)
       (j :: k) a b.
(Functor (f i j), Functor (g i j)) =>
(a -> b) -> (:*:) f g i j a -> (:*:) f g i j b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k k (f :: k -> k -> * -> *) (g :: k -> k -> * -> *) (i :: k)
       (j :: k) a b.
(Functor (f i j), Functor (g i j)) =>
(a -> b) -> (:*:) f g i j a -> (:*:) f g i j b
fmap :: forall a b. (a -> b) -> (:*:) f g i j a -> (:*:) f g i j b
$c<$ :: forall k k (f :: k -> k -> * -> *) (g :: k -> k -> * -> *) (i :: k)
       (j :: k) a b.
(Functor (f i j), Functor (g i j)) =>
a -> (:*:) f g i j b -> (:*:) f g i j a
<$ :: forall a b. a -> (:*:) f g i j b -> (:*:) f g i j a
Functor)

-- ⚠️ All the patterns on `x :*: y` must be lazy lest definitions like `many` start
-- looping because they become strict in their recursive arguments.
fst_star :: (f :*: g) i j a -> f i j a
fst_star :: forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
(:*:) f g i j a -> f i j a
fst_star ~(f i j a
x :*: g i j a
_) = f i j a
x

snd_star :: (f :*: g) i j a -> g i j a
snd_star :: forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
(:*:) f g i j a -> g i j a
snd_star ~(f i j a
_ :*: g i j a
y) = g i j a
y

instance (Prelude.Applicative (f i j), Prelude.Applicative (g i j)) => Prelude.Applicative ((f :*: g) i j) where
  pure :: forall a. a -> (:*:) f g i j a
pure a
a = (a -> f i j a
forall a. a -> f i j a
forall (f :: * -> *) a. Applicative f => a -> f a
Prelude.pure a
a) f i j a -> g i j a -> (:*:) f g i j a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (a -> g i j a
forall a. a -> g i j a
forall (f :: * -> *) a. Applicative f => a -> f a
Prelude.pure a
a)
  ~(f i j (a -> b)
f :*: g i j (a -> b)
f') <*> :: forall a b.
(:*:) f g i j (a -> b) -> (:*:) f g i j a -> (:*:) f g i j b
<*> (f i j a
a :*: g i j a
a') = (f i j (a -> b)
f f i j (a -> b) -> f i j a -> f i j b
forall a b. f i j (a -> b) -> f i j a -> f i j b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
Prelude.<*> f i j a
a) f i j b -> g i j b -> (:*:) f g i j b
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j (a -> b)
f' g i j (a -> b) -> g i j a -> g i j b
forall a b. g i j (a -> b) -> g i j a -> g i j b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
Prelude.<*> g i j a
a')

instance (Applicative f, Applicative g) => Applicative (f :*: g) where
  pure :: forall a (i :: k). a -> (:*:) f g i i a
pure a
a = (a -> f i i a
forall a (i :: k). a -> f i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure a
a) f i i a -> g i i a -> (:*:) f g i i a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (a -> g i i a
forall a (i :: k). a -> g i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure a
a)

  ~(f i j (a -> b)
f :*: g i j (a -> b)
f') <*> :: forall (i :: k) (j :: k) a b (k :: k).
(:*:) f g i j (a -> b) -> (:*:) f g j k a -> (:*:) f g i k b
<*> ~(f j k a
a :*: g j k a
a') = (f i j (a -> b)
f f i j (a -> b) -> f j k a -> f i k b
forall (i :: k) (j :: k) a b (k :: k).
f i j (a -> b) -> f j k a -> f i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Applicative f =>
f i j (a -> b) -> f j k a -> f i k b
<*> f j k a
a) f i k b -> g i k b -> (:*:) f g i k b
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j (a -> b)
f' g i j (a -> b) -> g j k a -> g i k b
forall (i :: k) (j :: k) a b (k :: k).
g i j (a -> b) -> g j k a -> g i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Applicative f =>
f i j (a -> b) -> f j k a -> f i k b
<*> g j k a
a')
  ~(f i j a
a :*: g i j a
a') *> :: forall (i :: k) (j :: k) a (k :: k) b.
(:*:) f g i j a -> (:*:) f g j k b -> (:*:) f g i k b
*> ~(f j k b
b :*: g j k b
b') = (f i j a
a f i j a -> f j k b -> f i k b
forall (i :: k) (j :: k) a (k :: k) b.
f i j a -> f j k b -> f i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Applicative f =>
f i j a -> f j k b -> f i k b
*> f j k b
b) f i k b -> g i k b -> (:*:) f g i k b
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j a
a' g i j a -> g j k b -> g i k b
forall (i :: k) (j :: k) a (k :: k) b.
g i j a -> g j k b -> g i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Applicative f =>
f i j a -> f j k b -> f i k b
*> g j k b
b')
  ~(f i j a
a :*: g i j a
a') <* :: forall (i :: k) (j :: k) a (k :: k) b.
(:*:) f g i j a -> (:*:) f g j k b -> (:*:) f g i k a
<* ~(f j k b
b :*: g j k b
b') = (f i j a
a f i j a -> f j k b -> f i k a
forall (i :: k) (j :: k) a (k :: k) b.
f i j a -> f j k b -> f i k a
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Applicative f =>
f i j a -> f j k b -> f i k a
<* f j k b
b) f i k a -> g i k a -> (:*:) f g i k a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j a
a' g i j a -> g j k b -> g i k a
forall (i :: k) (j :: k) a (k :: k) b.
g i j a -> g j k b -> g i k a
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Applicative f =>
f i j a -> f j k b -> f i k a
<* g j k b
b')

instance (Prelude.Monad (f i j), Prelude.Monad (g i j)) => Prelude.Monad ((f :*: g) i j) where
  ~(f i j a
a :*: g i j a
b) >>= :: forall a b.
(:*:) f g i j a -> (a -> (:*:) f g i j b) -> (:*:) f g i j b
>>= a -> (:*:) f g i j b
k =
    (f i j a
a f i j a -> (a -> f i j b) -> f i j b
forall a b. f i j a -> (a -> f i j b) -> f i j b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
Prelude.>>= \a
x -> let (f i j b
r :*: g i j b
_) = a -> (:*:) f g i j b
k a
x in f i j b
r)
      f i j b -> g i j b -> (:*:) f g i j b
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j a
b g i j a -> (a -> g i j b) -> g i j b
forall a b. g i j a -> (a -> g i j b) -> g i j b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
Prelude.>>= \a
y -> let (f i j b
_ :*: g i j b
s) = a -> (:*:) f g i j b
k a
y in g i j b
s)

instance (Monad f, Monad g) => Monad (f :*: g) where
  ~(f i j a
a :*: g i j a
b) >>= :: forall (i :: k) (j :: k) a (k :: k) b.
(:*:) f g i j a -> (a -> (:*:) f g j k b) -> (:*:) f g i k b
>>= a -> (:*:) f g j k b
k =
    (f i j a
a f i j a -> (a -> f j k b) -> f i k b
forall (i :: k) (j :: k) a (k :: k) b.
f i j a -> (a -> f j k b) -> f i k b
forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Monad m =>
m i j a -> (a -> m j k b) -> m i k b
>>= \a
x -> let (f j k b
r :*: g j k b
_) = a -> (:*:) f g j k b
k a
x in f j k b
r)
      f i k b -> g i k b -> (:*:) f g i k b
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j a
b g i j a -> (a -> g j k b) -> g i k b
forall (i :: k) (j :: k) a (k :: k) b.
g i j a -> (a -> g j k b) -> g i k b
forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Monad m =>
m i j a -> (a -> m j k b) -> m i k b
>>= \a
y -> let (f j k b
_ :*: g j k b
s) = a -> (:*:) f g j k b
k a
y in g j k b
s)

instance (Fail f, Fail g) => Fail (f :*: g) where
  fail :: forall (i :: k) (j :: k) (a :: k). String -> (:*:) f g i j a
fail String
msg = String -> f i j a
forall (i :: k) (j :: k) (a :: k). String -> f i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
Fail m =>
String -> m i j a
fail String
msg f i j a -> g i j a -> (:*:) f g i j a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: String -> g i j a
forall (i :: k) (j :: k) (a :: k). String -> g i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
Fail m =>
String -> m i j a
fail String
msg

instance (Applicative.Alternative (f i j), Applicative.Alternative (g i j)) => Applicative.Alternative ((f :*: g) i j) where
  empty :: forall a. (:*:) f g i j a
empty = f i j a
forall a. f i j a
forall (f :: * -> *) a. Alternative f => f a
Applicative.empty f i j a -> g i j a -> (:*:) f g i j a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: g i j a
forall a. g i j a
forall (f :: * -> *) a. Alternative f => f a
Applicative.empty
  ~(f i j a
a :*: g i j a
a') <|> :: forall a. (:*:) f g i j a -> (:*:) f g i j a -> (:*:) f g i j a
<|> ~(f i j a
b :*: g i j a
b') = (f i j a
a f i j a -> f i j a -> f i j a
forall a. f i j a -> f i j a -> f i j a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
Applicative.<|> f i j a
b) f i j a -> g i j a -> (:*:) f g i j a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g i j a
a' g i j a -> g i j a -> g i j a
forall a. g i j a -> g i j a -> g i j a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
Applicative.<|> g i j a
b')

instance (Monad.MonadPlus (f i j), Monad.MonadPlus (g i j)) => Monad.MonadPlus ((f :*: g) i j)

instance (Additive (f r r' a), Additive (g r r' a)) => Additive ((f :*: g) r r' a) where
  empty :: (:*:) f g r r' a
empty = f r r' a
forall a. Additive a => a
empty f r r' a -> g r r' a -> (:*:) f g r r' a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: g r r' a
forall a. Additive a => a
empty
  ~(f r r' a
a :*: g r r' a
a') <|> :: (:*:) f g r r' a -> (:*:) f g r r' a -> (:*:) f g r r' a
<|> ~(f r r' a
b :*: g r r' a
b') = (f r r' a
a f r r' a -> f r r' a -> f r r' a
forall a. Additive a => a -> a -> a
<|> f r r' a
b) f r r' a -> g r r' a -> (:*:) f g r r' a
forall {k} {k} {k} (f :: k -> k -> k -> *) (g :: k -> k -> k -> *)
       (i :: k) (j :: k) (a :: k).
f i j a -> g i j a -> (:*:) f g i j a
:*: (g r r' a
a' g r r' a -> g r r' a -> g r r' a
forall a. Additive a => a -> a -> a
<|> g r r' a
b')

newtype IgnoreIndices m i j a = IgnoreIndices {forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
IgnoreIndices m i j a -> m a
unIgnoreIndices :: m a}
  deriving newtype
    ( (forall a b.
 (a -> b) -> IgnoreIndices m i j a -> IgnoreIndices m i j b)
-> (forall a b.
    a -> IgnoreIndices m i j b -> IgnoreIndices m i j a)
-> Functor (IgnoreIndices m i j)
forall a b. a -> IgnoreIndices m i j b -> IgnoreIndices m i j a
forall a b.
(a -> b) -> IgnoreIndices m i j a -> IgnoreIndices m i j b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Functor m =>
a -> IgnoreIndices m i j b -> IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Functor m =>
(a -> b) -> IgnoreIndices m i j a -> IgnoreIndices m i j b
$cfmap :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Functor m =>
(a -> b) -> IgnoreIndices m i j a -> IgnoreIndices m i j b
fmap :: forall a b.
(a -> b) -> IgnoreIndices m i j a -> IgnoreIndices m i j b
$c<$ :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Functor m =>
a -> IgnoreIndices m i j b -> IgnoreIndices m i j a
<$ :: forall a b. a -> IgnoreIndices m i j b -> IgnoreIndices m i j a
Functor,
      Functor (IgnoreIndices m i j)
Functor (IgnoreIndices m i j) =>
(forall a. a -> IgnoreIndices m i j a)
-> (forall a b.
    IgnoreIndices m i j (a -> b)
    -> IgnoreIndices m i j a -> IgnoreIndices m i j b)
-> (forall a b c.
    (a -> b -> c)
    -> IgnoreIndices m i j a
    -> IgnoreIndices m i j b
    -> IgnoreIndices m i j c)
-> (forall a b.
    IgnoreIndices m i j a
    -> IgnoreIndices m i j b -> IgnoreIndices m i j b)
-> (forall a b.
    IgnoreIndices m i j a
    -> IgnoreIndices m i j b -> IgnoreIndices m i j a)
-> Applicative (IgnoreIndices m i j)
forall a. a -> IgnoreIndices m i j a
forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j a
forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
forall a b.
IgnoreIndices m i j (a -> b)
-> IgnoreIndices m i j a -> IgnoreIndices m i j b
forall a b c.
(a -> b -> c)
-> IgnoreIndices m i j a
-> IgnoreIndices m i j b
-> IgnoreIndices m i j c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *) k (i :: k) k (j :: k).
Applicative m =>
Functor (IgnoreIndices m i j)
forall (m :: * -> *) k (i :: k) k (j :: k) a.
Applicative m =>
a -> IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j (a -> b)
-> IgnoreIndices m i j a -> IgnoreIndices m i j b
forall (m :: * -> *) k (i :: k) k (j :: k) a b c.
Applicative m =>
(a -> b -> c)
-> IgnoreIndices m i j a
-> IgnoreIndices m i j b
-> IgnoreIndices m i j c
$cpure :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Applicative m =>
a -> IgnoreIndices m i j a
pure :: forall a. a -> IgnoreIndices m i j a
$c<*> :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j (a -> b)
-> IgnoreIndices m i j a -> IgnoreIndices m i j b
<*> :: forall a b.
IgnoreIndices m i j (a -> b)
-> IgnoreIndices m i j a -> IgnoreIndices m i j b
$cliftA2 :: forall (m :: * -> *) k (i :: k) k (j :: k) a b c.
Applicative m =>
(a -> b -> c)
-> IgnoreIndices m i j a
-> IgnoreIndices m i j b
-> IgnoreIndices m i j c
liftA2 :: forall a b c.
(a -> b -> c)
-> IgnoreIndices m i j a
-> IgnoreIndices m i j b
-> IgnoreIndices m i j c
$c*> :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
*> :: forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
$c<* :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Applicative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j a
<* :: forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j a
Prelude.Applicative,
      Applicative (IgnoreIndices m i j)
Applicative (IgnoreIndices m i j) =>
(forall a b.
 IgnoreIndices m i j a
 -> (a -> IgnoreIndices m i j b) -> IgnoreIndices m i j b)
-> (forall a b.
    IgnoreIndices m i j a
    -> IgnoreIndices m i j b -> IgnoreIndices m i j b)
-> (forall a. a -> IgnoreIndices m i j a)
-> Monad (IgnoreIndices m i j)
forall a. a -> IgnoreIndices m i j a
forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
forall a b.
IgnoreIndices m i j a
-> (a -> IgnoreIndices m i j b) -> IgnoreIndices m i j b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
forall (m :: * -> *) k (i :: k) k (j :: k).
Monad m =>
Applicative (IgnoreIndices m i j)
forall (m :: * -> *) k (i :: k) k (j :: k) a.
Monad m =>
a -> IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Monad m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Monad m =>
IgnoreIndices m i j a
-> (a -> IgnoreIndices m i j b) -> IgnoreIndices m i j b
$c>>= :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Monad m =>
IgnoreIndices m i j a
-> (a -> IgnoreIndices m i j b) -> IgnoreIndices m i j b
>>= :: forall a b.
IgnoreIndices m i j a
-> (a -> IgnoreIndices m i j b) -> IgnoreIndices m i j b
$c>> :: forall (m :: * -> *) k (i :: k) k (j :: k) a b.
Monad m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
>> :: forall a b.
IgnoreIndices m i j a
-> IgnoreIndices m i j b -> IgnoreIndices m i j b
$creturn :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Monad m =>
a -> IgnoreIndices m i j a
return :: forall a. a -> IgnoreIndices m i j a
Prelude.Monad,
      Applicative (IgnoreIndices m i j)
Applicative (IgnoreIndices m i j) =>
(forall a. IgnoreIndices m i j a)
-> (forall a.
    IgnoreIndices m i j a
    -> IgnoreIndices m i j a -> IgnoreIndices m i j a)
-> (forall a. IgnoreIndices m i j a -> IgnoreIndices m i j [a])
-> (forall a. IgnoreIndices m i j a -> IgnoreIndices m i j [a])
-> Alternative (IgnoreIndices m i j)
forall a. IgnoreIndices m i j a
forall a. IgnoreIndices m i j a -> IgnoreIndices m i j [a]
forall a.
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
forall (f :: * -> *).
Applicative f =>
(forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) k (i :: k) k (j :: k).
Alternative m =>
Applicative (IgnoreIndices m i j)
forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a -> IgnoreIndices m i j [a]
forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
$cempty :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a
empty :: forall a. IgnoreIndices m i j a
$c<|> :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
<|> :: forall a.
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
$csome :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a -> IgnoreIndices m i j [a]
some :: forall a. IgnoreIndices m i j a -> IgnoreIndices m i j [a]
$cmany :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
Alternative m =>
IgnoreIndices m i j a -> IgnoreIndices m i j [a]
many :: forall a. IgnoreIndices m i j a -> IgnoreIndices m i j [a]
Applicative.Alternative,
      Monad (IgnoreIndices m i j)
Alternative (IgnoreIndices m i j)
(Alternative (IgnoreIndices m i j), Monad (IgnoreIndices m i j)) =>
(forall a. IgnoreIndices m i j a)
-> (forall a.
    IgnoreIndices m i j a
    -> IgnoreIndices m i j a -> IgnoreIndices m i j a)
-> MonadPlus (IgnoreIndices m i j)
forall a. IgnoreIndices m i j a
forall a.
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
forall (m :: * -> *).
(Alternative m, Monad m) =>
(forall a. m a) -> (forall a. m a -> m a -> m a) -> MonadPlus m
forall (m :: * -> *) k (i :: k) k (j :: k).
MonadPlus m =>
Monad (IgnoreIndices m i j)
forall (m :: * -> *) k (i :: k) k (j :: k).
MonadPlus m =>
Alternative (IgnoreIndices m i j)
forall (m :: * -> *) k (i :: k) k (j :: k) a.
MonadPlus m =>
IgnoreIndices m i j a
forall (m :: * -> *) k (i :: k) k (j :: k) a.
MonadPlus m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
$cmzero :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
MonadPlus m =>
IgnoreIndices m i j a
mzero :: forall a. IgnoreIndices m i j a
$cmplus :: forall (m :: * -> *) k (i :: k) k (j :: k) a.
MonadPlus m =>
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
mplus :: forall a.
IgnoreIndices m i j a
-> IgnoreIndices m i j a -> IgnoreIndices m i j a
Monad.MonadPlus
    )

instance (Prelude.Applicative f) => Applicative (IgnoreIndices f) where
  pure :: forall a (i :: k). a -> IgnoreIndices f i i a
pure a
a = f a -> IgnoreIndices f i i a
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices (f a -> IgnoreIndices f i i a) -> f a -> IgnoreIndices f i i a
forall a b. (a -> b) -> a -> b
$ a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
Prelude.pure a
a
  IgnoreIndices f (a -> b)
f <*> :: forall (i :: k) (j :: k) a b (k :: k).
IgnoreIndices f i j (a -> b)
-> IgnoreIndices f j k a -> IgnoreIndices f i k b
<*> IgnoreIndices f a
a = f b -> IgnoreIndices f i k b
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices (f b -> IgnoreIndices f i k b) -> f b -> IgnoreIndices f i k b
forall a b. (a -> b) -> a -> b
$ f (a -> b)
f f (a -> b) -> f a -> f b
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
Prelude.<*> f a
a

instance (Prelude.Monad m) => Monad (IgnoreIndices m) where
  IgnoreIndices m a
a >>= :: forall (i :: k) (j :: k) a (k :: k) b.
IgnoreIndices m i j a
-> (a -> IgnoreIndices m j k b) -> IgnoreIndices m i k b
>>= a -> IgnoreIndices m j k b
k = m b -> IgnoreIndices m i k b
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices (m b -> IgnoreIndices m i k b) -> m b -> IgnoreIndices m i k b
forall a b. (a -> b) -> a -> b
$ m a
a m a -> (a -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
Prelude.>>= \a
x -> IgnoreIndices m j k b -> m b
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
IgnoreIndices m i j a -> m a
unIgnoreIndices (a -> IgnoreIndices m j k b
k a
x)

instance (Applicative.Alternative m) => Additive (IgnoreIndices m r r' a) where
  empty :: IgnoreIndices m r r' a
empty = m a -> IgnoreIndices m r r' a
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices m a
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
Applicative.empty
  (IgnoreIndices m a
a) <|> :: IgnoreIndices m r r' a
-> IgnoreIndices m r r' a -> IgnoreIndices m r r' a
<|> (IgnoreIndices m a
b) = m a -> IgnoreIndices m r r' a
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices (m a -> IgnoreIndices m r r' a) -> m a -> IgnoreIndices m r r' a
forall a b. (a -> b) -> a -> b
$ m a
a m a -> m a -> m a
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
Applicative.<|> m a
b

instance (Prelude.MonadFail m) => Fail (IgnoreIndices m) where
  fail :: forall (i :: k) (j :: k) a. String -> IgnoreIndices m i j a
fail String
msg = m a -> IgnoreIndices m i j a
forall {k} {k} {k} (m :: k -> *) (i :: k) (j :: k) (a :: k).
m a -> IgnoreIndices m i j a
IgnoreIndices (m a -> IgnoreIndices m i j a) -> m a -> IgnoreIndices m i j a
forall a b. (a -> b) -> a -> b
$ String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
Prelude.fail String
msg

-- | A deriving via combinator
newtype FromIndexed m i j a = FromIndexed (m i j a)
  deriving ((forall a b.
 (a -> b) -> FromIndexed m i j a -> FromIndexed m i j b)
-> (forall a b. a -> FromIndexed m i j b -> FromIndexed m i j a)
-> Functor (FromIndexed m i j)
forall a b. a -> FromIndexed m i j b -> FromIndexed m i j a
forall a b. (a -> b) -> FromIndexed m i j a -> FromIndexed m i j b
forall k k (m :: k -> k -> * -> *) (i :: k) (j :: k) a b.
Functor (m i j) =>
a -> FromIndexed m i j b -> FromIndexed m i j a
forall k k (m :: k -> k -> * -> *) (i :: k) (j :: k) a b.
Functor (m i j) =>
(a -> b) -> FromIndexed m i j a -> FromIndexed m i j b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k k (m :: k -> k -> * -> *) (i :: k) (j :: k) a b.
Functor (m i j) =>
(a -> b) -> FromIndexed m i j a -> FromIndexed m i j b
fmap :: forall a b. (a -> b) -> FromIndexed m i j a -> FromIndexed m i j b
$c<$ :: forall k k (m :: k -> k -> * -> *) (i :: k) (j :: k) a b.
Functor (m i j) =>
a -> FromIndexed m i j b -> FromIndexed m i j a
<$ :: forall a b. a -> FromIndexed m i j b -> FromIndexed m i j a
Functor)

instance (Applicative m, i ~ j) => Prelude.Applicative (FromIndexed m i j) where
  pure :: forall a. a -> FromIndexed m i j a
pure a
x = m i j a -> FromIndexed m i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
m i j a -> FromIndexed m i j a
FromIndexed (m i j a -> FromIndexed m i j a) -> m i j a -> FromIndexed m i j a
forall a b. (a -> b) -> a -> b
$ a -> m i i a
forall a (i :: k). a -> m i i a
forall {k} (f :: k -> k -> * -> *) a (i :: k).
Applicative f =>
a -> f i i a
pure a
x
  (FromIndexed m i j (a -> b)
f) <*> :: forall a b.
FromIndexed m i j (a -> b)
-> FromIndexed m i j a -> FromIndexed m i j b
<*> (FromIndexed m i j a
a) = m i j b -> FromIndexed m i j b
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
m i j a -> FromIndexed m i j a
FromIndexed (m i j b -> FromIndexed m i j b) -> m i j b -> FromIndexed m i j b
forall a b. (a -> b) -> a -> b
$ m i j (a -> b)
f m i j (a -> b) -> m j j a -> m i j b
forall (i :: k) (j :: k) a b (k :: k).
m i j (a -> b) -> m j k a -> m i k b
forall {k} (f :: k -> k -> * -> *) (i :: k) (j :: k) a b (k :: k).
Applicative f =>
f i j (a -> b) -> f j k a -> f i k b
<*> m i j a
m j j a
a

instance (Monad m, i ~ j) => Prelude.Monad (FromIndexed m i j) where
  (FromIndexed m i j a
a) >>= :: forall a b.
FromIndexed m i j a
-> (a -> FromIndexed m i j b) -> FromIndexed m i j b
>>= a -> FromIndexed m i j b
k =
    m i j b -> FromIndexed m i j b
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
m i j a -> FromIndexed m i j a
FromIndexed (m i j b -> FromIndexed m i j b) -> m i j b -> FromIndexed m i j b
forall a b. (a -> b) -> a -> b
$
      m i j a
a m i j a -> (a -> m j j b) -> m i j b
forall (i :: k) (j :: k) a (k :: k) b.
m i j a -> (a -> m j k b) -> m i k b
forall {k} (m :: k -> k -> * -> *) (i :: k) (j :: k) a (k :: k) b.
Monad m =>
m i j a -> (a -> m j k b) -> m i k b
>>= \a
x ->
        let (FromIndexed m i j b
b) = a -> FromIndexed m i j b
k a
x in m i j b
m j j b
b

instance (Alternative m, i ~ j) => Applicative.Alternative (FromIndexed m i j) where
  empty :: forall a. FromIndexed m i j a
empty = m i j a -> FromIndexed m i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
m i j a -> FromIndexed m i j a
FromIndexed m i j a
forall a. Additive a => a
empty
  (FromIndexed m i j a
a) <|> :: forall a.
FromIndexed m i j a -> FromIndexed m i j a -> FromIndexed m i j a
<|> (FromIndexed m i j a
b) = m i j a -> FromIndexed m i j a
forall {k} {k} {k} (m :: k -> k -> k -> *) (i :: k) (j :: k)
       (a :: k).
m i j a -> FromIndexed m i j a
FromIndexed (m i j a -> FromIndexed m i j a) -> m i j a -> FromIndexed m i j a
forall a b. (a -> b) -> a -> b
$ m i j a
a m i j a -> m i j a -> m i j a
forall a. Additive a => a -> a -> a
<|> m i j a
b

instance (MonadPlus m, i ~ j) => Monad.MonadPlus (FromIndexed m i j)