{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE LambdaCase #-}

module Data.Type.Index.Trans
  ( module Data.Type.Index.Trans
  , (:~:)(..)
  ) where

import Data.Type.Index
import Type.Class.Witness ((:~:)(..))
import Type.Family.List

ixList :: Index a b -> i b c -> IxList i a c
ixList = \case
  IZ   -> IxHead
  IS x -> IxTail . ixList x

data IxList (i :: k -> l -> *) :: [k] -> l -> * where
  IxHead :: !(i a b)
         -> IxList i (a :< as) b
  IxTail :: !(IxList i as b)
         -> IxList i (a :< as) b

data IxFirst (i :: k -> l -> *) :: (k,m) -> l -> * where
  IxFirst :: !(i a b)
          -> IxFirst i '(a,c) b

data IxSecond (i :: k -> l -> *) :: (m,k) -> l -> * where
  IxSecond :: !(i a b)
           -> IxSecond i '(c,a) b

data IxOr (i :: k -> m -> *) (j :: l -> m -> *) :: Either k l -> m -> * where
  IxOrL :: !(i a b)
        -> IxOr i j (Left a) b
  IxOrR :: !(j a b)
        -> IxOr i j (Right a) b

data IxJust (i :: k -> l -> *) :: Maybe k -> l -> * where
  IxJust :: !(i a b)
         -> IxJust i (Just a) b

data IxComp (i :: k -> l -> *) (j :: l -> m -> *) :: k -> m -> * where
  IxComp :: !(i a b)
         -> !(j b c)
         -> IxComp i j a c