Top.Interface.TypeInference

Documentation

data ClassTI

Constructors

ClassTI

Instances

Embedded ClassTI (Simple (TIState info) x m) (TIState info)

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 where

Methods

getUnique :: m Int

setUnique :: Int -> m ()

setTypeSynonyms :: OrderedTypeSynonyms -> m ()

getTypeSynonyms :: m OrderedTypeSynonyms

getSkolems :: m [([Int], info, Tps)]

setSkolems :: [([Int], info, Tps)] -> m ()

allTypeSchemes :: m (Map Int (Scheme Predicates))

getTypeScheme :: Int -> m (Scheme Predicates)

storeTypeScheme :: Int -> Scheme Predicates -> m ()

Instances

(Monad m, Embedded ClassTI (s (StateFixT s m)) t, HasTI (Select t (StateFixT s m)) info) => HasTI (StateFixT s m) info

(MonadState s m, Embedded ClassTI s (TIState info)) => HasTI (Select (TIState info) m) info

nextUnique :: HasTI m info => m Int

zipWithUniques :: HasTI m info => (Int -> a -> b) -> [a] -> m [b]

Instantiation and skolemization

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

makeConsistent :: (HasTI m info, HasBasic m info, HasSubst m info) => m ()

First, make the substitution consistent. Then check the skolem constants(?)

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)