{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_HADDOCK not-home #-}
module Polysemy.Internal.Index where
import GHC.TypeLits (Nat)
import Type.Errors (TypeError, ErrorMessage(ShowType))
import Type.Errors.Pretty (type (<>), type (%))
import Polysemy.Internal.Sing (SList (SEnd, SCons))
class InsertAtIndex (index :: Nat) (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k]) where
insertAtIndex :: SList inserted
instance inserted ~ '[] => InsertAtIndex index head oldTail oldTail full inserted where
insertAtIndex :: SList inserted
insertAtIndex = SList inserted
forall a. SList '[]
SEnd
{-# INLINE insertAtIndex #-}
instance {-# INCOHERENT #-} (
InsertAtIndex index head tail oldTail full insertedTail,
inserted ~ (e ': insertedTail)
) => InsertAtIndex index head (e ': tail) oldTail full inserted where
insertAtIndex :: SList inserted
insertAtIndex = SList insertedTail -> SList (e : insertedTail)
forall a (xs :: [a]) (x :: a). SList xs -> SList (x : xs)
SCons (forall (inserted :: [a]).
InsertAtIndex index head tail oldTail full inserted =>
SList inserted
forall k (index :: Nat) (head :: [k]) (tail :: [k])
(oldTail :: [k]) (full :: [k]) (inserted :: [k]).
InsertAtIndex index head tail oldTail full inserted =>
SList inserted
insertAtIndex @_ @index @head @tail @oldTail @full)
{-# INLINE insertAtIndex #-}
instance {-# INCOHERENT #-} TypeError (InsertAtFailure index oldTail head full)
=> InsertAtIndex index head tail oldTail full inserted where
insertAtIndex :: SList inserted
insertAtIndex = [Char] -> SList inserted
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"
type family InsertAtUnprovidedIndex where
InsertAtUnprovidedIndex = TypeError (
"insertAt: You must provide the index at which the effects should be inserted as a type application."
% "Example: insertAt @5"
)
type InsertAtFailure index soughtTail head full =
"insertAt: Failed to insert effects at index " <> 'ShowType index
% "There is a mismatch between what's been determined as the head and tail between the newly inserted effects,"
<> " and the actual desired return type."
% "Determined head before inserted effects:"
% "\t" <> 'ShowType head
% "Determined tail after the inserted effects:"
% "\t" <> 'ShowType soughtTail
% "Actual desired return type:"
% "\t" <> 'ShowType full
% "Make sure that the index provided to insertAt is correct, and that the desired return type simply requires"
<> " inserting effects."