{-# OPTIONS_GHC -fglasgow-exts #-}

module Indices where

data I ix = I { unI :: ix }

data Id ixr   (l :: * -> *) (r :: * -> *) ix = Ix l ixr => Id (r ixr)
data Unit     (l :: * -> *) (r :: * -> *) ix = Unit
data K a      (l :: * -> *) (r :: * -> *) ix = K a
data Sum f g  (l :: * -> *) (r :: * -> *) ix = Inl (f l r ix) | Inr (g l r ix)
data Prod f g (l :: * -> *) (r :: * -> *) ix = Prod (f l r ix) (g l r ix)

-- ((* -> *) -> (* -> *) -> * -> *) -> 

data Tag ixt f (l :: * -> *) (r :: * -> *) ix where
  Tag :: f l r ix -> Tag ix f l r ix

data HFix (h :: (* -> *) -> * -> *) ix     = HIn { hout :: h (HFix h) ix }

data TEq a b where
  TEq :: TEq a a

type family PF (l :: * -> *) :: (* -> *) -> (* -> *) -> * -> *

coerce :: (Repr l, Monad m) => l ix -> l ix' -> f ix -> m (f ix')
coerce ix ix' x
  = do
    TEq <- ixeq ix ix'
    return x

class Repr l where
  ixeq :: Monad m => l ix -> l ix' -> m (TEq ix ix')

class Ix l a where
  from :: a -> PF l l I a
  to :: PF l l I a -> a
  ix :: l a


type Str l a = HFix (PF l l) a