Experience reports using indexed monads in production?

Question

In a previous question I discovered the existence of Conor McBride's Kleisli arrows of Outrageous Fortune while looking for ways of encoding Idris examples in Haskell. My efforts to understand McBride's code and make it compile in Haskell led to this gist: https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f

While searching on Hackage, I discovered several implementations of these concepts, notably by (guess who?) Edward Kmett and Gabriel Gonzalez.

What experience do people have putting such code in production? In particular, do the expected benefits (runtime safety, self-guiding usage) actually occur IRL? How about maintaining this kind of code over time and onboarding newcomers?

EDIT: I changed the title to be more explicit about what I am looking for: Real-world use of indexed monads in the wild. I am interested in using them and I have several use-cases in mind, just wondering if other people have already used them in "production" code.

EDIT 2: Thanks to the great answers provided so far and helpful comments, I edited that question's title and description again to reflect more precisely what kind of answer I expect, e.g. experience report.

Answer 1

I think the below should count as a practical example: statically enforcing "well-stackedness" in a compiler. Boilerplate first:

{-# LANGUAGE GADTs, KindSignatures #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE RebindableSyntax #-}

import qualified Prelude
import Prelude hiding (return, fail, (>>=), (>>))

Then a simple stack language:

data Op (i :: [*]) (j :: [*]) where
    IMM :: a -> Op i (a ': i)
    BINOP :: (a -> b -> c) -> Op (a ': b ': i) (c ': i)
    BRANCH :: Label i j -> Label i j -> Op (Bool ': i) j

and we won't bother with real Labels:

data Label (i :: [*]) (j :: [*]) where
    Label :: Prog i j -> Label i j

and Programs are just type-aligned lists of Ops:

data Prog (i :: [*]) (j :: [*]) where
    PNil :: Prog i i
    PCons :: Op i j -> Prog j k -> Prog i k

So in this setting, we can very easily make a compiler which is an indexed writer monad; that is, an indexed monad:

class IMonad (m :: idx -> idx -> * -> *) where
    ireturn :: a -> m i i a
    ibind :: m i j a -> (a -> m j k b) -> m i k b

-- For RebindableSyntax, so that we get that sweet 'do' sugar
return :: (IMonad m) => a -> m i i a
return = ireturn
(>>=) :: (IMonad m) => m i j a -> (a -> m j k b) -> m i k b
(>>=) = ibind
m >> n = m >>= const n
fail = error

that allows accumulating a(n indexed) monoid:

class IMonoid (m :: idx -> idx -> *) where
    imempty :: m i i
    imappend :: m i j -> m j k -> m i k

just like regular Writer:

newtype IWriter w (i :: [*]) (j :: [*]) (a :: *) = IWriter{ runIWriter :: (w i j, a) }

instance (IMonoid w) => IMonad (IWriter w) where
    ireturn x = IWriter (imempty, x)
    ibind m f = IWriter $ case runIWriter m of
        (w, x) -> case runIWriter (f x) of
            (w', y) -> (w `imappend` w', y)

itell :: w i j -> IWriter w i j ()
itell w = IWriter (w, ())

So we just apply this machinery to Programs:

instance IMonoid Prog where
    imempty = PNil
    imappend PNil prog' = prog'
    imappend (PCons op prog) prog' = PCons op $ imappend prog prog'

type Compiler = IWriter Prog

tellOp :: Op i j -> Compiler i j ()
tellOp op = itell $ PCons op PNil

label :: Compiler i j () -> Compiler k k (Label i j)
label m = case runIWriter m of
    (prog, ()) -> ireturn (Label prog)

and then we can try compiling a simple expression language:

data Expr a where
    Lit :: a -> Expr a
    And :: Expr Bool -> Expr Bool -> Expr Bool
    Plus :: Expr Int -> Expr Int -> Expr Int
    If :: Expr Bool -> Expr a -> Expr a -> Expr a

compile :: Expr a -> Compiler i (a ': i) ()
compile (Lit x) = tellOp $ IMM x
compile (And x y) = do
    compile x
    compile y
    tellOp $ BINOP (&&)
compile (Plus x y) = do
    compile x
    compile y
    tellOp $ BINOP (+)
compile (If b t e) = do
    labThen <- label $ compile t
    labElse <- label $ compile e
    compile b
    tellOp $ BRANCH labThen labElse

and if we omitted e.g. one of the arguments to BINOP, the typechecker will detect this:

compile (And x y) = do
    compile x
    tellOp $ BINOP (&&)

• Could not deduce: i ~ (Bool : i) from the context: a ~ Bool