data Peano
foreign import data Succ :: Peano -> Peano
foreign import data Z :: Peano

instance fooZ :: Foo Z
instance foo2 :: Foo (Succ (Succ Z))
instance fooN :: Foo (Succ n)

module Test.Main where

import Prelude

import Control.Monad.Indexed (class IxApplicative, class IxApply, class IxBind, class IxFunctor, class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.List (List(..), fromFoldable)
import Data.Newtype (class Newtype, unwrap)
import Effect (Effect)
import Effect.Class (class MonadEffect)
import Effect.Class.Console (log)
import Type.Proxy (Proxy(..))

data Unk

foreign import data Unk0 :: Unk

foreign import data UnkX :: Unk -> Unk
newtype MUnk (i :: Unk) (o :: Unk) a
  = MUnk (Effect a)

derive instance newtypeUnk :: Newtype (MUnk i o a) _

derive newtype instance functorMUnk :: Functor (MUnk i o)

derive newtype instance applicativeMUnk :: Applicative (MUnk i o)

derive newtype instance applyMUnk :: Apply (MUnk i o)
derive newtype instance bindMUnk :: Bind (MUnk i o)
derive newtype instance monadMUnk :: Monad (MUnk i o)
derive newtype instance monadEffectMUnk :: MonadEffect (MUnk i o)

instance munkIxFunctor :: IxFunctor MUnk where
  imap f (MUnk a) = MUnk (f <$> a)

instance munkIxApplicative :: IxApply MUnk where
  iapply (MUnk f) (MUnk a) = MUnk (f <*> a)

instance munkIxApply :: IxApplicative MUnk where
  ipure a = MUnk $ pure a

instance munkIxBind :: IxBind MUnk where
  ibind (MUnk monad) function = MUnk (monad >>= (unwrap <<< function))

instance munkIxMonad :: IxMonad MUnk

class TLShow :: ∀ (k ∷ Type). k → Constraint
class TLShow i where
  tlShow :: Proxy i -> String

instance tlShowUnk2 :: TLShow (UnkX (UnkX Unk0)) where
  tlShow _ = "I'm unk 2"
else instance tlShowUnk0 :: TLShow Unk0 where
  tlShow _ = "Unk0"
else instance tlShowUnkX :: TLShow x => TLShow (UnkX x) where
  tlShow _ = "UnkX (" <> tlShow (Proxy :: Proxy x) <> ")"

class IxRec m where
  next :: forall (i :: Unk) a. Show a => TLShow i => a -> m i (UnkX i) a
  done :: forall (i :: Unk). m i Unk0 Unit

iFor_ :: forall (i :: Unk) m a. Show a => TLShow i => IxRec m => IxMonad m => List a -> m i Unk0 Unit
iFor_ Nil = done
iFor_ (Cons a b) = Ix.do
  _ <- next a
  iFor_ b

printMUnk :: forall (i :: Unk). TLShow i => MUnk i i Unit
printMUnk = Ix.do
  log $ tlShow (Proxy :: Proxy i)

instance ixRec :: IxRec MUnk where
  next a = Ix.do
    printMUnk
    log $ show a
    pure a
  done = pure unit

foreign import arr0 :: Effect (Array Int)

main :: Effect Unit
main = do
  list0 <- fromFoldable <$> arr0
  let (MUnk o) = (iFor_ :: List Int -> MUnk Unk0 Unk0 Unit) list0
  o
  log $ (tlShow (Proxy :: Proxy (UnkX (UnkX (UnkX Unk0)))))