{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module FindElem (
FindElem(..)
, Idx(..)) where
import GHC.TypeLits ( TypeError, ErrorMessage(Text, (:<>:), (:$$:), ShowType) )
class FindElem x xs where
findElem :: Idx x 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"