-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Solve type equalities using custom type-level rewrite rules
--
-- A typechecker plugin which allows the user to specify a set of
-- domain-specific rewrite rules. These get applied whenever the compiler
-- is unable to solve a type equality constraint, in the hope that the
-- rewritten equality constraint will be easier to solve.
@package typelevel-rewrite-rules
@version 1.0
module TypeLevel.Append
type family (++) as bs
type RightIdentity as = (as ++ '[]) ~ as
type RightAssociative as bs cs = ((as ++ bs) ++ cs) ~ (as ++ (bs ++ cs))
module TypeLevel.Rewrite.Internal.DecomposedConstraint
data DecomposedConstraint a
EqualityConstraint :: a -> a -> DecomposedConstraint a
InstanceConstraint :: Class -> [a] -> DecomposedConstraint a
asEqualityConstraint :: Ct -> Maybe (Type, Type)
asInstanceConstraint :: Ct -> Maybe (Class, [Type])
asDecomposedConstraint :: Ct -> Maybe (DecomposedConstraint Type)
fromDecomposeConstraint :: DecomposedConstraint Type -> Type
instance Data.Traversable.Traversable TypeLevel.Rewrite.Internal.DecomposedConstraint.DecomposedConstraint
instance Data.Foldable.Foldable TypeLevel.Rewrite.Internal.DecomposedConstraint.DecomposedConstraint
instance GHC.Base.Functor TypeLevel.Rewrite.Internal.DecomposedConstraint.DecomposedConstraint
module TypeLevel.Rewrite.Internal.Lookup
lookupModule :: String -> TcPluginM Module
lookupTyCon :: String -> String -> TcPluginM TyCon
lookupDataCon :: String -> String -> TcPluginM DataCon
splitFirstDot :: String -> Maybe (String, String)
splitLastDot :: String -> Maybe (String, String)
lookupFQN :: String -> TcPluginM TyCon
module TypeLevel.Rewrite.Internal.Term
-- | an expression like (as ++ '[]) ++ bs would be represented as
-- Fun appendTyCon [Var "as", Fun nilTyCon [] or rather Fun
-- appendTyCon [Fun starTyCon [], Var "as", Fun nilTyCon [Fun starTyCon
-- []] because those polymorphic TyCons need to be specialized to
-- the * kind
atomTerm :: f -> Term f v
module TypeLevel.Rewrite.Internal.TypeEq
-- | A newtype around Type which has an Eq instance.
newtype TypeEq
TypeEq :: Type -> TypeEq
[unTypeEq] :: TypeEq -> Type
instance GHC.Classes.Eq TypeLevel.Rewrite.Internal.TypeEq.TypeEq
module TypeLevel.Rewrite.Internal.TypeNode
data TypeNode
TyCon :: TyCon -> TypeNode
TyLit :: TypeEq -> TypeNode
toTypeNodeApp_maybe :: Type -> Maybe (TypeNode, [Type])
fromTypeNode :: TypeNode -> [Type] -> Type
instance GHC.Classes.Eq TypeLevel.Rewrite.Internal.TypeNode.TypeNode
module TypeLevel.Rewrite.Internal.TypeTemplate
type TypeTemplate = Term TypeNode TyVar
toTypeTemplate_maybe :: Type -> Maybe TypeTemplate
module TypeLevel.Rewrite.Internal.TypeRule
type TypeRule = Rule TypeNode TyVar
toTypeRule_maybe :: Type -> Maybe TypeRule
fromTyVar :: TyVar -> Type
fromTerm :: (f -> [Type] -> Type) -> (v -> Type) -> Term f v -> Type
fromTypeRule :: TypeRule -> Type
module TypeLevel.Rewrite.Internal.TypeTerm
type TypeTerm = Term TypeNode TypeEq
toTypeTerm :: Type -> TypeTerm
fromTypeTerm :: TypeTerm -> Type
module TypeLevel.Rewrite.Internal.TypeSubst
type TypeSubst = [(TypeEq, TypeTerm)]
module TypeLevel.Rewrite.Internal.PrettyPrint
pprMaybe :: (a -> String) -> Maybe a -> String
pprPair :: (a -> String) -> (b -> String) -> (a, b) -> String
pprList :: (a -> String) -> [a] -> String
pprTyCon :: TyCon -> String
pprType :: Type -> String
pprTyVar :: TyVar -> String
pprTypeEq :: TypeEq -> String
pprTerm :: (f -> String) -> (v -> String) -> Term f v -> String
pprRule :: (f -> String) -> (v -> String) -> Rule f v -> String
pprReduct :: (f -> String) -> (v -> String) -> (v' -> String) -> Reduct f v v' -> String
pprTypeNode :: TypeNode -> String
pprTypeSubst :: TypeSubst -> String
pprTypeTemplate :: TypeTemplate -> String
pprTypeTerm :: TypeTerm -> String
pprTypeRule :: TypeRule -> String
pprTypeReduct :: Reduct TyCon TypeEq TyVar -> String
module TypeLevel.Rewrite.Internal.ApplyRules
type Subst = Map TyVar (Term TypeNode TypeEq)
applyRules :: Traversable t => TypeSubst -> [TypeRule] -> t TypeTerm -> Maybe (TypeRule, t TypeTerm)
multiRewrite :: TypeSubst -> [TypeRule] -> TypeTerm -> Maybe (TypeRule, TypeTerm)
singleRewrite :: TypeSubst -> TypeRule -> TypeTerm -> Maybe TypeTerm
topLevelRewrite :: TypeSubst -> TypeRule -> TypeTerm -> Maybe TypeTerm
traverseFirst :: Traversable t => (a -> Maybe a) -> t a -> Maybe (t a)
annotatedTraverseFirst :: Traversable t => (a -> Maybe (annotation, a)) -> t a -> Maybe (annotation, t a)
traverseAll :: Traversable t => (a -> Maybe a) -> t a -> [t a]
annotatedTraverseAll :: Traversable t => (a -> Maybe (annotation, a)) -> t a -> [(annotation, t a)]
module TypeLevel.Rewrite
plugin :: Plugin