Type.Errors

Generating Error Messages

data ErrorMessage where

A description of a custom type error.

Constructors

Text :: forall. Symbol -> ErrorMessage

Show the text as is.

ShowType :: forall t. t -> ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 5

Stack two pieces of error message on top of each other.

type family PrettyPrintList (vs :: [k]) :: ErrorMessage where ...

Pretty print a list.

>>> :show_error PrettyPrintList '[Bool]
...
... 'Bool'
...

>>> :show_error PrettyPrintList '[1, 2]
...
... '1', and '2'
...

>>> :show_error PrettyPrintList '["hello", "world", "cool"]
...
... "hello", "world", and "cool"
...

Since: 0.1.0.0

Equations

PrettyPrintList '[] = Text ""

PrettyPrintList '[a] = ShowTypeQuoted a

PrettyPrintList '[a, b] = (ShowTypeQuoted a :<>: Text ", and ") :<>: ShowTypeQuoted b

PrettyPrintList (a ': vs) = (ShowTypeQuoted a :<>: Text ", ") :<>: PrettyPrintList vs

type family ShowTypeQuoted (t :: k) :: ErrorMessage where ...

Like ShowType, but quotes the type if necessary.

>>> :show_error ShowTypeQuoted Int
...
... 'Int'
...

>>> :show_error ShowTypeQuoted "symbols aren't quoted"
...
... "symbols aren't quoted"
...

Since: 0.1.0.0

Equations

ShowTypeQuoted (t :: Symbol) = ShowType t

ShowTypeQuoted t = (Text "'" :<>: ShowType t) :<>: Text "'"

Emitting Error Messages

type family TypeError (a :: ErrorMessage) :: b where ...

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: base-4.9.0.0

type DelayError err = Eval (DelayErrorFcf err)

Error messages produced via TypeError are often too strict, and will be emitted sooner than you'd like. The solution is to use DelayError, which will switch the error messages to being consumed lazily.

>>> :{
foo :: TypeError ('Text "Too eager; prevents compilation") => ()
foo = ()
:}
...
... Too eager; prevents compilation
...

>>> :{
foo :: DelayError ('Text "Lazy; emitted on use") => ()
foo = ()
:}

>>> foo
...
... Lazy; emitted on use
...

Since: 0.1.0.0

data DelayErrorFcf :: ErrorMessage -> Exp k

Like DelayError, but implemented as a first-class family. DelayErrorFcf is useful when used as the last argument to IfStuck and UnlessStuck.

Since: 0.1.0.0

Instances

type Eval (DelayErrorFcf a2 :: a1 -> Type)

Defined in Type.Errors

type Eval (DelayErrorFcf a2 :: a1 -> Type) = (TypeError a2 :: a1)

type NoError = (() :: Constraint)

A helper definition that doesn't emit a type error. This is occassionally useful to leave as the residual constraint in IfStuck when you only want to observe if an expression isn't stuck.

Since: 0.1.0.0

type NoErrorFcf = Pure NoError

Like NoError, but implemented as a first-class family. NoErrorFcf is useful when used as the last argument to IfStuck and UnlessStuck.

Since: 0.1.0.0

Observing Stuckness

type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where ...

IfStuck expr b c leaves b in the residual constraints whenever expr is stuck, otherwise it Evaluates c.

Often you want to leave a DelayError in b in order to report an error when expr is stuck.

The c parameter is a first-class family, which allows you to perform arbitrarily-complicated type-level computations whenever expr isn't stuck. For example, you might want to produce a typeclass Constraint here. Alternatively, you can nest calls to IfStuck in order to do subsequent processing.

This is a generalization of kcsongor's Break machinery described in detecting the undetectable.

Since: 0.1.0.0

Equations

IfStuck (_ AnythingOfAnyKind) b c = b

IfStuck a b c = Eval c

type WhenStuck expr b = IfStuck expr b NoErrorFcf

Like IfStuck, but specialized to the case when you don't want to do anything if expr isn't stuck.

>>> :{
observe_no_rep
    :: WhenStuck
         (Rep t)
         (DelayError ('Text "No Rep instance for " ':<>: ShowTypeQuoted t))
    => t
    -> ()
observe_no_rep _ = ()
:}

>>> observe_no_rep HasNoRep
...
... No Rep instance for 'HasNoRep'
...

>>> observe_no_rep True
()

Since: 0.1.0.0

type UnlessStuck expr c = IfStuck expr NoError c

Like IfStuck, but leaves no residual constraint when expr is stuck. This can be used to ensure an expression isn't stuck before analyzing it further.

See the example under UnlessPhantomFcf for an example of this use-case.

Since: 0.1.0.0

Observing Phantomness

type PHANTOM = VAR

A meta-variable for marking which argument should be a phantom when working with UnlessPhantom and UnlessPhantomFcf.

PHANTOM is polykinded and can be used in several settings.

See UnlessPhantom for examples.

Since: 0.1.0.0

type UnlessPhantom exp err = Eval (UnlessPhantomFcf exp err)

UnlessPhantom expr err determines if the type described by expr is phantom in the variables marked via PHANTOM. If it's not, it produces the error message err.

For example, consider the definition:

>>> :{
data Qux a b = Qux b
:}

which is phantom in a:

>>> :eval_error UnlessPhantom (Qux PHANTOM Int) ('Text "Ok")
()

but not in b:

>>> :eval_error UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!")
...
... Bad!
...

Unfortunately there is no known way to emit an error message if the variable is a phantom.

Since: 0.1.0.0

data UnlessPhantomFcf :: k -> ErrorMessage -> Exp Constraint

Like UnlessPhantom, but implemented as a first-class family. As such, this allows UnlessPhantomFcf to be chained after IfStuck to only be run if an expression isn't stuck.

This can be used to avoid emitting false error messages when a type variable isn't phantom, just ambiguous.

>>> :{
observe_phantom
    :: UnlessStuck
         f
         (UnlessPhantomFcf
           (f PHANTOM)
           ('Text "It's not phantom!"))
    => f p
    -> ()
observe_phantom _ = ()
:}

>>> observe_phantom Proxy
()

>>> observe_phantom (Just 5)
...
... It's not phantom!
...

In the next example, we leave observe_phantom unsaturated, and therefore f isn't yet known. Without guarding the UnlessPhantomFcf behind UnlessStuck, this would incorrectly produce the message "It's not phantom!"

>>> observe_phantom
...
... No instance for (Show ...
...

Since: 0.1.0.0

Instances

type Eval (UnlessPhantomFcf exp err :: Constraint -> Type)

Defined in Type.Errors

type Eval (UnlessPhantomFcf exp err :: Constraint -> Type) = Coercible (SubstVar exp (Stuck :: (Any :: Type))) (SubstVar exp (DelayError err :: (Any :: Type)))

Performing Type Substitutions

type family Subst (e :: k1) (var :: k2) (sub :: k2) :: k1 where ...

Subst expr a b substitutes all instances of a for b in expr.

>>> :kind! Subst (Either Int Int) Int Bool
...
= Either Bool Bool

>>> :kind! Subst (Either Int Bool) Int [Char]
...
= Either [Char] Bool

>>> :kind! Subst (Either Int Bool) Either (->)
...
= Int -> Bool

Since: 0.1.0.0

Equations

Subst var var sub = sub

Subst (a b) var sub = Subst a var sub (Subst b var sub)

Subst a var sub = a

type VAR = SubMe Var

VAR is a meta-varaible which marks a substitution in SubstVar. The result of SubstVar expr val is expr[val/VAR].

VAR is polykinded and can be used in several settings.

See SubstVar for examples.

Since: 0.1.0.0

type family SubstVar (e :: k1) (r :: k2) :: k1 where ...

Like Subst, but uses the explicit meta-variable VAR to mark substitution points.

>>> :kind! SubstVar (Either VAR Bool) [Char]
...
= Either [Char] Bool

>>> :kind! SubstVar (VAR Int Bool :: Type) (->)
...
= Int -> Bool

Since: 0.1.0.0

Equations

SubstVar (_ Var) r = r

SubstVar (a b) r = SubstVar a r (SubstVar b r)

SubstVar a r = a

Working With Fcfs

type Exp a = a -> Type

Kind of type-level expressions indexed by their result type.

type family Eval (e :: Exp a) :: a

Expression evaluator.

Instances

type Eval (Not False)

Defined in Fcf.Data.Bool

type Eval (Not False) = True

type Eval (Not True)

Defined in Fcf.Data.Bool

type Eval (Not True) = False

type Eval (Constraints (a ': as) :: Constraint -> Type)

Defined in Fcf.Utils

type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))

type Eval (Constraints ([] :: [Constraint]))

Defined in Fcf.Utils

type Eval (Constraints ([] :: [Constraint])) = ()

type Eval (Null (a2 ': as) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null (a2 ': as) :: Bool -> Type) = False

type Eval (Null ([] :: [a]) :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Null ([] :: [a]) :: Bool -> Type) = True

type Eval (a <= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a <= b :: Bool -> Type) = a <=? b

type Eval (a >= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a >= b :: Bool -> Type) = b <=? a

type Eval (a < b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))

type Eval (a > b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))

type Eval (False || b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (False || b :: Bool -> Type) = b

type Eval (True || b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (True || b :: Bool -> Type) = True

type Eval (a || False :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a || False :: Bool -> Type) = a

type Eval (a || True :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a || True :: Bool -> Type) = True

type Eval (False && b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (False && b :: Bool -> Type) = False

type Eval (True && b :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (True && b :: Bool -> Type) = b

type Eval (a && True :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a && True :: Bool -> Type) = a

type Eval (a && False :: Bool -> Type)

Defined in Fcf.Data.Bool

type Eval (a && False :: Bool -> Type) = False

type Eval (IsNothing (Nothing :: Maybe a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsNothing (Nothing :: Maybe a) :: Bool -> Type) = True

type Eval (IsNothing (Just _a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsNothing (Just _a) :: Bool -> Type) = False

type Eval (IsJust (Nothing :: Maybe a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsJust (Nothing :: Maybe a) :: Bool -> Type) = False

type Eval (IsJust (Just _a) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsJust (Just _a) :: Bool -> Type) = True

type Eval (Length (a2 ': as) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)

type Eval (Length ([] :: [a]) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length ([] :: [a]) :: Nat -> Type) = 0

type Eval (a + b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a + b :: Nat -> Type) = a + b

type Eval (a - b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a - b :: Nat -> Type) = a - b

type Eval (a * b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a * b :: Nat -> Type) = a * b

type Eval (a ^ b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b

type Eval (DelayErrorFcf a2 :: a1 -> Type)

Defined in Type.Errors

type Eval (DelayErrorFcf a2 :: a1 -> Type) = (TypeError a2 :: a1)

type Eval (Error msg :: a -> Type)

Defined in Fcf.Utils

type Eval (Error msg :: a -> Type) = (TypeError (Text msg) :: a)

type Eval (TError msg :: a -> Type)

Defined in Fcf.Utils

type Eval (TError msg :: a -> Type) = (TypeError msg :: a)

type Eval (Pure x :: a -> Type)

Defined in Fcf.Combinators

type Eval (Pure x :: a -> Type) = x

type Eval (Join e :: a -> Type)

Defined in Fcf.Combinators

type Eval (Join e :: a -> Type) = Eval (Eval e)

type Eval (IsLeft (Right _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsLeft (Right _a :: Either a b) :: Bool -> Type) = False

type Eval (IsLeft (Left _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsLeft (Left _a :: Either a b) :: Bool -> Type) = True

type Eval (IsRight (Right _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsRight (Right _a :: Either a b) :: Bool -> Type) = True

type Eval (IsRight (Left _a :: Either a b) :: Bool -> Type)

Defined in Fcf.Data.Common

type Eval (IsRight (Left _a :: Either a b) :: Bool -> Type) = False

type Eval (UnlessPhantomFcf exp err :: Constraint -> Type)

Defined in Type.Errors

type Eval (UnlessPhantomFcf exp err :: Constraint -> Type) = Coercible (SubstVar exp (Stuck :: (Any :: Type))) (SubstVar exp (DelayError err :: (Any :: Type)))

type Eval (Fst ((,) a2 _b) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (Fst ((,) a2 _b) :: a1 -> Type) = a2

type Eval (Snd ((,) _a b) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (Snd ((,) _a b) :: a1 -> Type) = b

type Eval (FromMaybe _a (Just b) :: a -> Type)

Defined in Fcf.Data.Common

type Eval (FromMaybe _a (Just b) :: a -> Type) = b

type Eval (FromMaybe a2 (Nothing :: Maybe a1) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (FromMaybe a2 (Nothing :: Maybe a1) :: a1 -> Type) = a2

type Eval (TyEq a b :: Bool -> Type)

Defined in Fcf.Utils

type Eval (TyEq a b :: Bool -> Type) = TyEqImpl a b

type Eval (UnBool fal tru True :: a -> Type)

Defined in Fcf.Data.Bool

type Eval (UnBool fal tru True :: a -> Type) = Eval tru

type Eval (UnBool fal tru False :: a -> Type)

Defined in Fcf.Data.Bool

type Eval (UnBool fal tru False :: a -> Type) = Eval fal

type Eval (Guarded x ((p := y) ': ys) :: a2 -> Type)

Defined in Fcf.Data.Bool

type Eval (Guarded x ((p := y) ': ys) :: a2 -> Type) = Eval (If (Eval (p x)) y (Guarded x ys))

type Eval (Pure1 f x :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure1 f x :: a2 -> Type) = f x

type Eval (k =<< e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (k =<< e :: a2 -> Type) = Eval (k (Eval e))

type Eval (f <$> e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f <$> e :: a2 -> Type) = f (Eval e)

type Eval (f <*> e :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)

type Eval (ConstFn a2 _b :: a1 -> Type)

Defined in Fcf.Combinators

type Eval (ConstFn a2 _b :: a1 -> Type) = a2

type Eval (f $ a3 :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (f $ a3 :: a2 -> Type) = Eval (f a3)

type Eval (Foldr f y (x ': xs) :: a2 -> Type)

Defined in Fcf.Data.List

type Eval (Foldr f y (x ': xs) :: a2 -> Type) = Eval (f x (Eval (Foldr f y xs)))

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type)

Defined in Fcf.Data.List

type Eval (Foldr f y ([] :: [a1]) :: a2 -> Type) = y

type Eval (UnList y f xs :: a2 -> Type)

Defined in Fcf.Data.List

type Eval (UnList y f xs :: a2 -> Type) = Eval (Foldr f y xs)

type Eval (Uncurry f ((,) x y) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (Uncurry f ((,) x y) :: a2 -> Type) = Eval (f x y)

type Eval (UnMaybe y f (Just x) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (UnMaybe y f (Just x) :: a2 -> Type) = Eval (f x)

type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type)

Defined in Fcf.Data.Common

type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 -> Type) = Eval y

type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (UnEither f g (Right y :: Either a2 b) :: a1 -> Type) = Eval (g y)

type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type)

Defined in Fcf.Data.Common

type Eval (UnEither f g (Left x :: Either a2 b) :: a1 -> Type) = Eval (f x)

type Eval (Pure2 f x y :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure2 f x y :: a2 -> Type) = f x y

type Eval ((f <=< g) x :: a3 -> Type)

Defined in Fcf.Combinators

type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))

type Eval (LiftM2 f x y :: a3 -> Type)

Defined in Fcf.Combinators

type Eval (LiftM2 f x y :: a3 -> Type) = Eval (f (Eval x) (Eval y))

type Eval (Flip f y x :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Flip f y x :: a2 -> Type) = Eval (f x y)

type Eval (Pure3 f x y z :: a2 -> Type)

Defined in Fcf.Combinators

type Eval (Pure3 f x y z :: a2 -> Type) = f x y z

type Eval (LiftM3 f x y z :: a4 -> Type)

Defined in Fcf.Combinators

type Eval (LiftM3 f x y z :: a4 -> Type) = Eval (f (Eval x) (Eval y) (Eval z))

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] -> Type) = Eval ((Map (Cons a2) :: Maybe [a1] -> Maybe [a1] -> Type) =<< Init (b ': as))

type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] -> Type) = Just ([] :: [a1])

type Eval (Init ([] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Init ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

type Eval (Tail (_a ': as) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail (_a ': as) :: Maybe [a] -> Type) = Just as

type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type)

Defined in Fcf.Data.List

type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2

type Eval (Head ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) = Eval (Last (b ': as))

type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 -> Type) = Just a2

type Eval (Last ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Last ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

type Eval (Cons a2 as :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as

type Eval ((x ': xs) ++ ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval ((x ': xs) ++ ys :: [a] -> Type) = x ': Eval (xs ++ ys)

type Eval (([] :: [a]) ++ ys :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (([] :: [a]) ++ ys :: [a] -> Type) = ys

type Eval (Filter p (a2 ': as) :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Filter p (a2 ': as) :: [a1] -> Type) = If (Eval (p a2)) (a2 ': Eval (Filter p as)) (Eval (Filter p as))

type Eval (Filter _p ([] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure (Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))

type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type) = (Nothing :: Maybe Nat)

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

type Eval (Find p (a2 ': as) :: Maybe a1 -> Type) = If (Eval (p a2)) (Just a2) (Eval (Find p as))

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)

type Eval (SetIndex n a' as :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (SetIndex n a' as :: [k] -> Type) = SetIndexImpl n a' as

type Eval (Map f (a2 ': as) :: [b] -> Type)

Defined in Fcf.Classes

type Eval (Map f (a2 ': as) :: [b] -> Type) = Eval (f a2) ': Eval (Map f as)

type Eval (Map f ([] :: [a]) :: [b] -> Type)

Defined in Fcf.Classes

type Eval (Map f ([] :: [a]) :: [b] -> Type) = ([] :: [b])

type Eval (Map f (Just a3) :: Maybe a2 -> Type)

Defined in Fcf.Classes

type Eval (Map f (Just a3) :: Maybe a2 -> Type) = Just (Eval (f a3))

type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type)

Defined in Fcf.Classes

type Eval (Map f (Nothing :: Maybe a) :: Maybe b -> Type) = (Nothing :: Maybe b)

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] -> Type) = Eval (f a2 b2) ': Eval (ZipWith f as bs)

type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f _as ([] :: [b]) :: [c] -> Type) = ([] :: [c])

type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type)

Defined in Fcf.Data.List

type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])

type Eval (Unzip as :: ([a], [b]) -> Type)

Defined in Fcf.Data.List

type Eval (Unzip as :: ([a], [b]) -> Type) = Eval (Foldr (Cons2 :: (a, b) -> ([a], [b]) -> ([a], [b]) -> Type) ((,) ([] :: [a]) ([] :: [b])) (Eval as))

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type)

Defined in Fcf.Data.List

type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) -> Type) = (,) (a3 ': as) (b ': bs)

type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type)

Defined in Fcf.Classes

type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b -> Type) = (Right (Eval (f a3)) :: Either a2 b)

type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type)

Defined in Fcf.Classes

type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b -> Type) = (Left x :: Either a2 b)

type Eval (Map f ((,) x a2) :: (k2, k1) -> Type)

Defined in Fcf.Classes

type Eval (Map f ((,) x a2) :: (k2, k1) -> Type) = (,) x (Eval (f a2))

type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type)

Defined in Fcf.Data.Common

type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) -> Type) = (,) (Eval (f b2)) (Eval (f' b'2))

type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type)

Defined in Fcf.Classes

type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 -> Type) = (Right (Eval (g y)) :: Either a' b2)

type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type)

Defined in Fcf.Classes

type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' -> Type) = (Left (Eval (f x)) :: Either a2 b')

type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type)

Defined in Fcf.Classes

type Eval (Bimap f g ((,) x y) :: (k2, k1) -> Type) = (,) (Eval (f x)) (Eval (g y))

type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type)

Defined in Fcf.Classes

type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) -> Type) = (,,) x y (Eval (f a2))

type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type)

Defined in Fcf.Classes

type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) -> Type) = (,,,) x y z (Eval (f a2))

type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type)

Defined in Fcf.Classes

type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) -> Type) = (,,,,) x y z w (Eval (f a2))

data Pure (b :: a) (c :: a) :: forall a. a -> a -> Type

Instances

type Eval (Pure x :: a -> Type)

Defined in Fcf.Combinators

type Eval (Pure x :: a -> Type) = x