Polysemy.Internal.Index

Documentation

class InsertAtIndex (index :: Nat) (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k]) where

Infer a partition of the result type full so that for the fixed segments head and tail, the new segment inserted contains the missing effects between them.

Methods

insertAtIndex :: SList inserted

Instances

inserted ~ ('[] :: [k]) => InsertAtIndex index (head :: [k]) (oldTail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k])

Defined in Polysemy.Internal.Index

Methods

insertAtIndex :: SList inserted

(TypeError (InsertAtFailure index oldTail head full) :: Constraint) => InsertAtIndex index (head :: [k]) (tail :: [k]) (oldTail :: [k]) (full :: [k]) (inserted :: [k])

Defined in Polysemy.Internal.Index

Methods

insertAtIndex :: SList inserted

(InsertAtIndex index head tail oldTail full insertedTail, inserted ~ (e ': insertedTail)) => InsertAtIndex index (head :: [a]) (e ': tail :: [a]) (oldTail :: [a]) (full :: [a]) (inserted :: [a])

Defined in Polysemy.Internal.Index

Methods

insertAtIndex :: SList inserted

type family InsertAtUnprovidedIndex where ...

Equations

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."))))))))