{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

{- | Auxiliary definitions for finding a type in a type-level list.
-}

module FindElem (
    FindElem(..)
  , Idx(..)) where

import GHC.TypeLits ( TypeError, ErrorMessage(Text, (:<>:), (:$$:), ShowType) )

-- | Proof that @x@ is an element of the type-level list @xs@
class FindElem x xs where
  findElem :: Idx x xs

-- | The integer index of @x@ in @xs@
newtype Idx x xs = Idx {forall {k} {k} (x :: k) (xs :: k). Idx x xs -> Int
unIdx :: Int}

instance FindElem x (x ': xs) where
  findElem :: Idx x (x : xs)
findElem = Int -> Idx x (x : xs)
forall {k} {k} (x :: k) (xs :: k). Int -> Idx x xs
Idx Int
0

instance {-# OVERLAPPABLE #-} FindElem x xs => FindElem x (x' : xs) where
  findElem :: Idx x (x' : xs)
findElem = Int -> Idx x (x' : xs)
forall {k} {k} (x :: k) (xs :: k). Int -> Idx x xs
Idx (Int -> Idx x (x' : xs)) -> Int -> Idx x (x' : xs)
forall a b. (a -> b) -> a -> b
$ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Idx x xs -> Int
forall {k} {k} (x :: k) (xs :: k). Idx x xs -> Int
unIdx (Idx x xs
forall {k} {k} (x :: k) (xs :: k). FindElem x xs => Idx x xs
findElem :: Idx x xs)

instance TypeError ('Text "Cannot unify effect types." ':$$:
                    'Text "Unhandled effect: " ':<>: 'ShowType x ':$$:
                    'Text "Perhaps check the type of effectful computation and the sequence of handlers for concordance?")
  => FindElem x '[] where
  findElem :: Idx x '[]
findElem = [Char] -> Idx x '[]
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"