| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Haskell.TH.Typecheck
Contents
Description
Poor man's typechecker in Template Haskell. Capable of working with type synonyms, type families, DataKinds, kind polymorphism.
Levity polymorphism is currently not supported. Return kind inference in type families is not supported.
GHC cannot reify roles correctly, so we cannot solve Coercible constraints correctly, so instance resolution was left out.
Synopsis
- type MonadTc m = (Quasi m, MonadState TcScope m)
- data TcScope
- runTc :: Monad m => StateT TcScope m a -> m a
- type TV = Name
- freshUnifTV :: MonadTc m => m TV
- extractKind :: MonadTc m => Type -> m Kind
- unifyTy :: MonadTc m => Type -> Type -> m ()
- data UnifyResult
- unifyTyResult :: MonadTc m => Bool -> Type -> Type -> m UnifyResult
- extractSubst :: MonadTc m => Type -> m [(TV, Type)]
- substZonked :: MonadTc m => Type -> m Type
Documentation
Scope of the typechecker. Includes information about unificational vs rigid (skolem) type variables, and a cache of type information reified from GHC.
runTc :: Monad m => StateT TcScope m a -> m a Source #
Execute a typechecker computation. Unificational variables will not persist
between different runTc blocks.
freshUnifTV :: MonadTc m => m TV Source #
Make a fresh (unused) unificational type variable. Unification will be able to replace this type variable with a concrete type.
extractKind :: MonadTc m => Type -> m Kind Source #
Attempt to compute the kind of a type. GHC doesn't give us complete kind information so this migth be more general than expected.
unifyTy :: MonadTc m => Type -> Type -> m () Source #
Assert that two types are equal, and replace unificational variables as necessary. Throws an error if the two types cannot be shown equal.
data UnifyResult Source #
Result of unification
Constructors
| Apart String | The types are known to be different. (Includes an error message for if the types were expected to be equal). |
| Unknown String | The types may be different depending on substitutions of rigid type variables or not-yet-known type family instances. (Includes an error message for if the types were expected to be equal). |
| Equal | The types are known to be equal |
Instances
| Eq UnifyResult Source # | |
Defined in Language.Haskell.TH.Typecheck | |
| Ord UnifyResult Source # | |
Defined in Language.Haskell.TH.Typecheck Methods compare :: UnifyResult -> UnifyResult -> Ordering # (<) :: UnifyResult -> UnifyResult -> Bool # (<=) :: UnifyResult -> UnifyResult -> Bool # (>) :: UnifyResult -> UnifyResult -> Bool # (>=) :: UnifyResult -> UnifyResult -> Bool # max :: UnifyResult -> UnifyResult -> UnifyResult # min :: UnifyResult -> UnifyResult -> UnifyResult # | |
| Show UnifyResult Source # | |
Defined in Language.Haskell.TH.Typecheck Methods showsPrec :: Int -> UnifyResult -> ShowS # show :: UnifyResult -> String # showList :: [UnifyResult] -> ShowS # | |
Arguments
| :: MonadTc m | |
| => Bool | expand type familes? |
| -> Type | |
| -> Type | |
| -> m UnifyResult |
Attempt unification and return an indication of whether the types were equal or not.
extractSubst :: MonadTc m => Type -> m [(TV, Type)] Source #
Recursively collect all zonked (unified with a type) unificational variables in the type, into a substitution. This is a separate step because we cannot actually replace the variables as the data structure is immutable.
substZonked :: MonadTc m => Type -> m Type Source #
Recursively replace all zonked unificational variables in the type.