{-# LANGUAGE TemplateHaskell, KindSignatures, DataKinds, PolyKinds, TypeFamilies, UndecidableInstances, GADTs, AllowAmbiguousTypes #-}

module BackwardsStateMonad where

import Data.Singletons.TH
import Data.Singletons.Prelude


$(promote [d|
 data Nat = Zero | Succ Nat

 bind :: (Nat -> (Foo, Nat)) -> (Foo -> Nat -> (Foo, Nat)) -> (Nat -> (Foo, Nat))
 bind m k s2 = let r1 :: (Foo, Nat)
                   r1 = m (snd r2)
                   r2 :: (Foo, Nat)
                   r2 = k (fst r1) s2
               in ((fst r2), (snd r1))
{-

 bind m k s2 = let (a,s0) = m s1
                   (b,s1) = k a s2
               in (b, s0)
-}
-- m `bind` k = \s2 -> let (a,s0) = m s1
--                         (b,s1) = k a s2
--                     in  (b,s0)

 data Foo = Foo

 m :: Nat -> (Foo, Nat)
 m n = (Foo, Succ n)

 k :: Foo -> Nat -> (Foo, Nat)
 k a n = (a, Succ n)

 bar :: Nat -> (Foo, Nat)
 bar p = (bind m k) p

 |])

instance Show Nat where
   show Zero = "Zero"
   show (Succ n) = "Succ (" ++ show n ++ ")"

instance Show Foo where
   show _ = "Foo"

baz1a :: Proxy (Bar Zero)
baz1a = Proxy

baz1b :: Proxy '( 'Foo, Succ (Succ Zero))
baz1b = baz1a
