FrontEnd.Tc.Monad

Documentation

data CoerceTerm

Constructors

CTId

CTAp [Type]

CTAbs [Tyvar]

CTFun CoerceTerm

CTCompose CoerceTerm CoerceTerm

Instances

Show CoerceTerm

Monoid CoerceTerm

UnVar Type => UnVar CoerceTerm

data Tc a

Instances

Monad Tc

Functor Tc

MonadFix Tc

MonadIO Tc

UniqueProducer Tc

MonadSrcLoc Tc

OptionMonad Tc

MonadWarn Tc

MonadReader TcEnv Tc

MonadWriter Output Tc

data TcInfo

information that is passed into the type checker.

Constructors

TcInfo

Fields

tcInfoEnv :: TypeEnv

tcInfoSigEnv :: TypeEnv

tcInfoModName :: Module

tcInfoKindInfo :: KindEnv

tcInfoClassHierarchy :: ClassHierarchy

type TypeEnv = Map Name Sigma

data TcEnv

Constructors

TcEnv

Fields

tcInfo :: TcInfo

tcDiagnostics :: [Diagnostic]

tcVarnum :: !(IORef Int)

tcCollectedEnv :: !(IORef (Map Name Sigma))

tcCollectedCoerce :: !(IORef (Map Name CoerceTerm))

tcConcreteEnv :: Map Name Sigma

tcMutableEnv :: Map Name Sigma

tcCurrentScope :: Set MetaVar

tcRecursiveCalls :: Set Name

tcInstanceEnv :: InstanceEnv

tcOptions :: Opt

Instances

MonadReader TcEnv Tc

tcRecursiveCalls_u :: (Set Name -> Set Name) -> TcEnv -> TcEnv

data Output

Constructors

Output

Fields

collectedPreds :: !Preds

existentialPreds :: !Preds

constraints :: !(Seq Constraint)

checkedRules :: !(Seq Rule)

existentialVars :: [Tyvar]

tcWarnings :: !(Seq Warning)

outKnots :: [(Name, Name)]

Instances

Monoid Output

MonadWriter Output Tc

addCoerce :: Name -> CoerceTerm -> Tc ()

addPreds :: Preds -> Tc ()

composeCoerce :: CoerceTerm -> CoerceTerm -> CoerceTerm

addRule :: Rule -> Tc ()

addToCollectedEnv :: TypeEnv -> Tc ()

boxyInstantiate :: Sigma -> Tc ([Type], Rho')

boxySpec :: Sigma -> Tc ([(BoundTV, [Sigma'])], Rho')

deconstructorInstantiate :: Sigma -> Tc Rho'

freeMetaVarsEnv :: Tc (Set MetaVar)

freshInstance :: MetaVarType -> Sigma -> Tc ([Type], Rho)

freshSigma :: Sigma -> Tc Sigma

getClassHierarchy :: Tc ClassHierarchy

getCollectedEnv :: Tc TypeEnv

getCollectedCoerce :: Tc (Map Name CoerceTerm)

getDeName :: DeNameable n => Tc (n -> n)

getKindEnv :: Tc KindEnv

getSigEnv :: Tc TypeEnv

evalFullType :: (MonadIO m, MonadReader TcEnv m) => Type -> m Type

inst :: Instantiate a => Map Int Type -> Map Name Type -> a -> a

listenCheckedRules :: Tc a -> Tc (a, [Rule])

listenPreds :: Tc a -> Tc (a, Preds)

listenCPreds :: Tc a -> Tc (a, (Preds, [Constraint]))

localEnv :: TypeEnv -> Tc a -> Tc a

run a computation with a local environment

lookupName :: Name -> Tc Sigma

newBox :: Kind -> Tc Type

returns a new box and a function to read said box.

newMetaVar :: MetaVarType -> Kind -> Tc Type

newVar :: Kind -> Tc Tyvar

quantify :: [MetaVar] -> [Pred] -> Rho -> Tc Sigma

quantify_n :: [MetaVar] -> [Pred] -> [Rho] -> Tc [Sigma]

runTc :: (MonadIO m, OptionMonad m) => TcInfo -> Tc a -> m a

skolomize :: Sigma -> Tc ([Tyvar], [Pred], Type)

replace bound variables with arbitrary new ones and drop the binding TODO predicates?

tcInfoEmpty :: TcInfo

toSigma :: Sigma -> Sigma

unBox :: Type -> Tc Type

evalType :: (MonadIO m, MonadReader TcEnv m) => Type -> m Type

unificationError :: Type -> Type -> Tc b

varBind :: MetaVar -> Type -> Tc ()

zonkKind :: Kind -> MetaVar -> Tc MetaVar

withContext :: Diagnostic -> Tc a -> Tc a

given a diagnostic and a computation to take place inside the TI-monad, run the computation but during it have the diagnostic at the top of the stack

withMetaVars :: MetaVar -> [Kind] -> ([Sigma] -> Sigma) -> ([Sigma'] -> Tc a) -> Tc a