gistfile1.txt

data General : (phi : Type) -> (r : phi -> Type) -> (a : Type) -> Type where
  Here : a -> General phi t a
  Request : (ix : phi) -> (k : t ix -> General phi t a) -> General phi t a

implementation Functor (General phi t) where
  map f (Here x) = Here (f x)
  map f (Request ix k) = Request ix (\j => map f $ k j)

implementation Applicative (General phi t) where
  pure = Here
  (<*>) (Here f) y = map f y
  (<*>) (Request ix k) y = Request ix (\j => k j <*> y)

cata : (r : a -> b) -> (c : (ix : phi) -> (t ix -> b) -> b) -> (x : General phi t a) -> b
cata r c (Here x) = r x
cata r c (Request ix k) = c ix $ \t => cata r c (k t)

implementation Monad (General phi t) where
  (>>=) g k = cata k Request g

call : (ix : phi) -> General phi t (t ix)
call ix = ix `Request` Here

PiG : (phi : Type) -> (t : phi -> Type) -> Type
PiG phi t = (ix : phi) -> General phi t (t ix)

-----
immediate : General Bool (const Int) Int
immediate = Here 5

delayed : General Bool (const Int) Int
delayed = Request True Here
-----
fusc : Nat -> Nat
fusc Z = Z
fusc (S n) = S (fusc (fusc n))

fusc' : PiG Nat (const Nat)
fusc' Z = pure Z
fusc' (S n) = do pure (S !(call !(call n)))

------------------------------
--- Here there be Dragons. ---
------------------------------
interface Monad m => Kleisli (m : Type -> Type) where
  rho : (b -> m c) -> (a -> m b) -> (a -> m c)
  rho f g a = g a >>= f

morph : Kleisli m => (h : (ix : phi) -> m (t ix)) -> General phi t a -> m a
morph h = cata pure ((>>=) . h)

gistfile2.txt

- + Errors (1)
 `-- general.idr line 50 col 27:
     When checking right hand side of morph with expected type
             General phi t a -> m a
     
     When checking an application of function Prelude.Basics..:
             Type mismatch between
                     (ix : phi) -> m (t ix) (Type of h)
             and
                     phi -> m (t _) (Expected type)
             
             Specifically:
                     Type mismatch between
                             t v0
                     and
                             t _