lift for compose using ConstraintKinds

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
{-# LANGUAGE ConstraintKinds, GADTs, MultiParamTypeClasses, PolyKinds, FlexibleContexts, FlexibleInstances, ScopedTypeVariables #-}

data Dict c where
  Dict :: c => Dict c

class MapsTo c d t where
  dict :: Dict (c x) -> Dict (d (t x))

newtype Compose f g m a = Compose { decompose :: f (g m) a }

instance forall f g m. (MapsTo Monad Monad f, MapsTo Monad Monad g, Monad m) => Monad (Compose f g m) where
  return = case dict (dict (Dict :: Dict (Monad m)) :: Dict (Monad (g m))) :: Dict (Monad (f (g m))) of
    Dict -> Compose . return
  (>>=) = case dict (dict (Dict :: Dict (Monad m)) :: Dict (Monad (g m))) :: Dict (Monad (f (g m))) of
    Dict -> \x f -> Compose $ decompose x >>= decompose . f

instance (MapsTo Monad Monad f, MapsTo Monad Monad g) => MapsTo Monad Monad (Compose f g) where
  dict Dict = Dict

class MapsTo Monad Monad t => MonadTrans t where
  lift :: Monad m => m a -> t m a

instance (MonadTrans f, MonadTrans g) => MonadTrans (Compose f g) where
  lift = lift'
    where lift' :: forall m a. Monad m => m a -> (Compose f g) m a
          lift' = case dict (Dict :: Dict (Monad m)) :: Dict (Monad (g m)) of 
            Dict -> Compose . lift . lift