content: {-# LANGUAGE DataKinds, GADTs, KindSignatures, RankNTypes, StandaloneDeriving,
      QuantifiedConstraints, LambdaCase, ScopedTypeVariables,
      TypeFamilies, UndecidableInstances, ConstraintKinds,
      IncoherentInstances, OverlappingInstances, TypeOperators #-}
  
  module Main where
  
  import Data.Constraint
  import Unsafe.Coerce
  
  data Time = Z | S Time deriving Show
  data Timey (t :: Time) :: * where
    Zy :: Timey Z
    Sy :: Timey n -> Timey (S n)
  
  data Le :: Time -> Time -> * where
    Now    :: Le t t
    Later  :: Le s t -> Le s (S t)
  deriving instance Show (Le s t)
  
  class Timed (v :: Time -> *) where
    (&>) :: v s -> Le s t -> v t
  
  instance Timed (Le s) where
    v &> Now = v
    v &> Later u = Later (v &> u)
  
  class LE (s :: Time)(t :: Time) where
    lesson :: Le s t
  
  instance LE s s where
    lesson = Now
  
  class StepTo (t :: Time) where
    type StepFrom t :: Time
    step :: Le (StepFrom t) t
  
  instance (LE s (StepFrom t), StepTo t) => LE s t where
    lesson = lesson &> step
  
  data FakeLe s t = FakeLe (Le s t)
  
  mkStep :: forall s t. Le s t -> Dict (StepTo t, (StepFrom t ~ s))
  mkStep u = case (foo, baz) of
      (Dict, Dict) -> Dict
    where
    foo :: Dict (StepTo t)
    foo = unsafeCoerce (FakeLe u)
    bar :: Dict (s ~ s)
    bar = Dict
    baz :: Dict (StepFrom t ~ s)
    baz = unsafeCoerce bar
  
  leap :: forall s t x
        . Le s t
       -> ((StepTo t, StepFrom t ~ s) => x)
       -> x
  leap u k = case mkStep u of
    Dict -> k
  
  type Kripke v t = forall u. LE t u => v u
  
  kripke :: Timed v => v s -> Kripke v s
  kripke v = v &> lesson
  
  class MoTime (m :: (Time -> *) -> (Time -> *)) where
    retNow :: Timed v => v s -> m v s
    (>>>=) :: (Timed f, Timed g)
           => m f s
           -> (forall t. (StepTo t, StepFrom t ~ s) =>
               Kripke f t -> m g t)
           -> m g s
  
  data TiMo
    (c :: (Time -> *) -> Time -> *)
    (v :: Time -> *)
    (s :: Time)
    :: * where
    RetNow :: v s -> TiMo c v s
    Call :: forall c r v s
          . c r s
         -> (forall t. Le s t -> r t -> TiMo c v t)
         -> TiMo c v s
  
  instance (forall r. Timed (c r), Timed v) => Timed (TiMo c v) where
    RetNow v &> u = RetNow (v &> u)
    Call c k &> u = Call (c &> u) $ \ w -> k (u &> w)
  
  now :: v s -> Le s s
  now _ = Now
  
  instance MoTime (TiMo c) where
    retNow = RetNow
    (>>>=) :: forall c f g s. (Timed f, Timed g)
           => TiMo c f s
           -> (forall t. (StepTo t, StepFrom t ~ s) =>
               Kripke f t -> TiMo c g t)
           -> TiMo c g s
    RetNow v >>>= k = leap (now v) (k (kripke v))
    Call c j >>>= k = Call c $ \ u r ->
      j u r >>>= jump u step
      where
        jump :: forall t t'. Le s t -> Le t t'
             -> Kripke f t' -> TiMo c g t'
        jump u w f = leap (u &> w) (k f)
  
  op :: Timed r => c r s -> TiMo c r s
  op c = Call c $ \ u r -> RetNow r
  
  newtype Ticky (t :: Time) = Clock Int deriving Show
  
  instance Timed Ticky where
    x &> Now = x
    x &> Later u = case x &> u of
      Clock i -> Clock (i + 1)
  
  data Cmd (r :: Time -> *)(s :: Time) :: * where
    Grab :: Cmd Ticky s
    Emit :: Ticky s -> Cmd (K ()) s
    Wait :: Cmd (K ()) s
  
  instance Timed (Cmd b) where
    Grab   &> u = Grab
    Emit x &> u = Emit (x &> u)
    Wait   &> u = Wait
  
  data K (a :: *)(s :: Time) :: * where
    K :: a -> K a s
  instance Show a => Show (K a s) where show (K a) = show a
  instance Timed (K a) where
    K a &> _ = K a
  
  run :: forall s v. (forall i. Show (v i)) => Timey s -> TiMo Cmd v s -> IO ()
  run _ (RetNow v) = print v
  run s (Call Wait k) = wait Now s where
    wait :: forall t. Le s t -> Timey t -> IO ()
    wait u t = do
      putStrLn "waiting"
      getLine >>= \case
        "" -> wait (Later u) (Sy t)
        _  -> run t (k u (K ()))
  run s (Call Grab k) = run s (k Now (Clock 0))
  run s (Call (Emit (Clock x)) k) = do
    print x
    run s (k Now (K ()))
  
  myProg :: TiMo Cmd (K ()) Z
  myProg =
    op Grab >>>= \ x ->
    op Wait >>>= \ _ ->
    op (Emit x) >>>= \ _ ->
    retNow (K ())
  
  myProg' :: TiMo Cmd (K ()) Z
  myProg' =
    op Grab >>>= \ x ->
    op Wait >>>= \ _ ->
    op Grab >>>= \ y ->
    op (Emit x) >>>= \ _ ->
    -- retNow x >>>= \ x ->
    op (Emit y) >>>= \ _ ->
    op Wait >>>= \ _ ->
    op (Emit x) >>>= \ _ ->
    op (Emit y) >>>= \ _ ->
    retNow (K ())
  
  main :: IO ()
  main = run Zy myProg