Type.Errors

This module provides useful tools for writing better type-errors. For a quickstart guide to the underlying TypeError machinery, check out Dmitrii Kovanikov's excellent blog post A story told by Type Errors.

Generating Error Messages

data ErrorMessage

A description of a custom type error.

Constructors

Text Symbol

Show the text as is.

ShowType t

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

ErrorMessage :<>: ErrorMessage infixl 6

Put two pieces of error message next to each other.

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 AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind 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 UnlessPhantom for an example of this use-case.

Since: 0.1.0.0

Running Magic Stuck Type Families

te :: Q Type -> Q Type

This library provides tools for performing lexical substitutions over types. For example, the function UnlessPhantom asks you to mark phantom variables via PHANTOM.

Unfortunately, this substitution cannot reliably be performed via type families, since it will too often get stuck. Instead we provide te, which is capable of reasoning about types symbolically.

Any type which comes with the warning "This type family is always stuck." must be used in the context of te and the magic [t| quasiquoter. To illustrate, the following is stuck:

>>> :{
foo :: SubstVar VAR Bool
foo = True
:}
...
... Couldn't match expected type ...SubstVar VAR Bool...
... with actual type ...Bool...
...

But running it via te makes everything work:

>>> :{
foo :: $(te[t| SubstVar VAR Bool |])
foo = True
:}

If you don't want to think about when to use te, it's a no-op when used with everyday types:

>>> :{
bar :: $(te[t| Bool |])
bar = True
:}

Since: 0.2.0.0

Observing Phantomness

type family PHANTOM :: k

This type family is always stuck. It must be used in the context of te.

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

PHANTOM is polykinded and can be used in several settings.

See UnlessPhantom for examples.

Since: 0.1.0.0

type family UnlessPhantom :: k -> ErrorMessage -> Constraint

This type family is always stuck. It must be used in the context of te.

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 $(te[t| UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") |])
()

but not in b:

>>> :eval_error $(te[t| UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") |])
...
... Bad!
...

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

Often you'll want to guard UnlessPhantom against IfStuck, to ensure you don't get errors when things are merely ambiguous. You can do this by writing your own fcf whose implementation is UnlessPhantom:

>>> :{
data NotPhantomErrorFcf :: k -> Exp Constraint
type instance Eval (NotPhantomErrorFcf f) =
  $(te[t| UnlessPhantom (f PHANTOM)
                        ( ShowTypeQuoted f
                   ':<>: 'Text " is not phantom in its argument!")
        |])
:}

>>> :{
observe_phantom
    :: UnlessStuck
         f
         (NotPhantomErrorFcf f)
    => f p
    -> ()
observe_phantom _ = ()
:}

We then notice that using observe_phantom against Proxy doesn't produce any errors, but against Maybe does:

>>> observe_phantom Proxy
()

>>> observe_phantom (Just 5)
...
... 'Maybe' is not phantom in its argument!
...

Finally, we leave observe_phantom unsaturated, and therefore f isn't yet known. Without guarding the UnlessPhantom behind UnlessStuck, this would incorrectly produce the message "f is not phantom in its argument!"

>>> observe_phantom
...

Performing Type Substitutions

type family Subst :: k1 -> k1 -> k2 -> k2

This type family is always stuck. It must be used in the context of te.

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

>>> :kind! $(te[t| Subst (Either Int Int) Int Bool |])
...
= Either Bool Bool

>>> :kind! $(te[t| Subst (Either Int Bool) Int [Char] |])
...
= Either [Char] Bool

>>> :kind! $(te[t| Subst (Either Int Bool) Either (,) |])
...
= (Int, Bool)

Since: 0.2.0.0

type family VAR :: k

This type family is always stuck. It must be used in the context of te.

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.2.0.0

type family SubstVar :: k1 -> k2 -> k2

This type family is always stuck. It must be used in the context of te.

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

>>> :kind! $(te[t| SubstVar (Either VAR VAR) Bool |])
...
= Either Bool Bool

>>> :kind! $(te[t| SubstVar (Either VAR Bool) [Char] |])
...
= Either [Char] Bool

>>> :kind! $(te[t| SubstVar (VAR Int Bool) (,) |])
...
= (Int, Bool)

Since: 0.2.0.0

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 (MEmpty_ :: a -> Type)

Defined in Fcf.Class.Monoid

type Eval (MEmpty_ :: a -> Type) = MEmpty :: a

type Eval (Sum ns :: Nat -> Type)

Defined in Fcf.Class.Foldable

type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

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

Defined in Fcf.Data.List

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

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 (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 (And lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (And lst :: Bool -> Type) = Eval (Foldr (&&) 'True lst)

type Eval (Or lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (Or lst :: Bool -> Type) = Eval (Foldr (||) 'False lst)

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 && 'False :: Bool -> Type)

Defined in Fcf.Data.Bool

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

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

Defined in Fcf.Data.Bool

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

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 (IsJust ('Just _a) :: Bool -> Type)

Defined in Fcf.Data.Common

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

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

Defined in Fcf.Data.Common

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

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

Defined in Fcf.Data.Common

type Eval (IsNothing ('Just _a) :: 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 (Null ('[] :: [a]) :: Bool -> Type)

Defined in Fcf.Data.List

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

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

Defined in Fcf.Data.List

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

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) = 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 (a >= b :: Bool -> Type)

Defined in Fcf.Data.Nat

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

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 (DelayErrorFcf a2 :: a1 -> Type)

Defined in Type.Errors

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

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 (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 (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 (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 (Elem a2 as :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (Elem a2 as :: Bool -> Type) = Eval ((IsJust :: Maybe Nat -> Bool -> Type) =<< FindIndex (TyEq a2 :: a1 -> Bool -> Type) as)

type Eval (IsInfixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsInfixOf xs ys :: Bool -> Type) = Eval ((Any (IsPrefixOf xs) :: [[a]] -> Bool -> Type) =<< Tails ys)

type Eval (IsPrefixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsPrefixOf xs ys :: Bool -> Type) = IsPrefixOf_ xs ys

type Eval (IsSuffixOf xs ys :: Bool -> Type)

Defined in Fcf.Data.List

type Eval (IsSuffixOf xs ys :: Bool -> Type) = Eval (IsPrefixOf ((Reverse :: [a] -> [a] -> Type) @@ xs) ((Reverse :: [a] -> [a] -> Type) @@ ys))

type Eval (Concat xs :: a -> Type)

Defined in Fcf.Class.Foldable

type Eval (Concat xs :: a -> Type) = Eval (FoldMap (Pure :: a -> a -> Type) xs)

type Eval (x .<> y :: a -> Type)

Defined in Fcf.Class.Monoid

type Eval (x .<> y :: a -> Type) = x <> y

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 (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 (All p lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (All p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (&&)) 'True lst)

type Eval (Any p lst :: Bool -> Type)

Defined in Fcf.Class.Foldable

type Eval (Any p lst :: Bool -> Type) = Eval (Foldr (Bicomap p (Pure :: Bool -> Bool -> Type) (||)) 'False lst)

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 'False :: a -> Type)

Defined in Fcf.Data.Bool

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

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 (f $ a3 :: a1 -> Type)

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

type Eval (e >>= k :: a1 -> Type)

Defined in Fcf.Combinators

type Eval (e >>= k :: a1 -> Type) = Eval (k (Eval e))

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

type Eval (x & f :: a1 -> Type)

Defined in Fcf.Data.Function

type Eval (x & f :: a1 -> Type) = Eval (f x)

type Eval (Case ms a :: k -> Type)

Defined in Fcf.Utils

type Eval (Case ms a :: k -> Type) = Case_ ms a

type Eval (FoldMap f ('Left _a :: Either a3 a2) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Left _a :: Either a3 a2) :: a1 -> Type) = MEmpty :: a1

type Eval (FoldMap f ('Right x :: Either a3 a2) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Right x :: Either a3 a2) :: a1 -> Type) = Eval (f x)

type Eval (FoldMap f ('Just x) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Just x) :: a1 -> Type) = Eval (f x)

type Eval (FoldMap f ('Nothing :: Maybe a2) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('Nothing :: Maybe a2) :: a1 -> Type) = MEmpty :: a1

type Eval (FoldMap f (x ': xs) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f (x ': xs) :: a1 -> Type) = Eval (f x) <> Eval (FoldMap f xs)

type Eval (FoldMap f ('[] :: [a2]) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (FoldMap f ('[] :: [a2]) :: a1 -> Type) = MEmpty :: a1

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

Defined in Fcf.Data.Common

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

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

Defined in Fcf.Data.Common

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

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

Defined in Fcf.Data.Common

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

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

Defined in Fcf.Data.List

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

type Eval (Foldr f y ('Left _a :: Either a3 a2) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Left _a :: Either a3 a2) :: a1 -> Type) = y

type Eval (Foldr f y ('Right x :: Either a3 a2) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Right x :: Either a3 a2) :: a1 -> Type) = Eval (f x y)

type Eval (Foldr f y ('Just x) :: a1 -> Type)

Defined in Fcf.Class.Foldable

type Eval (Foldr f y ('Just x) :: a1 -> Type) = Eval (f x y)

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

Defined in Fcf.Class.Foldable

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

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

Defined in Fcf.Class.Foldable

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

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

Defined in Fcf.Class.Foldable

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

type Eval (Pure2 f x y :: a1 -> Type) = f x 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 (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 (On r f x y :: a1 -> Type)

Defined in Fcf.Data.Function

type Eval (On r f x y :: a1 -> Type) = Eval (r (Eval (f x)) (Eval (f y)))

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

Defined in Fcf.Combinators

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

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

Defined in Fcf.Combinators

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

type Eval (Bicomap f g r x y :: a1 -> Type)

Defined in Fcf.Data.Function

type Eval (Bicomap f g r x y :: a1 -> Type) = Eval (r (Eval (f x)) (Eval (g y)))

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 (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] :: Maybe [a1] -> Type)

Defined in Fcf.Data.List

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

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 ('[] :: [a]) :: Maybe a -> Type)

Defined in Fcf.Data.List

type Eval (Last ('[] :: [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 (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] :: Maybe a1 -> Type)

Defined in Fcf.Data.List

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

type Eval (Tails ('[] :: [a]) :: [[a]] -> Type)

Defined in Fcf.Data.List

type Eval (Tails ('[] :: [a]) :: [[a]] -> Type) = '[] :: [[a]]

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

Defined in Fcf.Data.List

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

type Eval (Reverse l :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Reverse l :: [a] -> Type) = Eval (Rev l ('[] :: [a]))

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 (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 (NumIter a s :: Maybe (k, Nat) -> Type)

Defined in Fcf.Data.List

type Eval (NumIter a s :: Maybe (k, Nat) -> Type) = If (Eval (s > 0)) ('Just '(a, s - 1)) ('Nothing :: Maybe (k, Natural))

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 (Find p (a2 ': as) :: Maybe a1 -> Type)

Defined in Fcf.Data.List

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

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

Defined in Fcf.Data.List

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

type Eval (Drop n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Drop n as :: [a] -> Type) = Drop_ n as

type Eval (DropWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) (DropWhile p xs) (Pure (x ': xs)))

type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (DropWhile p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

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

Defined in Fcf.Data.List

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

type Eval (Intercalate xs xss :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intercalate xs xss :: [a] -> Type) = Eval ((Concat :: [[a]] -> [a] -> Type) =<< Intersperse xs xss)

type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse _1 ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (Intersperse sep (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Intersperse sep (x ': xs) :: [a] -> Type) = x ': Eval (PrependToAll sep xs)

type Eval (PrependToAll _1 ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (PrependToAll _1 ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

type Eval (PrependToAll sep (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (PrependToAll sep (x ': xs) :: [a] -> Type) = sep ': (x ': Eval (PrependToAll sep xs))

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

Defined in Fcf.Data.List

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

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

Defined in Fcf.Data.List

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

type Eval (Take n as :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Take n as :: [a] -> Type) = Take_ n as

type Eval (TakeWhile p (x ': xs) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p (x ': xs) :: [a] -> Type) = Eval (If (Eval (p x)) ('(:) x <$> TakeWhile p xs) (Pure ('[] :: [a])))

type Eval (TakeWhile p ('[] :: [a]) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (TakeWhile p ('[] :: [a]) :: [a] -> Type) = '[] :: [a]

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

Defined in Fcf.Data.List

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

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

Defined in Fcf.Data.List

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

type Eval (Replicate n a2 :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (Replicate n a2 :: [a1] -> Type) = Eval (Unfoldr (NumIter a2) n)

type Eval (Snoc lst a :: [k] -> Type)

Defined in Fcf.Data.List

type Eval (Snoc lst a :: [k] -> Type) = Eval (lst ++ '[a])

type Eval (Lookup a as :: Maybe b -> Type)

Defined in Fcf.Data.List

type Eval (Lookup a as :: Maybe b -> Type) = Eval (Map (Snd :: (k, b) -> b -> Type) (Eval (Find ((TyEq a :: k -> Bool -> Type) <=< (Fst :: (k, b) -> k -> Type)) as)))

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

Defined in Fcf.Data.List

type Eval (Zip as bs :: [(a, b)] -> Type) = Eval (ZipWith (Pure2 ('(,) :: a -> b -> (a, b))) as bs)

type Eval (Unfoldr f c :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (Unfoldr f c :: [a] -> Type) = Eval (UnfoldrCase f (f @@ c))

type Eval (UnfoldrCase _1 ('Nothing :: Maybe (a, b)) :: [a] -> Type)

Defined in Fcf.Data.List

type Eval (UnfoldrCase _1 ('Nothing :: Maybe (a, b)) :: [a] -> Type) = '[] :: [a]

type Eval (UnfoldrCase f ('Just ab) :: [a1] -> Type)

Defined in Fcf.Data.List

type Eval (UnfoldrCase f ('Just ab) :: [a1] -> Type) = Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))

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 ('Just a3) :: Maybe a1 -> Type)

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

type Eval (ConcatMap f xs :: [b] -> Type)

Defined in Fcf.Class.Foldable

type Eval (ConcatMap f xs :: [b] -> Type) = Eval (FoldMap f xs)

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Data.List

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

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 (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 (Break p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Break p lst :: ([a], [a]) -> Type) = Eval (Span (Not <=< p) lst)

type Eval (Partition p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Partition p lst :: ([a], [a]) -> Type) = Eval (Foldr (PartHelp p) '('[] :: [a], '[] :: [a]) lst)

type Eval (Span p lst :: ([a], [a]) -> Type)

Defined in Fcf.Data.List

type Eval (Span p lst :: ([a], [a]) -> Type) = '(Eval (TakeWhile p lst), Eval (DropWhile p lst))

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 (PartHelp p a2 '(xs, ys) :: ([a1], [a1]) -> Type)

Defined in Fcf.Data.List

type Eval (PartHelp p a2 '(xs, ys) :: ([a1], [a1]) -> Type) = If (Eval (p a2)) '(a2 ': xs, ys) '(xs, a2 ': ys)

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

Defined in Fcf.Data.List

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Data.Common

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

type Eval (Second g x :: f a' b' -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (Second g x :: f a' b' -> Type) = Eval (Bimap (Pure :: a' -> a' -> Type) g x)

type Eval (First f2 x :: f1 a' b' -> Type)

Defined in Fcf.Class.Bifunctor

type Eval (First f2 x :: f1 a' b' -> Type) = Eval (Bimap f2 (Pure :: b' -> b' -> Type) x)

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

Defined in Fcf.Class.Bifunctor

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

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

Defined in Fcf.Class.Bifunctor

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

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

Defined in Fcf.Class.Bifunctor

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

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

Defined in Fcf.Class.Functor

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

data Pure (b :: a) (c :: a)

Instances

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

Defined in Fcf.Combinators

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