{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
{-# LANGUAGE KindSignatures, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.TypeLevel.List (
	Length(..), IsPrefixOf, InfixIndex(..),
	module Data.TypeLevel.List.Unzip
	) where

import Prelude hiding (length, unzip)

import Data.TypeLevel.List.Unzip

class Length (as :: [k]) where length :: Integral n => n
instance Length '[] where length :: forall n. Integral n => n
length = n
0
instance Length as => Length (a ': as) where length :: forall n. Integral n => n
length = forall k (as :: [k]) n. (Length as, Integral n) => n
length @_ @as n -> n -> n
forall a. Num a => a -> a -> a
+ n
1

class (xs :: [k]) `IsPrefixOf` (ys :: [k])
instance '[] `IsPrefixOf` ys
instance xs `IsPrefixOf` ys => (x ': xs) `IsPrefixOf` (x ': ys)

class InfixIndex (xs :: [k]) (ys :: [k]) where infixIndex :: Int

instance (x ': xs) `IsPrefixOf` (x ': ys) =>
	InfixIndex (x ': xs) (x ': ys) where
	infixIndex :: Int
infixIndex = Int
0

instance {-# OVERLAPPABLE #-} InfixIndex xs ys => InfixIndex xs (y ': ys) where
	infixIndex :: Int
infixIndex = forall k (xs :: [k]) (ys :: [k]). InfixIndex xs ys => Int
infixIndex @_ @xs @ys Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1