type-errors-0.2.0.0: Tools for writing better type errors

Safe HaskellNone
LanguageHaskell2010

Type.Errors

Contents

Description

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.

Synopsis

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 ... Source #

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

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

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) Source #

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 Source #

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) Source # 
Instance details

Defined in Type.Errors

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

type NoError = (() :: Constraint) Source #

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 Source #

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 ... Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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
...
... No instance for (Show (f0 p0 -> ()))
...

Since: 0.2.0.0

Performing Type Substitutions

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

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 Source #

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 Source #

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) 
Instance details

Defined in Fcf.Data.Bool

type Eval (Not False) = True
type Eval (Not True) 
Instance details

Defined in Fcf.Data.Bool

type Eval (Not True) = False
type Eval (Constraints (a ': as) :: Constraint -> Type) 
Instance details

Defined in Fcf.Utils

type Eval (Constraints (a ': as) :: Constraint -> Type) = (a, Eval (Constraints as))
type Eval (Constraints ([] :: [Constraint])) 
Instance details

Defined in Fcf.Utils

type Eval (Constraints ([] :: [Constraint])) = ()
type Eval (Null (a2 ': as) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Null (a2 ': as) :: Bool -> Type) = False
type Eval (Null ([] :: [a]) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Null ([] :: [a]) :: Bool -> Type) = True
type Eval (a <= b :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))
type Eval (False || b :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

type Eval (True || b :: Bool -> Type) = True
type Eval (a || False :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

type Eval (a || True :: Bool -> Type) = True
type Eval (False && b :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

type Eval (a && False :: Bool -> Type) = False
type Eval (IsNothing (Nothing :: Maybe a) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (IsNothing (Nothing :: Maybe a) :: Bool -> Type) = True
type Eval (IsNothing (Just _a) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (IsNothing (Just _a) :: Bool -> Type) = False
type Eval (IsJust (Nothing :: Maybe a) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (IsJust (Nothing :: Maybe a) :: Bool -> Type) = False
type Eval (IsJust (Just _a) :: Bool -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (IsJust (Just _a) :: Bool -> Type) = True
type Eval (Length (a2 ': as) :: Nat -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ([] :: [a]) :: Nat -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Length ([] :: [a]) :: Nat -> Type) = 0
type Eval (a + b :: Nat -> Type) 
Instance details

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

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

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b
type Eval (DelayErrorFcf a2 :: a1 -> Type) Source # 
Instance details

Defined in Type.Errors

type Eval (DelayErrorFcf a2 :: a1 -> Type) = (TypeError a2 :: a1)
type Eval (Error msg :: a -> Type) 
Instance details

Defined in Fcf.Utils

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

Defined in Fcf.Utils

type Eval (TError msg :: a -> Type) = (TypeError msg :: a)
type Eval (Pure x :: a -> Type) 
Instance details

Defined in Fcf.Combinators

type Eval (Pure x :: a -> Type) = x
type Eval (Join e :: a -> Type) 
Instance details

Defined in Fcf.Combinators

type Eval (Join e :: a -> Type) = Eval (Eval e)
type Eval (IsLeft (Right _a :: Either a b) :: Bool -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Data.Common

type Eval (IsRight (Left _a :: Either a b) :: Bool -> Type) = False
type Eval (Fst ((,) a2 _b) :: a1 -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (Fst ((,) a2 _b) :: a1 -> Type) = a2
type Eval (Snd ((,) _a b) :: a1 -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (Snd ((,) _a b) :: a1 -> Type) = b
type Eval (FromMaybe _a (Just b) :: a -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (FromMaybe _a (Just b) :: a -> Type) = b
type Eval (FromMaybe a2 (Nothing :: Maybe a1) :: a1 -> Type) 
Instance details

Defined in Fcf.Data.Common

type Eval (FromMaybe a2 (Nothing :: Maybe a1) :: a1 -> Type) = a2
type Eval (TyEq a b :: Bool -> Type) 
Instance details

Defined in Fcf.Utils

type Eval (TyEq a b :: Bool -> Type) = TyEqImpl a b
type Eval (UnBool fal tru True :: a -> Type) 
Instance details

Defined in Fcf.Data.Bool

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

Defined in Fcf.Data.Bool

type Eval (UnBool fal tru False :: a -> Type) = Eval fal
type Eval (Guarded x ((p := y) ': ys) :: a2 -> Type) 
Instance details

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) 
Instance details

Defined in Fcf.Combinators

type Eval (Pure1 f x :: a2 -> Type) = f x
type Eval (k =<< e :: a2 -> Type) 
Instance details

Defined in Fcf.Combinators

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

Defined in Fcf.Combinators

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

Defined in Fcf.Combinators

type Eval (f <*> e :: a2 -> Type) = Eval f (Eval e)
type Eval (ConstFn a2 _b :: a1 -> Type) 
Instance details

Defined in Fcf.Combinators

type Eval (ConstFn a2 _b :: a1 -> Type) = a2
type Eval (f $ a3 :: a2 -> Type) 
Instance details

Defined in Fcf.Combinators

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

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) 
Instance details

Defined in Fcf.Data.List

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

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Combinators

type Eval (Pure2 f x y :: a2 -> Type) = f x y
type Eval ((f <=< g) x :: a3 -> Type) 
Instance details

Defined in Fcf.Combinators

type Eval ((f <=< g) x :: a3 -> Type) = Eval (f (Eval (g x)))
type Eval (LiftM2 f x y :: a3 -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Data.List

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

Defined in Fcf.Data.List

type Eval (Init ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])
type Eval (Tail (_a ': as) :: Maybe [a] -> Type) 
Instance details

Defined in Fcf.Data.List

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

Defined in Fcf.Data.List

type Eval (Tail ([] :: [a]) :: Maybe [a] -> Type) = (Nothing :: Maybe [a])
type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Head (a2 ': _as) :: Maybe a1 -> Type) = Just a2
type Eval (Head ([] :: [a]) :: Maybe a -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Head ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval (Last (a2 ': (b ': as)) :: Maybe a1 -> Type) 
Instance details

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) 
Instance details

Defined in Fcf.Data.List

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

Defined in Fcf.Data.List

type Eval (Last ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval (Cons a2 as :: [a1] -> Type) 
Instance details

Defined in Fcf.Data.List

type Eval (Cons a2 as :: [a1] -> Type) = a2 ': as
type Eval ((x ': xs) ++ ys :: [a] -> Type) 
Instance details

Defined in Fcf.Data.List

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

Defined in Fcf.Data.List

type Eval (([] :: [a]) ++ ys :: [a] -> Type) = ys
type Eval (Filter p (a2 ': as) :: [a1] -> Type) 
Instance details

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) 
Instance details

Defined in Fcf.Data.List

type Eval (Filter _p ([] :: [a]) :: [a] -> Type) = ([] :: [a])
type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Data.List

type Eval (Find _p ([] :: [a]) :: Maybe a -> Type) = (Nothing :: Maybe a)
type Eval (SetIndex n a' as :: [k] -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Classes

type Eval (Map f ([] :: [a]) :: [b] -> Type) = ([] :: [b])
type Eval (Map f (Just a3) :: Maybe a2 -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Data.List

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

Defined in Fcf.Data.List

type Eval (ZipWith _f ([] :: [a]) _bs :: [c] -> Type) = ([] :: [c])
type Eval (Unzip as :: ([a], [b]) -> Type) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

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) 
Instance details

Defined in Fcf.Combinators

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