Safe Haskell  None 

Language  Haskell2010 
This module provides useful tools for writing better typeerrors. For
a quickstart guide to the underlying TypeError
machinery,
check out Dmitrii Kovanikov's excellent blog post
A story told by Type Errors.
Synopsis
 data ErrorMessage where
 Text :: forall. Symbol > ErrorMessage
 ShowType :: forall t. t > ErrorMessage
 (:<>:) :: forall. ErrorMessage > ErrorMessage > ErrorMessage
 (:$$:) :: forall. ErrorMessage > ErrorMessage > ErrorMessage
 type family PrettyPrintList (vs :: [k]) :: ErrorMessage where ...
 type family ShowTypeQuoted (t :: k) :: ErrorMessage where ...
 type family TypeError (a :: ErrorMessage) :: b where ...
 type DelayError err = Eval (DelayErrorFcf err)
 data DelayErrorFcf :: ErrorMessage > Exp k
 type NoError = (() :: Constraint)
 type NoErrorFcf = Pure NoError
 type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where ...
 type WhenStuck expr b = IfStuck expr b NoErrorFcf
 type UnlessStuck expr c = IfStuck expr NoError c
 te :: Q Type > Q Type
 type family PHANTOM :: k
 type family UnlessPhantom :: k > ErrorMessage > Constraint
 type family Subst :: k1 > k1 > k2 > k2
 type family VAR :: k
 type family SubstVar :: k1 > k2 > k2
 type Exp a = a > Type
 type family Eval (e :: Exp a) :: a
 data Pure (b :: a) (c :: a) :: forall a. a > a > Type
Generating Error Messages
data ErrorMessage where #
A description of a custom type error.
Text :: forall. Symbol > ErrorMessage  Show the text as is. 
ShowType :: forall t. t > ErrorMessage  Pretty print the type.

(:<>:) :: 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
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 ... 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
ShowTypeQuoted (t :: Symbol) = ShowType t  
ShowTypeQuoted t = (Text "'" :<>: ShowType t) :<>: Text "'" 
Emitting Error Messages
type family TypeError (a :: ErrorMessage) :: b where ... #
The typelevel 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 nonexistent 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 righthand side of a typelevel 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: base4.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 firstclass 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 #  
Defined in Type.Errors 
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 firstclass 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 #
leaves IfStuck
expr b cb
in the residual constraints whenever
expr
is stuck, otherwise it Eval
uates 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 firstclass family, which allows you to perform
arbitrarilycomplicated typelevel 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
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 usecase.
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 noop 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 metavariable 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
.
determines if the type described by UnlessPhantom
expr errexpr
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
.
substitutes all instances of Subst
expr a ba
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 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 metavariable 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 family Eval (e :: Exp a) :: a #
Expression evaluator.
Instances
type Eval (Not False)  
Defined in Fcf.Data.Bool  
type Eval (Not True)  
Defined in Fcf.Data.Bool  
type Eval (Constraints (a ': as) :: Constraint > Type)  
Defined in Fcf.Utils  
type Eval (Constraints ([] :: [Constraint]))  
Defined in Fcf.Utils  
type Eval (Null (a2 ': as) :: Bool > Type)  
type Eval (Null ([] :: [a]) :: Bool > Type)  
type Eval (a <= b :: Bool > Type)  
type Eval (a >= b :: Bool > Type)  
type Eval (a < b :: Bool > Type)  
type Eval (a > b :: Bool > Type)  
type Eval (False  b :: Bool > Type)  
type Eval (True  b :: Bool > Type)  
type Eval (a  False :: Bool > Type)  
type Eval (a  True :: Bool > Type)  
type Eval (False && b :: Bool > Type)  
type Eval (True && b :: Bool > Type)  
type Eval (a && True :: Bool > Type)  
type Eval (a && False :: Bool > Type)  
type Eval (IsNothing (Nothing :: Maybe a) :: Bool > Type)  
type Eval (IsNothing (Just _a) :: Bool > Type)  
type Eval (IsJust (Nothing :: Maybe a) :: Bool > Type)  
type Eval (IsJust (Just _a) :: Bool > Type)  
type Eval (Length (a2 ': as) :: Nat > Type)  
type Eval (Length ([] :: [a]) :: Nat > Type)  
Defined in Fcf.Data.List  
type Eval (a + b :: Nat > Type)  
type Eval (a  b :: Nat > Type)  
type Eval (a * b :: Nat > Type)  
type Eval (a ^ b :: Nat > Type)  
type Eval (DelayErrorFcf a2 :: a1 > Type) Source #  
Defined in Type.Errors  
type Eval (Error msg :: a > Type)  
type Eval (TError msg :: a > Type)  
type Eval (Pure x :: a > Type)  
Defined in Fcf.Combinators  
type Eval (Join e :: a > Type)  
type Eval (IsLeft (Right _a :: Either a b) :: Bool > Type)  
type Eval (IsLeft (Left _a :: Either a b) :: Bool > Type)  
type Eval (IsRight (Right _a :: Either a b) :: Bool > Type)  
type Eval (IsRight (Left _a :: Either a b) :: Bool > Type)  
type Eval (Fst ((,) a2 _b) :: a1 > Type)  
Defined in Fcf.Data.Common  
type Eval (Snd ((,) _a b) :: a1 > Type)  
Defined in Fcf.Data.Common  
type Eval (FromMaybe _a (Just b) :: a > Type)  
Defined in Fcf.Data.Common  
type Eval (FromMaybe a2 (Nothing :: Maybe a1) :: a1 > Type)  
type Eval (TyEq a b :: Bool > Type)  
type Eval (UnBool fal tru True :: a > Type)  
type Eval (UnBool fal tru False :: a > Type)  
type Eval (Guarded x ((p := y) ': ys) :: a2 > Type)  
type Eval (Pure1 f x :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval (k =<< e :: a2 > Type)  
type Eval (f <$> e :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval (f <*> e :: a2 > Type)  
type Eval (ConstFn a2 _b :: a1 > Type)  
Defined in Fcf.Combinators  
type Eval (f $ a3 :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval (Foldr f y (x ': xs) :: a2 > Type)  
type Eval (Foldr f y ([] :: [a1]) :: a2 > Type)  
Defined in Fcf.Data.List  
type Eval (UnList y f xs :: a2 > Type)  
type Eval (Uncurry f ((,) x y) :: a2 > Type)  
type Eval (UnMaybe y f (Just x) :: a2 > Type)  
type Eval (UnMaybe y f (Nothing :: Maybe a1) :: a2 > Type)  
type Eval (UnEither f g (Right y :: Either a2 b) :: a1 > Type)  
type Eval (UnEither f g (Left x :: Either a2 b) :: a1 > Type)  
type Eval (Pure2 f x y :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval ((f <=< g) x :: a3 > Type)  
type Eval (LiftM2 f x y :: a3 > Type)  
type Eval (Flip f y x :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval (Pure3 f x y z :: a2 > Type)  
Defined in Fcf.Combinators  
type Eval (LiftM3 f x y z :: a4 > Type)  
type Eval (Init (a2 ': (b ': as)) :: Maybe [a1] > Type)  
type Eval (Init (a2 ': ([] :: [a1])) :: Maybe [a1] > Type)  
type Eval (Init ([] :: [a]) :: Maybe [a] > Type)  
type Eval (Tail (_a ': as) :: Maybe [a] > Type)  
type Eval (Tail ([] :: [a]) :: Maybe [a] > Type)  
type Eval (Head (a2 ': _as) :: Maybe a1 > Type)  
type Eval (Head ([] :: [a]) :: Maybe a > Type)  
type Eval (Last (a2 ': (b ': as)) :: Maybe a1 > Type)  
type Eval (Last (a2 ': ([] :: [a1])) :: Maybe a1 > Type)  
type Eval (Last ([] :: [a]) :: Maybe a > Type)  
type Eval (Cons a2 as :: [a1] > Type)  
Defined in Fcf.Data.List  
type Eval ((x ': xs) ++ ys :: [a] > Type)  
type Eval (([] :: [a]) ++ ys :: [a] > Type)  
Defined in Fcf.Data.List  
type Eval (Filter p (a2 ': as) :: [a1] > Type)  
type Eval (Filter _p ([] :: [a]) :: [a] > Type)  
Defined in Fcf.Data.List  
type Eval (FindIndex p (a2 ': as) :: Maybe Nat > Type)  
type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat > Type)  
type Eval (Find p (a2 ': as) :: Maybe a1 > Type)  
type Eval (Find _p ([] :: [a]) :: Maybe a > Type)  
type Eval (SetIndex n a' as :: [k] > Type)  
Defined in Fcf.Data.List  
type Eval (Map f (a2 ': as) :: [b] > Type)  
type Eval (Map f ([] :: [a]) :: [b] > Type)  
Defined in Fcf.Classes  
type Eval (Map f (Just a3) :: Maybe a2 > Type)  
type Eval (Map f (Nothing :: Maybe a) :: Maybe b > Type)  
type Eval (ZipWith f (a2 ': as) (b2 ': bs) :: [c] > Type)  
type Eval (ZipWith _f _as ([] :: [b]) :: [c] > Type)  
Defined in Fcf.Data.List  
type Eval (ZipWith _f ([] :: [a]) _bs :: [c] > Type)  
Defined in Fcf.Data.List  
type Eval (Unzip as :: ([a], [b]) > Type)  
type Eval (Cons2 ((,) a3 b) ((,) as bs) :: ([a2], [a1]) > Type)  
type Eval (Map f (Right a3 :: Either a2 a1) :: Either a2 b > Type)  
type Eval (Map f (Left x :: Either a2 a1) :: Either a2 b > Type)  
type Eval (Map f ((,) x a2) :: (k2, k1) > Type)  
type Eval ((f *** f') ((,) b2 b'2) :: (k2, k1) > Type)  
type Eval (Bimap f g (Right y :: Either a b1) :: Either a' b2 > Type)  
type Eval (Bimap f g (Left x :: Either a1 b) :: Either a2 b' > Type)  
type Eval (Bimap f g ((,) x y) :: (k2, k1) > Type)  
type Eval (Map f ((,,) x y a2) :: (k2, k3, k1) > Type)  
type Eval (Map f ((,,,) x y z a2) :: (k2, k3, k4, k1) > Type)  
type Eval (Map f ((,,,,) x y z w a2) :: (k2, k3, k4, k5, k1) > Type)  