{-# Language UndecidableInstances,MultiParamTypeClasses,TypeOperators , DataKinds,GADTs,TypeFamilies,TypeFamilyDependencies#-}
{-
fold a hlist of kliesli types
passing previous return type into next input
needs a hlist type with adjacently coupled types...
this can be generated by a zipWIth . tail pattern
-}

{-
eg = -- cant really use list, intersperse with Xcons instead
[\int
  -> return $ show int
,\string
  -> return $ (reverse string,read string)
,\(string,int)
  -> return $ replicate int string
,\strings
  -> return $ concat strings
 ]
eg :: HList (fmap (Uncurry . fmap IO) (Stagger xs))
type xs = '[Int,String,(String,Int),[String],String]

then have some function to fold this up into an Int -> IO String
-}

--foldl (>>=) :: (Foldable t, Monad m) => m a -> t (a -> m a) -> m a
-- a -> m b,b -> m c etc

infixr 6 :-:

data HList xs where
 HEmpty :: HList '[]
 (:-:)  :: x -> HList xs -> HList (x ': xs)

type XList m xs = HList (FX m xs)

-- should really use Map, but would have to defunctionalise and write Uncurry...
type family FX (m :: * -> *) (xs :: [*]) = (ys :: [*]) | ys -> m xs where
-- FX m (x ': y ': '[]) = '[x -> m y]
-- FX m (x ': y ':  xs) =  (x -> m y) ': FX m (y ': xs)

eg :: Monad m => XList m '[Int,String,(String,Int),[String],String]
eg =     (\int
   -> return $ show int)
 :-: (\string
   -> return $ (reverse string,read string))
 :-: (\(string,int)
  -> return $ replicate int string)
 :-: (\strings
  -> return $ concat strings)
 :-: HEmpty

eg1 :: XList IO '[Int,String,Bool]
eg1 = ((return . show) :: Int -> IO String) :-: ((return . null) :: String -> IO Bool) :-: HEmpty

type family Head xs where
 Head (x ': _) = x

type family Last xs where
 Last (x ': '[]) = x
 Last (x ': xs) = Last xs

{-
class RunXList m xs where
 runXList :: XList m xs -> (Head xs -> m (Last xs))

    * Couldn't match type `Head xs' with `Head xs0'
      Expected type: XList m xs -> Head xs -> m (Last xs)
        Actual type: XList m xs0 -> Head xs0 -> m (Last xs0)
      NB: `Head' is a non-injective type family
      The type variable `xs0' is ambiguous
    * In the ambiguity check for `runXList'
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        runXList :: forall (m :: * -> *) (xs :: [*]).
                    RunXList m xs =>
                    XList m xs -> Head xs -> m (Last xs)
      In the class declaration for `RunXList'
   |
64 |  runXList :: XList m xs -> (Head xs -> m (Last xs))
   |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
runXList (x :-: HEmpty) = x
runXList (x :-: xs) = x >>= (runXList xs)
-}

-- should really use nonempty list, eg. FX2 basecase

infixr 6 :--:

data HList2 (zs :: (*,[*],*)) where
 HLast2 :: (i -> o) -> HList2 '(i , '[] , o)
 (:--:)  :: i -> HList2 '(i' , xs , o) -> HList2 '(i, (i ': xs), o)

type XList2 m i xs o = HList2 (FX2 m i xs o)

type family FX2 m i (xs :: [*]) o where
 FX2 m i '[] o = '(i , '[] , m o) -- '[i -> m o]
 FX2 m i (x ': xs) o = InsertFX2 (i -> m x) (FX2 m x xs o)

type family InsertFX2 f xs where
 InsertFX2 f '(i,xs,o) = '(i,f ':xs,o)

{-
eg2 :: Monad m => XList2 m Int '[String,(String,Int),[String]] String
eg2 =     (\int
   -> return $ show int)
 :--: (\string
   -> return $ (reverse string,read string))
 :--: (\(string,int)
  -> return $ replicate int string)
 (HLast2 (\strings -> return $ concat strings))
-}

eg2 :: Monad m => XList2 m [String] '[] String
eg2 = (\strings -> return $ concat strings) :-: HEmpty

class RunXList m xs where
 runXList :: XList2 m i xs o -> (i -> m o)

{-
    * Couldn't match type `FX2 m i xs o' with `FX2 m i xs0 o'
      Expected type: XList2 m i xs o -> i -> m o
        Actual type: XList2 m i xs0 o -> i -> m o
      NB: `FX2' is a non-injective type family
      The type variable `xs0' is ambiguous
    * In the ambiguity check for `runXList'
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the class method:
        runXList :: forall (m :: * -> *) (xs :: [*]) i o.
                    RunXList m xs =>
                    XList2 m i xs o -> i -> m o
      In the class declaration for `RunXList'
    |
118 |  runXList :: XList2 m i xs o -> (i -> m o)
    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-}