-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Constraint solving framework employed by the Helium Compiler.
--   
--   At its most general, Top is a framework for constructing abstract
--   interpretations which focuses on giving good feedback on why an
--   abstract interpretation does not give any useful information. In a
--   mathematical notation this is usually made explicit by returning the
--   top element of a (complete) lattice. This is also one of the reasons
--   for the name of the project.
@package Top
@version 1.7


-- | This module contains a data type to represent (plain) types, some
--   basic functionality for types, and an instance for Show.
module Top.Types.Primitive
type Tps = [Tp]

-- | A data type to represent monotypes. Note that <tt>Type</tt> is already
--   in use in the Unified Haskell Architecture (UHA) which is used in the
--   Helium compiler
data Tp

-- | The type variables are numbered.
TVar :: Int -> Tp

-- | A type constant is represented by a string.
TCon :: String -> Tp

-- | The application of two Top.Types. Not all types that can be
--   constructed are well-formed.
TApp :: Tp -> Tp -> Tp
intType, stringType, boolType, floatType, charType :: Tp

-- | Constructs a function type from one type to another. This operator is
--   left associative.
(.->.) :: Tp -> Tp -> Tp

-- | For instance, <tt>(listType intType)</tt> represents <tt>[Int]</tt>
listType :: Tp -> Tp

-- | For instance, <tt>(ioType boolType)</tt> represents <tt>(IO Bool)</tt>
ioType :: Tp -> Tp

-- | A cathesian product of zero or more Top.Types. For instance,
--   <tt>(tupleType [])</tt> represents <tt>()</tt>, and <tt>(tupleType
--   [charType, stringType])</tt> represents <tt>(Char,String)</tt>
tupleType :: Tps -> Tp

-- | The unit type. A special instance of of tuple type.
voidType :: Tp

-- | Returns the list of type variables of a type. (no duplicates)
variablesInType :: Tp -> [Int]

-- | Returns the list of type constants of a type. (no duplicates)
constantsInType :: Tp -> [String]

-- | Returns the left spine of a type. For instance, if type <tt>t</tt> is
--   <tt>Either Bool [Int]</tt>, then <tt>leftSpine t</tt> is
--   <tt>(Either,[Bool,[Int]])</tt>.
leftSpine :: Tp -> (Tp, Tps)

-- | Returns the right spine of a function type. For instance, if type
--   <tt>t</tt> is <tt>Int -&gt; (Bool -&gt; String)</tt>, then
--   <tt>functionSpine t</tt> is <tt>([Int,Bool],String)</tt>.
functionSpine :: Tp -> (Tps, Tp)

-- | Returns the right spine of a function type of a maximal length.
functionSpineOfLength :: Int -> Tp -> (Tps, Tp)

-- | Returns the arity of a type, that is, the number of expected
--   arguments.
arityOfTp :: Tp -> Int

-- | The priority of a type, primarily used for the insertion of
--   parentheses in pretty printing.
priorityOfType :: Tp -> Int

-- | All the type variables in a type are frozen by turning them into a
--   type constant. The integer numeral is prefixed with an underscore
--   ('_').
freezeVariablesInType :: Tp -> Tp

-- | Recover the type variables that are frozen in a type.
unfreezeVariablesInType :: Tp -> Tp
isTVar :: Tp -> Bool
isTCon :: Tp -> Bool
isTApp :: Tp -> Bool
isFunctionType :: Tp -> Bool
isTupleConstructor :: String -> Bool
isIOType :: Tp -> Bool
tpParser :: String -> [(Tp, String)]
class HasTypes a
getTypes :: HasTypes a => a -> Tps
changeTypes :: HasTypes a => (Tp -> Tp) -> a -> a
instance Eq Tp
instance Ord Tp
instance (HasTypes a, HasTypes b) => HasTypes (Either a b)
instance HasTypes a => HasTypes (Maybe a)
instance (HasTypes a, HasTypes b) => HasTypes (a, b)
instance HasTypes a => HasTypes [a]
instance HasTypes Tp
instance Read Tp
instance Show Tp


module Top.Ordering.TreeWalk
newtype TreeWalk
TreeWalk :: (forall a. List a -> [(List a, List a)] -> List a) -> TreeWalk
topDownTreeWalk :: TreeWalk
bottomUpTreeWalk :: TreeWalk
inorderTopFirstPreTreeWalk :: TreeWalk
inorderTopLastPreTreeWalk :: TreeWalk
inorderTopFirstPostTreeWalk :: TreeWalk
inorderTopLastPostTreeWalk :: TreeWalk
reverseTreeWalk :: TreeWalk -> TreeWalk
type List a = [a] -> [a]
concatList :: [List a] -> List a


module Top.Ordering.Tree
type Trees a = [Tree a]
data Tree a
Node :: (Trees a) -> Tree a
AddList :: Direction -> [a] -> (Tree a) -> Tree a
StrictOrder :: (Tree a) -> (Tree a) -> Tree a
Spread :: Direction -> [a] -> (Tree a) -> Tree a
Receive :: Int -> Tree a
Phase :: Int -> [a] -> Tree a
Chunk :: Int -> (Tree a) -> Tree a
emptyTree :: Tree a
unitTree :: a -> Tree a
listTree :: [a] -> Tree a
binTree :: Tree a -> Tree a -> Tree a
(.>., .<<., .<., .>>.) :: [a] -> Tree a -> Tree a
makeTreeHelper :: (t -> [a] -> t1 -> t1) -> t -> [a] -> t1 -> t1
data Direction
Up :: Direction
Down :: Direction
type Spreaded a = Map Int [a]
type Phased a = Map Int (List a)
flattenTree :: TreeWalk -> Tree a -> [a]
spreadTree :: (a -> Maybe Int) -> Tree a -> Tree a
phaseTree :: a -> Tree a -> Tree a
chunkTree :: Tree a -> [(Int, Tree a)]
instance Eq Direction
instance Show Direction
instance Show a => Show (Tree a)
instance Functor Tree


module Top.Monad.StateFix
type StateFix s = StateFixT s Identity
data StateFixT s m a
Fix :: StateT (s (StateFixT s m)) m a -> StateFixT s m a
unFix :: StateFixT s m a -> StateT (s (StateFixT s m)) m a
runStateFixT :: StateFixT s m a -> s (StateFixT s m) -> m (a, s (StateFixT s m))
evalStateFixT :: Monad m => StateFixT s m a -> s (StateFixT s m) -> m a
execStateFixT :: Monad m => StateFixT s m a -> s (StateFixT s m) -> m (s (StateFixT s m))
runStateFix :: StateFix s a -> s (StateFix s) -> (a, s (StateFix s))
evalStateFix :: StateFix s a -> s (StateFix s) -> a
execStateFix :: StateFix s a -> s (StateFix s) -> s (StateFix s)
instance MonadWriter w m => MonadWriter w (StateFixT s m)
instance MonadTrans (StateFixT s)
instance Monad m => MonadState (s (StateFixT s m)) (StateFixT s m)
instance Monad m => Monad (StateFixT s m)


module Top.Implementation.TypeGraph.Path
data Path a
(:|:) :: Path a -> Path a -> Path a
(:+:) :: Path a -> Path a -> Path a
Step :: a -> Path a
Fail :: Path a
Empty :: Path a
seqList, seqList1 :: [Path a] -> Path a
altList, altList1 :: [Path a] -> Path a

-- | Combine two monadic computations
mCombine :: Monad m => (a -> b -> c) -> m a -> m b -> m c
(<+>, <|>) :: Monad m => m (Path a) -> m (Path a) -> m (Path a)
(<++>) :: Monad m => m [Path a] -> m [Path a] -> m [Path a]
steps :: Path a -> [a]
mapPath :: (a -> b) -> Path a -> Path b
changeStep :: (a -> Path b) -> Path a -> Path b
changeStepM :: Monad m => (a -> m (Path b)) -> Path a -> m (Path b)
minCompleteInPath :: (a -> a -> Ordering) -> Path a -> Maybe a
simplifyPath :: Path a -> Path a
tailSharingBy :: (a -> a -> Ordering) -> Path a -> Path a
flattenPath :: Path a -> [[a]]
minimalSets :: (a -> a -> Bool) -> Path a -> [[a]]
removeSomeDuplicates :: Ord b => (a -> b) -> Path a -> Path a
participationMap :: Ord a => Path a -> (Integer, Map a Integer)
pathSize :: Path a -> Int

-- | The maximal number of equality paths that is returned by equalPaths
--   (although this number can be exceeded...it is more or less used as
--   approximation) Nothing indicates that there is no limit
maxNumberOfEqualPaths :: Maybe Int
reduceNumberOfPaths :: Path a -> Path a
limitNumberOfPaths :: Int -> Path a -> Path a
instance Show a => Show (Path a)


-- | This module contains a data type to represent (plain) types, some
--   basic functionality for types, and an instance for Show.
module Top.Types.Substitution
class Substitution s
lookupInt :: Substitution s => Int -> s -> Tp
removeDom :: Substitution s => [Int] -> s -> s
restrictDom :: Substitution s => [Int] -> s -> s
dom :: Substitution s => s -> [Int]
cod :: Substitution s => s -> Tps
class Substitutable a
(|->) :: (Substitutable a, Substitution s) => s -> a -> a
ftv :: Substitutable a => a -> [Int]

-- | The next type variable that is not free (default is zero)
nextFTV :: Substitutable a => a -> Int

-- | A substitution represented by a finite map.
type MapSubstitution = Map Int Tp
emptySubst :: MapSubstitution

-- | Compose two finite map substitutions: safe. Note for <a>union</a>:
--   bindings in right argument shadow those in the left
(@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution

-- | Compose two finite map substitutions: quick and dirty!
(@@@) :: MapSubstitution -> MapSubstitution -> MapSubstitution
singleSubstitution :: Int -> Tp -> MapSubstitution
listToSubstitution :: [(Int, Tp)] -> MapSubstitution

-- | A fixpoint is computed when looking up the target of a type variable
--   in this substitution. Combining two substitutions is cheap, whereas a
--   lookup is more expensive than the normal finite map substitution.
newtype FixpointSubstitution
FixpointSubstitution :: (Map Int Tp) -> FixpointSubstitution

-- | The empty fixpoint substitution
emptyFPS :: FixpointSubstitution

-- | Combine two fixpoint substitutions that are disjoint
disjointFPS :: FixpointSubstitution -> FixpointSubstitution -> FixpointSubstitution
wrapSubstitution :: Substitution substitution => substitution -> WrappedSubstitution
data WrappedSubstitution
WrappedSubstitution :: a -> (Int -> a -> Tp, [Int] -> a -> a, [Int] -> a -> a, a -> [Int], a -> Tps) -> WrappedSubstitution
freezeFTV :: Substitutable a => a -> a
allTypeVariables :: HasTypes a => a -> [Int]
allTypeConstants :: HasTypes a => a -> [String]
instance (Substitutable a, Substitutable b) => Substitutable (Either a b)
instance Substitutable a => Substitutable (Maybe a)
instance (Substitutable a, Substitutable b) => Substitutable (a, b)
instance Substitutable a => Substitutable [a]
instance Substitutable Tp
instance Substitution WrappedSubstitution
instance Substitution FixpointSubstitution
instance Substitution MapSubstitution


-- | Qualification of types (for instance, predicates to deal with type
--   classes).
module Top.Types.Qualification
newtype Qualification q a
Qualification :: (q, a) -> Qualification q a
split :: Qualification q a -> (q, a)
(.=>.) :: q -> a -> Qualification q a
qualifiers :: Qualification q a -> q
unqualify :: Qualification q a -> a
qualify :: (Substitutable context, Substitutable q, Substitutable a) => context -> [q] -> a -> Qualification [q] a
class Show a => ShowQualifiers a where showQualifiers = (: []) . show
showQualifiers :: ShowQualifiers a => a -> [String]
showContext :: ShowQualifiers a => a -> String
showContextSimple :: [String] -> String
instance ShowQualifiers a => ShowQualifiers [a]
instance (ShowQualifiers a, ShowQualifiers b) => ShowQualifiers (a, b)
instance (ShowQualifiers q, Show a) => Show (Qualification q a)
instance (HasTypes q, HasTypes a) => HasTypes (Qualification q a)
instance (Substitutable q, Substitutable a) => Substitutable (Qualification q a)


-- | Universal and existential quantification of types
module Top.Types.Quantification
newtype Quantification q a
Quantification :: ([Int], QuantorMap, a) -> Quantification q a
type QuantorMap = [(Int, String)]
withoutQuantors :: Quantification q a -> Bool
showQuantor :: Show q => Quantification q a -> String
noQuantifiers :: a -> Quantification q a
quantifiers :: Quantification q a -> [Int]
unquantify :: Quantification q a -> a
introduceTypeVariables :: Substitutable a => Int -> Quantification q a -> (Int, a)
introduceSkolemConstants :: Substitutable a => Int -> Quantification q a -> (Int, a)
bindTypeVariables :: Substitutable a => [Int] -> a -> Quantification q a
bindSkolemConstants :: HasSkolems a => [Int] -> a -> Quantification q a
getQuantorMap :: Quantification q a -> QuantorMap
data Universal
type Forall = Quantification Universal
instantiate, skolemize :: Substitutable a => Int -> Forall a -> (Int, a)
generalize :: (Substitutable context, Substitutable a) => context -> a -> Forall a
generalizeAll :: Substitutable a => a -> Forall a
quantify :: Substitutable a => [Int] -> a -> Forall a
unskolemize :: HasSkolems a => [Int] -> a -> Forall a
data Existential
type Exists = Quantification Existential
open, reveal :: Substitutable a => Int -> Exists a -> (Int, a)
close :: HasSkolems a => [Int] -> a -> Exists a
unreveal :: Substitutable a => [Int] -> a -> Exists a
skolemPrefix :: String
makeSkolemConstant :: Int -> Tp
fromSkolemString :: String -> Maybe Int
skolemizeFTV :: Substitutable a => a -> a
class HasSkolems a
allSkolems :: HasSkolems a => a -> [Int]
changeSkolems :: HasSkolems a => [(Int, Tp)] -> a -> a
data ShowQuantorOptions
ShowQuantorOptions :: Bool -> [String] -> String -> Bool -> Bool -> ShowQuantorOptions
showTopLevelQuantors :: ShowQuantorOptions -> Bool
dontUseIdentifiers :: ShowQuantorOptions -> [String]
variablePrefix :: ShowQuantorOptions -> String
showAllTheSame :: ShowQuantorOptions -> Bool
useTheNameMap :: ShowQuantorOptions -> Bool
defaultOptions :: ShowQuantorOptions
showQuantors :: ShowQuantors a => a -> String

-- | This class can deal with the pretty printing of (possibly nested)
--   quantifiers.
class Show a => ShowQuantors a where showQuantorsWithout = const show
showQuantorsWithout :: ShowQuantors a => ShowQuantorOptions -> a -> String

-- | List of unique identifiers.(a, b, .., z, a1, b1 .., z1, a2, ..)
variableList :: [String]
instance (Substitutable a, ShowQuantors a, Show q) => ShowQuantors (Quantification q a)
instance (Substitutable a, ShowQuantors a, Show q) => Show (Quantification q a)
instance ShowQuantors Tp
instance HasSkolems a => HasSkolems [a]
instance HasSkolems Tp
instance Show Existential
instance Show Universal
instance HasTypes a => HasTypes (Quantification q a)
instance Substitutable a => Substitutable (Quantification q a)


-- | This module contains type synonyms to represent type synonyms. A
--   collection of type synonyms can always be ordered, since (mutually)
--   recursive type synonyms are not permitted. The ordering of type
--   synonyms must be determined to find a minimal number of unfold steps
--   to make two types syntactically equivalent.
module Top.Types.Synonym

-- | A (unordered) collection of type synonyms is represented by a finite
--   map of strings (the name of the type synonym) to pairs that have an
--   int (the number of arguments of the type synonym) and a function.
type TypeSynonyms = Map String (Int, Tps -> Tp)

-- | An ordering of type synonyms maps a name of a type synonym to a
--   position in the ordering.
type TypeSynonymOrdering = Map String Int

-- | An (unordered) collection of type synonyms, together with an ordering.
type OrderedTypeSynonyms = (TypeSynonymOrdering, TypeSynonyms)

-- | An empty collection of ordered type synonyms.
noOrderedTypeSynonyms :: OrderedTypeSynonyms

-- | A string is a list of characters
stringAsTypeSynonym :: OrderedTypeSynonyms

-- | Order a collection of type synonyms, and return this ordering paired
--   with sets of mutually recursive type synonyms that are detected.
getTypeSynonymOrdering :: TypeSynonyms -> (TypeSynonymOrdering, [[String]])
isPhantomTypeSynonym :: OrderedTypeSynonyms -> String -> Bool

-- | Fully expand a type in a recursive way.
expandType :: TypeSynonyms -> Tp -> Tp

-- | Fully expand the top-level type constructor.
expandTypeConstructor :: TypeSynonyms -> Tp -> Tp

-- | Fully expand the top-level type constructor.
expandToplevelTC :: OrderedTypeSynonyms -> Tp -> Maybe Tp

-- | Try to expand the top-level type constructor one step.
expandTypeConstructorOneStep :: TypeSynonyms -> Tp -> Maybe Tp

-- | Try to expand the top-level type constructor of one of the two paired
--   Top.Types. If both top-level type constructors can be expanded, then
--   the type synonym thast appears first in the ordering is expanded.
expandOneStepOrdered :: OrderedTypeSynonyms -> (Tp, Tp) -> Maybe (Tp, Tp)


-- | A unification algorithm for types, which can take a list of (ordered)
--   type synonyms into account.
module Top.Types.Unification

-- | There are two reasons why two types cannot be unified: either two
--   (different) type constants clash (they should be the same), or a type
--   variable should be unified with a composed type that contains this
--   same type variable.
data UnificationError
ConstantClash :: String -> String -> UnificationError
InfiniteType :: Int -> UnificationError

-- | The most general unification (substitution) of two types.
mgu :: Tp -> Tp -> Either UnificationError MapSubstitution
mguWithTypeSynonyms :: OrderedTypeSynonyms -> Tp -> Tp -> Either UnificationError (Bool, MapSubstitution)

-- | Find the most general type for two types that are equal under type
--   synonyms (i.e., the least number of expansions)
equalUnderTypeSynonyms :: OrderedTypeSynonyms -> Tp -> Tp -> Maybe Tp

-- | Given a set of (ordered) type synonyms, can two types be unified?
unifiable :: OrderedTypeSynonyms -> Tp -> Tp -> Bool

-- | Same as unifiable, but takes as input a list of types
unifiableList :: OrderedTypeSynonyms -> Tps -> Bool
instance Show UnificationError
instance Eq UnificationError


-- | Type classes and the standard reduction instances. A part of the code
--   was taken from the paper <a>Typing Haskell in Haskell</a>.
module Top.Types.Classes
type Predicates = [Predicate]
data Predicate
Predicate :: String -> Tp -> Predicate
type ClassEnvironment = Map String Class
type Class = ([String], Instances)
type Instances = [Instance]
type Instance = (Predicate, Predicates)

-- | The empty class environment
emptyClassEnvironment :: ClassEnvironment
matchPredicates :: OrderedTypeSynonyms -> Predicate -> Predicate -> Maybe MapSubstitution
insertInstance :: String -> Instance -> ClassEnvironment -> ClassEnvironment
inClassEnvironment :: String -> ClassEnvironment -> Bool
superclassPaths :: String -> String -> ClassEnvironment -> [[String]]

-- | For example, Eq is a superclass of Ord
superclasses :: String -> ClassEnvironment -> [String]
instances :: String -> ClassEnvironment -> Instances
inHeadNormalForm :: Predicate -> Bool
listToHeadNormalForm :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Maybe Predicates
toHeadNormalForm :: OrderedTypeSynonyms -> ClassEnvironment -> Predicate -> Maybe Predicates
bySuperclass :: ClassEnvironment -> Predicate -> Predicates
byInstance :: OrderedTypeSynonyms -> ClassEnvironment -> Predicate -> Maybe Predicates
entail :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Predicate -> Bool
entailList :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> Predicates -> Bool
scEntail :: ClassEnvironment -> Predicates -> Predicate -> Bool
newtype ReductionError a
ReductionError :: a -> ReductionError a
contextReduction :: OrderedTypeSynonyms -> ClassEnvironment -> Predicates -> (Predicates, [ReductionError Predicate])
associatedContextReduction :: OrderedTypeSynonyms -> ClassEnvironment -> [(Predicate, a)] -> ([(Predicate, a)], [ReductionError (Predicate, a)])
standardClasses :: ClassEnvironment
instance Eq Predicate
instance Show a => Show (ReductionError a)
instance ShowQualifiers Predicate
instance HasTypes Predicate
instance Substitutable Predicate
instance Show Predicate


-- | A representation of type schemes. A type scheme is a (qualified) type
--   with a number of quantifiers (foralls) in front of it. A partial
--   mapping from type variable (Int) to their name (String) is preserved.
module Top.Types.Schemes

-- | A type scheme consists of a list of quantified type variables, a
--   finite map that partially maps these type variables to their original
--   identifier, and a qualified type.
type TpScheme = Forall QType
type QType = Qualification Predicates Tp

-- | A type class to convert something into a type scheme
class IsTpScheme a
toTpScheme :: IsTpScheme a => a -> TpScheme

-- | Determine the arity of a type scheme.
arityOfTpScheme :: TpScheme -> Int
genericInstanceOf :: OrderedTypeSynonyms -> ClassEnvironment -> TpScheme -> TpScheme -> Bool

-- | Is the type scheme overloaded (does it contain predicates)?
isOverloaded :: TpScheme -> Bool
makeScheme :: [Int] -> Predicates -> Tp -> TpScheme
instantiateWithNameMap :: Int -> TpScheme -> (Int, Predicates, Tp)

-- | A sigma is a type scheme or a type scheme variable
type Scheme qs = Forall (Qualification qs Tp)
data Sigma qs
SigmaVar :: SigmaVar -> Sigma qs
SigmaScheme :: (Scheme qs) -> Sigma qs
type SigmaVar = Int

-- | A substitution for type scheme variables
type TpSchemeMap = Map SigmaVar TpScheme
type SigmaPreds = Sigma Predicates
class IsSigmaPreds a
toSigmaPreds :: IsSigmaPreds a => a -> SigmaPreds
instance IsSigmaPreds Int
instance IsSigmaPreds Tp
instance IsSigmaPreds QType
instance IsSigmaPreds TpScheme
instance IsSigmaPreds SigmaPreds
instance (Substitutable qs, ShowQualifiers qs) => ShowQuantors (Sigma qs)
instance Substitutable qs => Substitutable (Sigma qs)
instance (ShowQualifiers qs, Substitutable qs) => Show (Sigma qs)
instance (ShowQualifiers q, Show a) => ShowQuantors (Qualification q a)
instance IsTpScheme Tp
instance IsTpScheme QType
instance IsTpScheme TpScheme


-- | Kinds can be represented by a type.
module Top.Types.Kinds
type Kind = Tp
type Kinds = [Kind]
type KindScheme = TpScheme

-- | Star is the kind of all values.
star :: Kind

-- | In traditional kind inference systems, a kind cannot contain
--   variables. At some point in the inference process the kind variables
--   are defaulted to star.
defaultToStar :: Kind -> Kind

-- | A function to show kinds.
showKind :: Kind -> String
showKindScheme :: KindScheme -> String


module Top.Util.Empty
class Empty a
empty :: Empty a => a
instance Empty a => Empty (Either a b)
instance Empty (Maybe a)
instance Empty [a]
instance (Empty a, Empty b) => Empty (a, b)
instance Empty ()


module Top.Util.Embedding
data Embedding a b
Embedding :: (a -> b) -> ((b -> b) -> a -> a) -> Embedding a b
getE :: Embedding a b -> a -> b
changeE :: Embedding a b -> (b -> b) -> a -> a
setE :: Embedding a b -> b -> a -> a
withE :: Embedding a b -> (b -> c) -> a -> c
idE :: Embedding a a
fstE :: Embedding (a, b) a
sndE :: Embedding (a, b) b
composeE :: Embedding a b -> Embedding b c -> Embedding a c
fromFstE :: Embedding a c -> Embedding (a, b) c
fromSndE :: Embedding b c -> Embedding (a, b) c


module Top.Monad.Select
newtype Select t m a
Select :: (m a) -> Select t m a
select :: m a -> Select t m a
data SelectFix (t :: (* -> *) -> *) (m :: * -> *) a
SelectFix :: (m a) -> SelectFix a
selectFix :: m a -> SelectFix t m a
class Embedded label s t | label s -> t, t -> label
embedding :: Embedded label s t => Embedding s t
deselect :: Select t m a -> m a
deselectFor :: (Embedded label s t, MonadState s m) => label -> Select t m a -> m a
deselectFix :: SelectFix t m a -> m a
deselectFixFor :: (Embedded label s (t m), MonadState s m) => label -> SelectFix t m a -> m a
instance Embedded c s2 t => Embedded c (s1, s2) t
instance MonadTrans (SelectFix t)
instance (MonadState s m, Embedded label s (t m)) => MonadState (t m) (SelectFix t m)
instance Monad m => Monad (SelectFix t m)
instance MonadTrans (Select t)
instance (MonadState s m, Embedded label s t) => MonadState t (Select t m)
instance Monad m => Monad (Select t m)


module Top.Implementation.General
class (Show s, Empty s) => SolveState s where showState = show stateOptions _ = [] collectStates s = [(stateName s, showState s)]
showState :: SolveState s => s -> String
stateName :: SolveState s => s -> String
stateOptions :: SolveState s => s -> [String]
collectStates :: SolveState s => s -> [(String, String)]
allStates :: (MonadState s m, SolveState s) => m [(String, String)]
allOptions :: (MonadState s m, SolveState s) => m [String]
data And f g x (m :: * -> *)
Compose :: (f (g x m) m) -> And f g x
data Simple a x (m :: * -> *)
Simple :: a -> x -> Simple a x
data Fix g x (m :: * -> *)
Fix :: (g m) -> x -> Fix g x
fromFstFixE :: Embedding (g m) c -> Embedding (Fix g x m) c
fromFstSimpleE :: Embedding a c -> Embedding (Simple a x m) c
fstSimpleE :: Embedding (Simple a x m) a
instance [overlap ok] Embedded c x s => Embedded c (Fix a x m) s
instance [overlap ok] Embedded c x s => Embedded c (Simple a x m) s
instance [overlap ok] Embedded c (f (g x m) m) s => Embedded c (And f g x m) s
instance [overlap ok] (SolveState (f m), SolveState x) => SolveState (Fix f x m)
instance [overlap ok] (SolveState a, SolveState x) => SolveState (Simple a x m)
instance [overlap ok] SolveState (f (g x m) m) => SolveState (And f g x m)
instance [overlap ok] (Show (f m), Show x) => Show (Fix f x m)
instance [overlap ok] (Show a, Show x) => Show (Simple a x m)
instance [overlap ok] Show (f (g x m) m) => Show (And f g x m)
instance [overlap ok] (Empty (g m), Empty x) => Empty (Fix g x m)
instance [overlap ok] (Empty a, Empty x) => Empty (Simple a x m)
instance [overlap ok] Empty (f (g x m) m) => Empty (And f g x m)
instance [overlap ok] SolveState ()


module Top.Util.Option
option :: a -> String -> Option a
data Option a
Option :: a -> a -> String -> Option a
defaultValue :: Option a -> a
currentValue :: Option a -> a
optionDescription :: Option a -> String
data OptionAccess m a
Access :: m a -> (a -> m ()) -> OptionAccess m a
getOption :: OptionAccess m a -> m a
setOption :: OptionAccess m a -> a -> m ()
ignoreOption :: Monad m => Option a -> OptionAccess m a
optionAccessTrans :: (forall a. m1 a -> m2 a) -> OptionAccess m1 b -> OptionAccess m2 b
useOption :: MonadState s m => (s -> Option a) -> (Option a -> s -> s) -> OptionAccess m a
instance Functor Option
instance (Show a, Eq a) => Show (Option a)


-- | A collection of type utilities.
module Top.Types


module Top.Constraint.Information
class Show info => TypeConstraintInfo info where equalityTypePair _ = id ambiguousPredicate _ = id unresolvedPredicate _ = id predicateArisingFrom _ = id parentPredicate _ = id escapedSkolems _ = id neverDirective _ = id closeDirective _ = id disjointDirective _ _ = id
equalityTypePair :: TypeConstraintInfo info => (Tp, Tp) -> info -> info
ambiguousPredicate :: TypeConstraintInfo info => Predicate -> info -> info
unresolvedPredicate :: TypeConstraintInfo info => Predicate -> info -> info
predicateArisingFrom :: TypeConstraintInfo info => (Predicate, info) -> info -> info
parentPredicate :: TypeConstraintInfo info => Predicate -> info -> info
escapedSkolems :: TypeConstraintInfo info => [Int] -> info -> info
neverDirective :: TypeConstraintInfo info => (Predicate, info) -> info -> info
closeDirective :: TypeConstraintInfo info => (String, info) -> info -> info
disjointDirective :: TypeConstraintInfo info => (String, info) -> (String, info) -> info -> info
class TypeConstraintInfo info => PolyTypeConstraintInfo info where instantiatedTypeScheme _ = id skolemizedTypeScheme _ = id
instantiatedTypeScheme :: PolyTypeConstraintInfo info => Forall (Qualification Predicates Tp) -> info -> info
skolemizedTypeScheme :: PolyTypeConstraintInfo info => (Tps, Forall (Qualification Predicates Tp)) -> info -> info
instance PolyTypeConstraintInfo String
instance TypeConstraintInfo String
instance PolyTypeConstraintInfo ()
instance TypeConstraintInfo ()


module Top.Implementation.TypeGraph.Basics
newtype VertexId
VertexId :: Int -> VertexId
type VertexInfo = (VertexKind, Maybe Tp)
data VertexKind
VVar :: VertexKind
VCon :: String -> VertexKind
VApp :: VertexId -> VertexId -> VertexKind
vertexIdToTp :: VertexId -> Tp
data EdgeId
EdgeId :: VertexId -> VertexId -> EdgeNr -> EdgeId
newtype EdgeNr
EdgeNrX :: Int -> EdgeNr
data ChildSide
LeftChild :: ChildSide
RightChild :: ChildSide
makeEdgeNr :: Int -> EdgeNr
impliedEdgeNr :: EdgeNr
data ParentChild
ParentChild :: VertexId -> VertexId -> ChildSide -> ParentChild
parent :: ParentChild -> VertexId
child :: ParentChild -> VertexId
childSide :: ParentChild -> ChildSide
type TypeGraphPath info = Path (EdgeId, PathStep info)
data PathStep info
Initial :: info -> PathStep info
Implied :: ChildSide -> VertexId -> VertexId -> PathStep info
Child :: ChildSide -> PathStep info
newtype Clique
CliqueX :: [ParentChild] -> Clique
type CliqueList = [Clique]
isSubsetClique :: Clique -> Clique -> Bool
isDisjointClique :: Clique -> Clique -> Bool
cliqueRepresentative :: Clique -> VertexId
triplesInClique :: Clique -> [ParentChild]
childrenInClique :: Clique -> [VertexId]
mergeCliques :: CliqueList -> Clique
makeClique :: [ParentChild] -> Clique
combineCliqueList :: CliqueList -> CliqueList -> CliqueList
instance Eq VertexId
instance Ord VertexId
instance Show VertexKind
instance Eq VertexKind
instance Ord VertexKind
instance Eq EdgeNr
instance Ord EdgeNr
instance Eq ChildSide
instance Ord ChildSide
instance Eq ParentChild
instance Ord Clique
instance Eq Clique
instance Show Clique
instance Ord EdgeId
instance Eq EdgeId
instance Show EdgeId
instance Show (PathStep info)
instance Ord ParentChild
instance Show ParentChild
instance Show ChildSide
instance Show EdgeNr
instance Show VertexId


module Top.Implementation.TypeGraph.Class
class TypeGraph graph info | graph -> info where allPaths i1 i2 = allPathsList i1 [i2] allPathsList = allPathsListWithout empty childrenInGroupOf i graph = unzip [(ParentChild {parent = p, child = t1, childSide = LeftChild},  ParentChild {parent = p, child = t2, childSide = RightChild}) | (p, (VApp t1 t2, _)) <- verticesInGroupOf i graph] constantsInGroupOf i graph = nub [s | (_, (VCon s, _)) <- verticesInGroupOf i graph] representativeInGroupOf i graph = case verticesInGroupOf i graph of { (vid, _) : _ -> vid _ -> internalError "Top.TypeGraph.TypeGraphState" "representativeInGroupOf" "unexpected empty equivalence group" } substituteVariable syns = substituteType syns . TVar substituteType syns tp graph = let err = internalError "Top.TypeGraph.TypeGraphState" "substituteType" "inconsistent state" in fromMaybe err (substituteTypeSafe syns tp graph) markAsPossibleError _ = id getMarkedPossibleErrors _ = [] unmarkPossibleErrors = id
addTermGraph :: TypeGraph graph info => OrderedTypeSynonyms -> Int -> Tp -> graph -> (Int, VertexId, graph)
addVertex :: TypeGraph graph info => VertexId -> VertexInfo -> graph -> graph
addEdge :: TypeGraph graph info => EdgeId -> info -> graph -> graph
addNewEdge :: TypeGraph graph info => (VertexId, VertexId) -> info -> graph -> graph
deleteEdge :: TypeGraph graph info => EdgeId -> graph -> graph
verticesInGroupOf :: TypeGraph graph info => VertexId -> graph -> [(VertexId, VertexInfo)]
childrenInGroupOf :: TypeGraph graph info => VertexId -> graph -> ([ParentChild], [ParentChild])
constantsInGroupOf :: TypeGraph graph info => VertexId -> graph -> [String]
representativeInGroupOf :: TypeGraph graph info => VertexId -> graph -> VertexId
edgesFrom :: TypeGraph graph info => VertexId -> graph -> [(EdgeId, info)]
allPaths :: TypeGraph graph info => VertexId -> VertexId -> graph -> TypeGraphPath info
allPathsList :: TypeGraph graph info => VertexId -> [VertexId] -> graph -> TypeGraphPath info
allPathsListWithout :: TypeGraph graph info => Set VertexId -> VertexId -> [VertexId] -> graph -> TypeGraphPath info
substituteVariable :: TypeGraph graph info => OrderedTypeSynonyms -> Int -> graph -> Tp
substituteType :: TypeGraph graph info => OrderedTypeSynonyms -> Tp -> graph -> Tp
substituteTypeSafe :: TypeGraph graph info => OrderedTypeSynonyms -> Tp -> graph -> Maybe Tp
makeSubstitution :: TypeGraph graph info => OrderedTypeSynonyms -> graph -> [(VertexId, Tp)]
typeFromTermGraph :: TypeGraph graph info => VertexId -> graph -> Tp
markAsPossibleError :: TypeGraph graph info => VertexId -> graph -> graph
getMarkedPossibleErrors :: TypeGraph graph info => graph -> [VertexId]
unmarkPossibleErrors :: TypeGraph graph info => graph -> graph


-- | An equivalence group is a graph-like structure containing type
--   variables and type constants that should all be equivalent. The edges
--   explain why they should be equal.
module Top.Implementation.TypeGraph.EquivalenceGroup
data EquivalenceGroup info
emptyGroup :: EquivalenceGroup info
insertVertex :: VertexId -> VertexInfo -> EquivalenceGroup info -> EquivalenceGroup info
insertEdge :: EdgeId -> info -> EquivalenceGroup info -> EquivalenceGroup info
insertClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info
combineGroups :: EquivalenceGroup info -> EquivalenceGroup info -> EquivalenceGroup info

-- | vertices in this equivalence group
vertices :: EquivalenceGroup info -> [(VertexId, VertexInfo)]
constants :: EquivalenceGroup info -> [String]

-- | (initial) edges in this equivalence group
edges :: EquivalenceGroup info -> [(EdgeId, info)]
equalPaths :: Set VertexId -> VertexId -> [VertexId] -> EquivalenceGroup info -> TypeGraphPath info
removeEdge :: EdgeId -> EquivalenceGroup info -> EquivalenceGroup info
removeClique :: Clique -> EquivalenceGroup info -> EquivalenceGroup info
splitGroup :: EquivalenceGroup info -> [EquivalenceGroup info]
typeOfGroup :: OrderedTypeSynonyms -> EquivalenceGroup info -> Maybe Tp
consistent :: EquivalenceGroup info -> Bool
checkGroup :: EquivalenceGroup info -> EquivalenceGroup info
instance Show (EquivalenceGroup info)


module Top.Implementation.TypeGraph.Standard
data StandardTypeGraph info
STG :: Map VertexId Int -> Map Int (EquivalenceGroup info) -> Int -> [VertexId] -> Int -> StandardTypeGraph info
referenceMap :: StandardTypeGraph info -> Map VertexId Int
equivalenceGroupMap :: StandardTypeGraph info -> Map Int (EquivalenceGroup info)
equivalenceGroupCounter :: StandardTypeGraph info -> Int
possibleErrors :: StandardTypeGraph info -> [VertexId]
constraintNumber :: StandardTypeGraph info -> Int
combineClasses :: [VertexId] -> StandardTypeGraph info -> StandardTypeGraph info
propagateEquality :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info
addClique :: Clique -> StandardTypeGraph info -> StandardTypeGraph info
propagateRemoval :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info
splitClass :: VertexId -> StandardTypeGraph info -> ([VertexId], StandardTypeGraph info)
deleteClique :: Clique -> StandardTypeGraph info -> StandardTypeGraph info
createGroup :: EquivalenceGroup info -> StandardTypeGraph info -> StandardTypeGraph info
removeGroup :: EquivalenceGroup info -> StandardTypeGraph info -> StandardTypeGraph info
updateGroupOf :: VertexId -> (EquivalenceGroup info -> EquivalenceGroup info) -> StandardTypeGraph info -> StandardTypeGraph info
maybeGetGroupOf :: VertexId -> StandardTypeGraph info -> Maybe (EquivalenceGroup info)
getGroupOf :: VertexId -> StandardTypeGraph info -> EquivalenceGroup info
getAllGroups :: StandardTypeGraph info -> [EquivalenceGroup info]
vertexExists :: VertexId -> StandardTypeGraph info -> Bool
getPossibleInconsistentGroups :: StandardTypeGraph info -> [VertexId]
setPossibleInconsistentGroups :: [VertexId] -> StandardTypeGraph info -> StandardTypeGraph info
addPossibleInconsistentGroup :: VertexId -> StandardTypeGraph info -> StandardTypeGraph info
instance TypeGraph (StandardTypeGraph info) info
instance Show (StandardTypeGraph info)
instance Show info => Empty (StandardTypeGraph info)


-- | A data type to represent constraints in general, and a type class for
--   constraints that are solvable.
module Top.Constraint
type Constraints m = [Constraint m]
data Constraint m
Constraint :: c -> (c -> m ()) -> (c -> m Bool) -> Constraint m

-- | A constraint is solvable if it knows how it can be solved in a certain
--   state (a monadic operation), if it can check afterwards whether the
--   final state satisfies it, and when it can be shown.
class (Show c, Substitutable c, Monad m) => Solvable c m where checkCondition _ = return True
solveConstraint :: Solvable c m => c -> m ()
checkCondition :: Solvable c m => c -> m Bool

-- | Lifting a constraint to the Constraint data type. Every instance of
--   the Solvable type class can be lifted.
liftConstraint :: Solvable c m => c -> Constraint m
liftConstraints :: Solvable c m => [c] -> Constraints m
mapConstraint :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2
newtype Operation m
Op_ :: String -> Operation m
operation :: Monad m => String -> m () -> Constraint m

-- | The data type ConstraintSum is similar to the (standard) Either data
--   type. However, its Show instance is slightly different as the name of
--   the constructor is not shown.
data ConstraintSum f g info
SumLeft :: (f info) -> ConstraintSum f g info
SumRight :: (g info) -> ConstraintSum f g info

-- | Similar to the <a>either</a> function.
constraintSum :: (f info -> c) -> (g info -> c) -> ConstraintSum f g info -> c
instance (Solvable (f info) m, Solvable (g info) m) => Solvable (ConstraintSum f g info) m
instance (Substitutable (f info), Substitutable (g info)) => Substitutable (ConstraintSum f g info)
instance (Functor f, Functor g) => Functor (ConstraintSum f g)
instance (Show (f info), Show (g info)) => Show (ConstraintSum f g info)
instance (Solvable a m, Solvable b m) => Solvable (Either a b) m
instance Substitutable (Operation m)
instance Show (Operation m)
instance Monad m => Solvable (Constraint m) m
instance Substitutable (Constraint m)
instance Show (Constraint m)


module Top.Interface.Basic
data ClassBasic
ClassBasic :: ClassBasic
deBasic :: (Embedded ClassBasic (s (StateFixT s m)) (t (StateFixT s m)), Monad m) => SelectFix t (StateFixT s m) a -> StateFixT s m a
class Monad m => HasBasic m info | m -> info where pushConstraint c = pushConstraints [c] pushConstraints = mapM_ pushConstraint stopAfterFirstError = ignoreOption stopOption checkConditions = ignoreOption checkOption
pushConstraint :: HasBasic m info => Constraint m -> m ()
pushConstraints :: HasBasic m info => Constraints m -> m ()
popConstraint :: HasBasic m info => m (Maybe (Constraint m))
discardConstraints :: HasBasic m info => m ()
addLabeledError :: HasBasic m info => ErrorLabel -> info -> m ()
getLabeledErrors :: HasBasic m info => m [(info, ErrorLabel)]
updateErrorInfo :: HasBasic m info => (info -> m info) -> m ()
addCheck :: HasBasic m info => String -> m Bool -> m ()
getChecks :: HasBasic m info => m [(m Bool, String)]
stopAfterFirstError :: HasBasic m info => OptionAccess m Bool
checkConditions :: HasBasic m info => OptionAccess m Bool
pushOperation :: HasBasic m info => m () -> m ()
pushNamedOperation :: HasBasic m info => String -> m () -> m ()
addError :: HasBasic m info => info -> m ()
getErrors :: HasBasic m info => m [info]
doChecks :: HasBasic m info => m ()
startSolving :: HasBasic m info => m ()

-- | A datatype to label the errors that are detected.
data ErrorLabel
ErrorLabel :: String -> ErrorLabel
NoErrorLabel :: ErrorLabel
stopOption, checkOption :: Option Bool
instance Eq ErrorLabel
instance Ord ErrorLabel
instance Show ErrorLabel
instance (Monad m, Embedded ClassBasic (s (StateFixT s m)) (t (StateFixT s m)), HasBasic (SelectFix t (StateFixT s m)) info) => HasBasic (StateFixT s m) info


module Top.Interface.Substitution
data ClassSubst
ClassSubst :: ClassSubst
deSubst :: (Embedded ClassSubst (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a
class Monad m => HasSubst m info | m -> info
makeSubstConsistent :: HasSubst m info => m ()
unifyTerms :: HasSubst m info => info -> Tp -> Tp -> m ()
findSubstForVar :: HasSubst m info => Int -> m Tp
fixpointSubst :: HasSubst m info => m FixpointSubstitution
unificationErrorLabel :: ErrorLabel

-- | Apply the substitution to a value that contains type variables (a
--   member of the Substitutable type class).
applySubst :: (Substitutable a, HasSubst m info) => a -> m a
instance (Monad m, Embedded ClassSubst (s (StateFixT s m)) t, HasSubst (Select t (StateFixT s m)) info) => HasSubst (StateFixT s m) info


module Top.Interface.Qualification
data ClassQual
ClassQual :: ClassQual
deQual :: (Embedded ClassQual (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a
class Monad m => HasQual m info | m -> info where generalizeWithQualifiers monos = return . generalize monos . ([] .=>.) improveQualifiers normal = if normal then improveQualifiersNormal else improveQualifiersFinal improveQualifiersNormal = return [] improveQualifiersFinal = return [] simplifyQualifiers = return () ambiguousQualifiers = return ()
proveQualifier :: HasQual m info => info -> Predicate -> m ()
assumeQualifier :: HasQual m info => info -> Predicate -> m ()
changeQualifiers :: HasQual m info => (Predicate -> m Predicate) -> m ()
allQualifiers :: HasQual m info => m [Predicate]
generalizeWithQualifiers :: HasQual m info => Tps -> Tp -> m (Scheme [Predicate])
improveQualifiers :: HasQual m info => Bool -> m [(info, Tp, Tp)]
improveQualifiersNormal :: HasQual m info => m [(info, Tp, Tp)]
improveQualifiersFinal :: HasQual m info => m [(info, Tp, Tp)]
simplifyQualifiers :: HasQual m info => m ()
ambiguousQualifiers :: HasQual m info => m ()
setClassEnvironment :: HasQual m info => ClassEnvironment -> m ()
getClassEnvironment :: HasQual m info => m ClassEnvironment
proveQualifiers :: HasQual m info => info -> Predicates -> m ()
assumeQualifiers :: HasQual m info => info -> Predicates -> m ()
contextReduction :: (HasSubst m info, HasQual m info) => m ()
ambiguities :: (HasSubst m info, HasQual m info) => m ()
improveQualifiersFix :: (HasSubst m info, HasQual m info) => Bool -> m ()
instance (Monad m, Embedded ClassQual (s (StateFixT s m)) t, HasQual (Select t (StateFixT s m)) info) => HasQual (StateFixT s m) info


module Top.Interface.TypeInference
data ClassTI
ClassTI :: ClassTI
deTI :: (Embedded ClassTI (s (StateFixT s m)) t, Monad m) => Select t (StateFixT s m) a -> StateFixT s m a
class Monad m => HasTI m info | m -> info
getUnique :: HasTI m info => m Int
setUnique :: HasTI m info => Int -> m ()
setTypeSynonyms :: HasTI m info => OrderedTypeSynonyms -> m ()
getTypeSynonyms :: HasTI m info => m OrderedTypeSynonyms
getSkolems :: HasTI m info => m [([Int], info, Tps)]
setSkolems :: HasTI m info => [([Int], info, Tps)] -> m ()
allTypeSchemes :: HasTI m info => m (Map Int (Scheme Predicates))
getTypeScheme :: HasTI m info => Int -> m (Scheme Predicates)
storeTypeScheme :: HasTI m info => Int -> Scheme Predicates -> m ()
nextUnique :: HasTI m info => m Int
zipWithUniques :: HasTI m info => (Int -> a -> b) -> [a] -> m [b]
addSkolem :: HasTI m info => ([Int], info, Tps) -> m ()
instantiateM :: (HasTI m info, Substitutable a) => Forall a -> m a
skolemizeTruly :: (HasTI m info, Substitutable a) => Forall a -> m a
skolemizeFaked :: (HasTI m info, Substitutable a) => info -> Tps -> Forall a -> m a
getSkolemSubstitution :: HasTI m info => m MapSubstitution

-- | First, make the substitution consistent. Then check the skolem
--   constants(?)
makeConsistent :: (HasTI m info, HasBasic m info, HasSubst m info) => m ()
checkSkolems :: (HasTI m info, HasSubst m info, HasBasic m info, TypeConstraintInfo info) => m ()
skolemVersusConstantLabel :: ErrorLabel
skolemVersusSkolemLabel :: ErrorLabel
escapingSkolemLabel :: ErrorLabel
replaceSchemeVar :: HasTI m info => Sigma Predicates -> m (Scheme Predicates)
findScheme :: HasTI m info => Sigma Predicates -> m (Scheme Predicates)
instance (Monad m, Embedded ClassTI (s (StateFixT s m)) t, HasTI (Select t (StateFixT s m)) info) => HasTI (StateFixT s m) info


module Top.Constraint.Equality
data EqualityConstraint info
Equality :: Tp -> Tp -> info -> EqualityConstraint info

-- | The constructor of an equality constraint.
(.==.) :: Tp -> Tp -> info -> EqualityConstraint info
instance (TypeConstraintInfo info, HasSubst m info, HasTI m info) => Solvable (EqualityConstraint info) m
instance Substitutable (EqualityConstraint info)
instance Functor EqualityConstraint
instance Show info => Show (EqualityConstraint info)


-- | Additional state information that should be stored in order to perform
--   type inference.
module Top.Implementation.TypeInference
data TIState info
TIState :: Int -> OrderedTypeSynonyms -> [([Int], info, Tps)] -> Map Int (Scheme Predicates) -> TIState info

-- | A counter for fresh type variables
counter :: TIState info -> Int

-- | All known type synonyms
synonyms :: TIState info -> OrderedTypeSynonyms

-- | List of skolem constants
skolems :: TIState info -> [([Int], info, Tps)]

-- | Type scheme map
schemeMap :: TIState info -> Map Int (Scheme Predicates)
instance (MonadState s m, Embedded ClassTI s (TIState info)) => HasTI (Select (TIState info) m) info
instance Embedded ClassTI (Simple (TIState info) x m) (TIState info)
instance Show info => Show (TIState info)
instance Show info => Empty (TIState info)
instance Show info => SolveState (TIState info)


module Top.Constraint.Polymorphism
data PolymorphismConstraint info
Generalize :: Int -> (Tps, Tp) -> info -> PolymorphismConstraint info
Instantiate :: Tp -> (Sigma Predicates) -> info -> PolymorphismConstraint info
Skolemize :: Tp -> (Tps, Sigma Predicates) -> info -> PolymorphismConstraint info
Implicit :: Tp -> (Tps, Tp) -> info -> PolymorphismConstraint info

-- | The constructor of an instantiate (explicit instance) constraint.
(.::.) :: Tp -> Scheme Predicates -> info -> PolymorphismConstraint info
instance (HasBasic m info, HasTI m info, HasSubst m info, HasQual m info, PolyTypeConstraintInfo info) => Solvable (PolymorphismConstraint info) m
instance Substitutable (PolymorphismConstraint info)
instance Functor PolymorphismConstraint
instance Show info => Show (PolymorphismConstraint info)


module Top.Implementation.FastSubstitution
newtype GreedyState info
GreedyState :: FixpointSubstitution -> GreedyState info
unGS :: GreedyState info -> FixpointSubstitution
writeExpandedType :: OrderedTypeSynonyms -> Tp -> Tp -> FixpointSubstitution -> FixpointSubstitution
instance [overlap ok] (MonadState s m, HasBasic m info, HasTI m info, Embedded ClassSubst s (GreedyState info)) => HasSubst (Select (GreedyState info) m) info
instance [overlap ok] Embedded ClassSubst (Simple (GreedyState info) m b) (GreedyState info)
instance [overlap ok] Embedded ClassSubst (GreedyState info) (GreedyState info)
instance [overlap ok] Empty (GreedyState info)
instance [overlap ok] Show (GreedyState info)
instance [overlap ok] SolveState (GreedyState info)


module Top.Implementation.Overloading
data OverloadingState info
OverloadingState :: ClassEnvironment -> PredicateMap info -> TypeClassDirectives info -> OverloadingState info

-- | All known type classes and instances
classEnvironment :: OverloadingState info -> ClassEnvironment

-- | Type class assertions
predicateMap :: OverloadingState info -> PredicateMap info

-- | Directives for type class assertions
typeClassDirectives :: OverloadingState info -> TypeClassDirectives info
simplify :: (HasTI m info, TypeConstraintInfo info, HasBasic m info) => OrderedTypeSynonyms -> ClassEnvironment -> TypeClassDirectives info -> [(Predicate, info)] -> m [(Predicate, info)]
ambiguous :: (HasBasic m info, HasTI m info, TypeConstraintInfo info) => [(Predicate, info)] -> m ()
modifyPredicateMap :: MonadState (OverloadingState info) m => (PredicateMap info -> PredicateMap info) -> m ()
proveQsSubst, generalizedQsSubst, assumeQsSubst :: (MonadState s m, Embedded ClassQual s (OverloadingState info)) => Select (OverloadingState info) m [(Predicate, info)]
substPredicate :: HasSubst m info => (Predicate, info) -> m (Predicate, info)
type TypeClassDirectives info = [TypeClassDirective info]
data TypeClassDirective info
NeverDirective :: Predicate -> info -> TypeClassDirective info
CloseDirective :: String -> info -> TypeClassDirective info
DisjointDirective :: [String] -> info -> TypeClassDirective info
DefaultDirective :: String -> Tps -> info -> TypeClassDirective info
data PredicateMap info
PredicateMap :: [(Predicate, info)] -> [(Predicate, info)] -> [(Predicate, info)] -> PredicateMap info
globalQualifiers :: PredicateMap info -> [(Predicate, info)]
globalGeneralizedQs :: PredicateMap info -> [(Predicate, info)]
globalAssumptions :: PredicateMap info -> [(Predicate, info)]
unresolvedLabel :: ErrorLabel
disjointLabel :: ErrorLabel
ambiguousLabel :: ErrorLabel
missingInSignatureLabel :: ErrorLabel
instance Substitutable (PredicateMap info)
instance Empty (PredicateMap info)
instance Show (PredicateMap info)
instance Show (TypeClassDirective info)
instance (MonadState s m, HasBasic m info, HasTI m info, TypeConstraintInfo info, Embedded ClassQual s (OverloadingState info)) => HasQual (Select (OverloadingState info) m) info
instance Embedded ClassQual (Simple (OverloadingState info) x m) (OverloadingState info)
instance Embedded ClassQual (OverloadingState info) (OverloadingState info)
instance Show info => SolveState (OverloadingState info)
instance Show (OverloadingState info)
instance Empty (OverloadingState info)


module Top.Implementation.SimpleSubstitution
newtype SimpleState info
SimpleState :: MapSubstitution -> SimpleState info
unSS :: SimpleState info -> MapSubstitution
instance (MonadState s m, HasBasic m info, HasTI m info, Embedded ClassSubst s (SimpleState info)) => HasSubst (Select (SimpleState info) m) info
instance Embedded ClassSubst (Simple (SimpleState info) x m) (SimpleState info)
instance Embedded ClassSubst (SimpleState info) (SimpleState info)
instance Empty (SimpleState info)
instance Show (SimpleState info)
instance SolveState (SimpleState info)


-- | Constraints for overloading
module Top.Constraint.Qualifier
data ExtraConstraint info
Prove :: Predicate -> info -> ExtraConstraint info
Assume :: Predicate -> info -> ExtraConstraint info
instance (HasQual m info, PolyTypeConstraintInfo info) => Solvable (ExtraConstraint info) m
instance Substitutable (ExtraConstraint info)
instance Functor ExtraConstraint
instance Show info => Show (ExtraConstraint info)


-- | An interface for a monad that constains the most basic operations to
--   solve constraints. Can be reused for all kinds of constraint-based
--   analyses.
module Top.Implementation.Basic

-- | A BasicState is parameterized over the monad in which the constraints
--   can be solved, and over the information that is stored with each
--   constraint.
data BasicState info m
BasicState :: Constraints m -> [(info, ErrorLabel)] -> [(m Bool, String)] -> Option Bool -> Option Bool -> BasicState info m

-- | A stack of constraints that is to be solved
constraints :: BasicState info m -> Constraints m

-- | The detected errors
errors :: BasicState info m -> [(info, ErrorLabel)]

-- | Conditions to check (for the solved constraints)
conditions :: BasicState info m -> [(m Bool, String)]

-- | Discard all remaining constraints after the first error
optionStop :: BasicState info m -> Option Bool
optionCheck :: BasicState info m -> Option Bool
instance [overlap ok] (MonadState s m, Embedded ClassBasic s (BasicState info m)) => HasBasic (SelectFix (BasicState info) m) info
instance [overlap ok] Embedded ClassBasic (Fix (BasicState info) x m) (BasicState info m)
instance [overlap ok] Embedded ClassBasic (BasicState info m) (BasicState info m)
instance [overlap ok] Show (BasicState info m)
instance [overlap ok] Empty (BasicState info m)
instance [overlap ok] SolveState (BasicState info m)


module Top.Solver
data ConstraintSolver constraint info
ConstraintSolver :: (SolveOptions -> [constraint] -> (SolveResult info, LogEntries)) -> ConstraintSolver constraint info
makeConstraintSolver :: Empty (f () (BasicMonad f)) => (SolveOptions -> [constraint] -> BasicMonad f (SolveResult info)) -> ConstraintSolver constraint info
solve :: SolveOptions -> [constraint] -> ConstraintSolver constraint info -> (SolveResult info, LogEntries)
onlySolveConstraints :: (HasTI m info, HasBasic m info, HasSubst m info, HasQual m info, TypeConstraintInfo info, Solvable constraint m, MonadState s m, SolveState s, MonadWriter LogEntries m) => [constraint] -> m ()
solveConstraints :: (HasTI m info, HasBasic m info, HasSubst m info, HasQual m info, TypeConstraintInfo info, Solvable constraint m, MonadState s m, SolveState s, MonadWriter LogEntries m) => SolveOptions -> [constraint] -> m (SolveResult info)
solveResult :: (HasBasic m info, HasTI m info, HasSubst m info, HasQual m info, TypeConstraintInfo info) => m (SolveResult info)
data SolveResult info
SolveResult :: Int -> FixpointSubstitution -> Map Int (Scheme Predicates) -> Predicates -> [(info, ErrorLabel)] -> SolveResult info
uniqueFromResult :: SolveResult info -> Int
substitutionFromResult :: SolveResult info -> FixpointSubstitution
typeschemesFromResult :: SolveResult info -> Map Int (Scheme Predicates)
qualifiersFromResult :: SolveResult info -> Predicates
errorsFromResult :: SolveResult info -> [(info, ErrorLabel)]
emptyResult :: Int -> SolveResult info
combineResults :: SolveResult info -> SolveResult info -> SolveResult info
data SolveOptions
SolveOptions_ :: Int -> OrderedTypeSynonyms -> ClassEnvironment -> Bool -> Bool -> SolveOptions
uniqueCounter :: SolveOptions -> Int
typeSynonyms :: SolveOptions -> OrderedTypeSynonyms
classEnvironment :: SolveOptions -> ClassEnvironment
setStopAfterFirstError :: SolveOptions -> Bool
setCheckConditions :: SolveOptions -> Bool
solveOptions :: SolveOptions
initialize :: (HasBasic m info, HasQual m info, HasTI m info, Substitutable a) => a -> SolveOptions -> m ()
type BasicMonad f = StateFixT (f ()) (Writer LogEntries)
newtype LogEntries
LogEntries :: ([LogEntry] -> [LogEntry]) -> LogEntries
data LogEntry
LogEntry :: Int -> String -> LogEntry
priority :: LogEntry -> Int
msg :: LogEntry -> String
noLogEntries :: LogEntries
singleEntry :: Int -> String -> LogEntries
evalBasicMonad :: Empty (f () (BasicMonad f)) => BasicMonad f a -> (a, LogEntries)
logMsg :: MonadWriter LogEntries m => String -> m ()
logMsgPrio :: MonadWriter LogEntries m => Int -> String -> m ()

-- | Print the current state and add this as a debug message.
logState :: (MonadState s m, SolveState s, MonadWriter LogEntries m) => m ()
instance Show LogEntries
instance Show LogEntry
instance Monoid LogEntries
instance Empty (SolveResult info)


module Top.Implementation.TypeGraph.ClassMonadic
class (HasBasic m info, HasTI m info, HasQual m info, HasTG m info, MonadWriter LogEntries m, Show info) => HasTypeGraph m info | m -> info
class Monad m => HasTG m info | m -> info
withTypeGraph :: HasTG m info => (forall graph. TypeGraph graph info => graph -> (a, graph)) -> m a
useTypeGraph :: HasTG m info => (forall graph. TypeGraph graph info => graph -> a) -> m a
changeTypeGraph :: HasTG m info => (forall graph. TypeGraph graph info => graph -> graph) -> m ()
addTermGraph :: HasTypeGraph m info => Tp -> m VertexId
addVertex :: HasTypeGraph m info => VertexId -> VertexInfo -> m ()
addEdge :: HasTypeGraph m info => EdgeId -> info -> m ()
addNewEdge :: HasTypeGraph m info => (VertexId, VertexId) -> info -> m ()
deleteEdge :: HasTypeGraph m info => EdgeId -> m ()
verticesInGroupOf :: HasTypeGraph m info => VertexId -> m [(VertexId, VertexInfo)]
childrenInGroupOf :: HasTypeGraph m info => VertexId -> m ([ParentChild], [ParentChild])
constantsInGroupOf :: HasTypeGraph m info => VertexId -> m [String]
representativeInGroupOf :: HasTypeGraph m info => VertexId -> m VertexId
edgesFrom :: HasTypeGraph m info => VertexId -> m [(EdgeId, info)]
allPaths :: HasTypeGraph m info => VertexId -> VertexId -> m (TypeGraphPath info)
allPathsList :: HasTypeGraph m info => VertexId -> [VertexId] -> m (TypeGraphPath info)
allPathsListWithout :: HasTypeGraph m info => Set VertexId -> VertexId -> [VertexId] -> m (TypeGraphPath info)
substituteVariable :: HasTypeGraph m info => Int -> m Tp
substituteType :: HasTypeGraph m info => Tp -> m Tp
substituteTypeSafe :: HasTypeGraph m info => Tp -> m (Maybe Tp)
makeSubstitution :: HasTypeGraph m info => m [(VertexId, Tp)]
typeFromTermGraph :: HasTypeGraph m info => VertexId -> m Tp
markAsPossibleError :: HasTypeGraph m info => VertexId -> m ()
getMarkedPossibleErrors :: HasTypeGraph m info => m [VertexId]
unmarkPossibleErrors :: HasTypeGraph m info => m ()
theUnifyTerms :: HasTypeGraph m info => info -> Tp -> Tp -> m ()
makeFixpointSubst :: HasTypeGraph m info => m FixpointSubstitution
instance (HasBasic m info, HasTI m info, HasQual m info, HasTG m info, MonadWriter LogEntries m, Show info) => HasTypeGraph m info


module Top.Implementation.TypeGraph.Heuristic
type PathHeuristics info = Path (EdgeId, info) -> [Heuristic info]
newtype Heuristic info
Heuristic :: (forall m. HasTypeGraph m info => HComponent m info) -> Heuristic info
data Selector m info
Selector :: (String, (EdgeId, info) -> m (Maybe (Int, String, [EdgeId], info))) -> Selector m info
SelectorList :: (String, [(EdgeId, info)] -> m (Maybe (Int, String, [EdgeId], info))) -> Selector m info
data HComponent m info
Filter :: String -> ([(EdgeId, info)] -> m [(EdgeId, info)]) -> HComponent m info
Voting :: [Selector m info] -> HComponent m info
getSelectorName :: (MonadWriter LogEntries m, HasTypeGraph m info) => Selector m info -> String
resultsEdgeFilter :: (Eq a, Monad m) => ([a] -> a) -> String -> ((EdgeId, info) -> m a) -> HComponent m info
maximalEdgeFilter :: (Ord a, Monad m) => String -> ((EdgeId, info) -> m a) -> HComponent m info
minimalEdgeFilter :: (Ord a, Monad m) => String -> ((EdgeId, info) -> m a) -> HComponent m info
edgeFilter :: Monad m => String -> ((EdgeId, info) -> m Bool) -> HComponent m info
doWithoutEdges :: HasTypeGraph m info => [(EdgeId, info)] -> m result -> m result
doWithoutEdge :: HasTypeGraph m info => (EdgeId, info) -> m result -> m result
eqInfo2 :: (EdgeId, info) -> (EdgeId, info) -> Bool
info2ToEdgeNr :: (EdgeId, info) -> EdgeNr
class HasTwoTypes a
getTwoTypes :: HasTwoTypes a => a -> (Tp, Tp)
getSubstitutedTypes :: (HasTypeGraph m info, HasTwoTypes info) => info -> m (Maybe Tp, Maybe Tp)


module Top.Implementation.TypeGraph.ApplyHeuristics
applyHeuristics :: HasTypeGraph m info => (Path (EdgeId, info) -> [Heuristic info]) -> m [ErrorInfo info]
predicatePath :: (HasQual m info, HasTypeGraph m info) => m (Path (EdgeId, PathStep info))
expandPath :: HasTypeGraph m info => TypeGraphPath info -> m (Path (EdgeId, info))
instance Ord IntPair
instance Eq IntPair
instance Show IntPair


module Top.Implementation.TypeGraph.DefaultHeuristics
defaultHeuristics :: Show info => Path (EdgeId, info) -> [Heuristic info]

-- | Compute the smallest <tt>minimal</tt> sets. This computation is
--   very(!) costly (might take a long time for complex inconsistencies)
inMininalSet :: Path (EdgeId, info) -> Heuristic info

-- | Although not as precise as the minimal set analysis, this calculates
--   the participation of each edge in all error paths. Default ratio = 1.0
--   (100 percent) (the ratio determines which scores compared to the best
--   are accepted)
highParticipation :: Show info => Double -> Path (EdgeId, info) -> Heuristic info

-- | Select the <a>latest</a> constraint
firstComeFirstBlamed :: Heuristic info

-- | Select only specific constraint numbers
selectConstraintNumbers :: [EdgeNr] -> Heuristic info

-- | Select only the constraints for which there is evidence in the
--   predicates of the current state that the constraint at hand is
--   incorrect.
inPredicatePath :: Heuristic info


module Top.Implementation.TypeGraphSubstitution
data TypeGraphState info
TypeGraphState :: StandardTypeGraph info -> PathHeuristics info -> TypeGraphState info
typegraph :: TypeGraphState info -> StandardTypeGraph info
heuristics :: TypeGraphState info -> PathHeuristics info
removeInconsistencies :: HasTypeGraph m info => PathHeuristics info -> m ()
instance (HasBasic m info, HasTI m info, HasQual m info, HasTG m info, MonadWriter LogEntries m, Show info, MonadState s m, Embedded ClassSubst s (TypeGraphState info)) => HasSubst (Select (TypeGraphState info) m) info
instance (MonadState s m, Embedded ClassSubst s (TypeGraphState info)) => HasTG (Select (TypeGraphState info) m) info
instance (Monad m, Embedded ClassSubst (s (StateFixT s m)) t, HasTG (Select t (StateFixT s m)) info) => HasTG (StateFixT s m) info
instance Embedded ClassSubst (Simple (TypeGraphState info) x m) (TypeGraphState info)
instance Embedded ClassSubst (TypeGraphState info) (TypeGraphState info)
instance Show info => Empty (TypeGraphState info)
instance Show info => Show (TypeGraphState info)
instance Show info => SolveState (TypeGraphState info)


module Top.Solver.PartitionCombinator
type Chunks constraint = [Chunk constraint]
type Chunk constraint = (ChunkID, Tree constraint)
type ChunkID = Int
solveChunkConstraints :: (Map Int (Scheme Predicates) -> constraint -> constraint) -> ConstraintSolver constraint info -> (Tree constraint -> [constraint]) -> Chunks constraint -> ConstraintSolver constraint info


module Top.Solver.SwitchCombinator

-- | The first solver is used to solve the constraint set. If this fails
--   (at least one error is returned), then the second solver takes over.
(|>>|) :: ConstraintSolver constraint info -> ConstraintSolver constraint info -> ConstraintSolver constraint info


module Top.Solver.Greedy
type Greedy info = BasicMonad (GreedyS info)
type GreedyS info = And (Fix (BasicState info)) (And (Simple (TIState info)) (And (Simple (GreedyState info)) (Simple (OverloadingState info))))
solveGreedy :: (Solvable constraint (Greedy info), TypeConstraintInfo info) => SolveOptions -> [constraint] -> Greedy info (SolveResult info)
greedyConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (Greedy info)) => ConstraintSolver constraint info
type GreedySimple info = BasicMonad (GreedySimpleS info)
type GreedySimpleS info = And (Fix (BasicState info)) (And (Simple (TIState info)) (And (Simple (SimpleState info)) (Simple (OverloadingState info))))
solveSimple :: (Solvable constraint (GreedySimple info), TypeConstraintInfo info) => SolveOptions -> [constraint] -> GreedySimple info (SolveResult info)
greedySimpleConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (GreedySimple info)) => ConstraintSolver constraint info


module Top.Solver.TypeGraph
type TG info = BasicMonad (TGS info)
type TGS info = And (Fix (BasicState info)) (And (Simple (TIState info)) (And (Simple (TypeGraphState info)) (Simple (OverloadingState info))))
solveTypeGraph :: (Solvable constraint (TG info), TypeConstraintInfo info) => TG info () -> SolveOptions -> [constraint] -> TG info (SolveResult info)
typegraphConstraintSolver :: (TypeConstraintInfo info, Solvable constraint (TG info)) => PathHeuristics info -> ConstraintSolver constraint info
typegraphConstraintSolverDefault :: (TypeConstraintInfo info, Solvable constraint (TG info)) => ConstraintSolver constraint info