Language.Haskell.TH.Typecheck

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.

Documentation

type MonadTc m = (Quasi m, MonadState TcScope m)

Constraints for the typechecking monad. You probably want to use m ~ StateT TcScope Q

data TcScope

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

Execute a typechecker computation. Unificational variables will not persist between different runTc blocks.

type TV = Name

Type variable.

freshUnifTV :: MonadTc m => m TV

Make a fresh (unused) unificational type variable. Unification will be able to replace this type variable with a concrete type.

class HasTV a where

A class for thigns that contain type variables.

Minimal complete definition

instantiating, occurrences

Methods

instantiate :: MonadTc m => a -> m a

Replace all free variables with fresh unificational type variables.

instantiating :: MonadTc m => a -> StateT (Map TV TV) m a

Replace all free variables with fresh unificational type variables, in a state transformer.

occurrences :: a -> Set TV

Free variables.

Instances

HasTV Type

Defined in Language.Haskell.TH.Typecheck

Methods

instantiate :: MonadTc m => Type -> m Type

instantiating :: MonadTc m => Type -> StateT (Map TV TV) m Type

occurrences :: Type -> Set TV

HasTV Name

Defined in Language.Haskell.TH.Typecheck

Methods

instantiate :: MonadTc m => Name -> m Name

instantiating :: MonadTc m => Name -> StateT (Map TV TV) m Name

occurrences :: Name -> Set TV

HasTV a => HasTV [a]

Defined in Language.Haskell.TH.Typecheck

Methods

instantiate :: MonadTc m => [a] -> m [a]

instantiating :: MonadTc m => [a] -> StateT (Map TV TV) m [a]

occurrences :: [a] -> Set TV

(HasTV a, HasTV b) => HasTV (a, b)

Defined in Language.Haskell.TH.Typecheck

Methods

instantiate :: MonadTc m => (a, b) -> m (a, b)

instantiating :: MonadTc m => (a, b) -> StateT (Map TV TV) m (a, b)

occurrences :: (a, b) -> Set TV

extractKind :: MonadTc m => Type -> m Kind

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 ()

Assert that two types are equal, and replace unificational variables as necessary. Throws an error if the two types cannot be shown equal.

unifyTys :: MonadTc m => [Type] -> [Type] -> m ()

Assert that two lists of types are equal, replace unificational variables as necessary. Throws an error if two corresponding types could not be shown to be equal, or if lists have different lengths.

data UnifyResult

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

Defined in Language.Haskell.TH.Typecheck

Methods

(==) :: UnifyResult -> UnifyResult -> Bool

(/=) :: UnifyResult -> UnifyResult -> Bool

Ord UnifyResult

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

Defined in Language.Haskell.TH.Typecheck

Methods

showsPrec :: Int -> UnifyResult -> ShowS

show :: UnifyResult -> String

showList :: [UnifyResult] -> ShowS

unifyTyResult :: MonadTc m => Type -> Type -> m UnifyResult

Attempt unification and return an indication of whether the types were equal or not.

unifyTysResult :: MonadTc m => [Type] -> [Type] -> m UnifyResult

Attempt unifying two lists of types. If any two corresponding types in the lists are apart, returns Apart. If the lists are of different lengths, returns Apart.

extractSubst :: MonadTc m => Type -> m [(TV, Type)]

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

Recursively replace all zonked unificational variables in the type.