Safe Haskell	Safe-Inferred
Language	Haskell2010

Gibbon.L0.Typecheck

Contents

Orphan instances

Synopsis

newtype TcM a = TcM (ExceptT Doc PassM a)
runTcM :: TcM a -> PassM (Either Doc a)
err :: Doc -> TcM a
tcProg :: Prog0 -> PassM Prog0
tcFun :: DDefs0 -> Gamma -> FunDef0 -> PassM FunDef0
tcExps :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> [(Bool, Exp0)] -> TcM (Subst, [Ty0], [Exp0])
tcExp :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> Bool -> Exp0 -> TcM (Subst, Ty0, Exp0)
tcCases :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> DDef0 -> [(DataCon, [(Var, Ty0)], Exp0)] -> Bool -> Exp0 -> TcM (Subst, Ty0, [(DataCon, [(Var, Ty0)], Exp0)])
instantiate :: TyScheme -> TcM ([Ty0], Ty0)
generalize :: Gamma -> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme)
instDataConTy :: DDefs0 -> DataCon -> TcM ([Ty0], [Ty0], Ty0)
type Gamma = TyEnv TyScheme
newtype Subst = Subst (Map MetaTv Ty0)
combine :: Ty0 -> Ty0 -> Ty0
emptySubst :: Subst
zonkTy :: Subst -> Ty0 -> Ty0
zonkTyScheme :: Subst -> TyScheme -> TyScheme
zonkTyEnv :: Subst -> Gamma -> Gamma
zonkExp :: Subst -> Exp0 -> Exp0
substTyVarDDef :: DDef0 -> [Ty0] -> TcM DDef0
substTyVarExp :: Map TyVar Ty0 -> Exp0 -> Exp0
substTyVarPrim :: Map TyVar Ty0 -> Prim Ty0 -> Prim Ty0
tyVarToMetaTyl :: [Ty0] -> TcM (Map TyVar Ty0, [Ty0])
tyVarToMetaTy :: Ty0 -> TcM (Map TyVar Ty0, Ty0)
unify :: Exp0 -> Ty0 -> Ty0 -> TcM Subst
unifyl :: Exp0 -> [Ty0] -> [Ty0] -> TcM Subst
unifyVar :: Exp0 -> MetaTv -> Ty0 -> TcM Subst
occursCheck :: MetaTv -> Ty0 -> Bool
ensureEqualTy :: Exp0 -> Ty0 -> Ty0 -> TcM ()

Documentation

newtype TcM a Source #

Constructors

TcM (ExceptT Doc PassM a)

Instances

Instances details

MonadFail TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods fail :: String -> TcM a Source #
Applicative TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods pure :: a -> TcM a Source # (<>) :: TcM (a -> b) -> TcM a -> TcM b Source # liftA2 :: (a -> b -> c) -> TcM a -> TcM b -> TcM c Source # (>) :: TcM a -> TcM b -> TcM b Source # (<*) :: TcM a -> TcM b -> TcM a Source #
Functor TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods fmap :: (a -> b) -> TcM a -> TcM b Source # (<$) :: a -> TcM b -> TcM a Source #
Monad TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods (>>=) :: TcM a -> (a -> TcM b) -> TcM b Source # (>>) :: TcM a -> TcM b -> TcM b Source # return :: a -> TcM a Source #
MonadError Doc TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods throwError :: Doc -> TcM a Source # catchError :: TcM a -> (Doc -> TcM a) -> TcM a Source #
MonadState Int TcM Source #
Instance details Defined in Gibbon.L0.Typecheck Methods get :: TcM Int Source # put :: Int -> TcM () Source # state :: (Int -> (a, Int)) -> TcM a Source #

runTcM :: TcM a -> PassM (Either Doc a) Source #

err :: Doc -> TcM a Source #

tcProg :: Prog0 -> PassM Prog0 Source #

tcFun :: DDefs0 -> Gamma -> FunDef0 -> PassM FunDef0 Source #

tcExps :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> [(Bool, Exp0)] -> TcM (Subst, [Ty0], [Exp0]) Source #

tcExp :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> Bool -> Exp0 -> TcM (Subst, Ty0, Exp0) Source #

tcCases :: DDefs0 -> Subst -> Gamma -> Gamma -> [TyVar] -> DDef0 -> [(DataCon, [(Var, Ty0)], Exp0)] -> Bool -> Exp0 -> TcM (Subst, Ty0, [(DataCon, [(Var, Ty0)], Exp0)]) Source #

instantiate :: TyScheme -> TcM ([Ty0], Ty0) Source #

Instantiate the topmost for-alls of the argument type with meta type variables.

generalize :: Gamma -> Subst -> [TyVar] -> Ty0 -> TcM (Subst, TyScheme) Source #

instDataConTy :: DDefs0 -> DataCon -> TcM ([Ty0], [Ty0], Ty0) Source #

type Gamma = TyEnv TyScheme Source #

newtype Subst Source #

Constructors

Subst (Map MetaTv Ty0)

Instances

Instances details

Out Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods docPrec :: Int -> Subst -> Doc Source # doc :: Subst -> Doc Source # docList :: [Subst] -> Doc Source #
Semigroup Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods (<>) :: Subst -> Subst -> Subst Source # sconcat :: NonEmpty Subst -> Subst Source # stimes :: Integral b => b -> Subst -> Subst Source #
Generic Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Associated Types type Rep Subst :: Type -> Type Source # Methods from :: Subst -> Rep Subst x Source # to :: Rep Subst x -> Subst Source #
Read Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods readsPrec :: Int -> ReadS Subst Source # readList :: ReadS [Subst] Source # readPrec :: ReadPrec Subst Source # readListPrec :: ReadPrec [Subst] Source #
Show Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods showsPrec :: Int -> Subst -> ShowS Source # show :: Subst -> String Source # showList :: [Subst] -> ShowS Source #
Eq Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods (==) :: Subst -> Subst -> Bool Source # (/=) :: Subst -> Subst -> Bool Source #
Ord Subst Source #
Instance details Defined in Gibbon.L0.Typecheck Methods compare :: Subst -> Subst -> Ordering Source # (<) :: Subst -> Subst -> Bool Source # (<=) :: Subst -> Subst -> Bool Source # (>) :: Subst -> Subst -> Bool Source # (>=) :: Subst -> Subst -> Bool Source # max :: Subst -> Subst -> Subst Source # min :: Subst -> Subst -> Subst Source #
type Rep Subst Source #
Instance details Defined in Gibbon.L0.Typecheck type Rep Subst = D1 ('MetaData "Subst" "Gibbon.L0.Typecheck" "gibbon-0.3-inplace" 'True) (C1 ('MetaCons "Subst" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map MetaTv Ty0))))

combine :: Ty0 -> Ty0 -> Ty0 Source #

Combine substitutions. In case of substitutions with intersecting keys, we will take the narrower type of the two. e.g. combine [($1, $2)] [($1, IntTy)] should be [($1, IntTy)]. Map.union does a left biased union so it will result in [($1, $2)]

emptySubst :: Subst Source #

zonkTy :: Subst -> Ty0 -> Ty0 Source #

Perform substitutions in the type.

zonkTyScheme :: Subst -> TyScheme -> TyScheme Source #

zonkTyEnv :: Subst -> Gamma -> Gamma Source #

zonkExp :: Subst -> Exp0 -> Exp0 Source #

substTyVarDDef :: DDef0 -> [Ty0] -> TcM DDef0 Source #

substTyVarExp :: Map TyVar Ty0 -> Exp0 -> Exp0 Source #

substTyVarPrim :: Map TyVar Ty0 -> Prim Ty0 -> Prim Ty0 Source #

tyVarToMetaTyl :: [Ty0] -> TcM (Map TyVar Ty0, [Ty0]) Source #

tyVarToMetaTy :: Ty0 -> TcM (Map TyVar Ty0, Ty0) Source #

Replace the specified quantified type variables by given meta type variables.

unify :: Exp0 -> Ty0 -> Ty0 -> TcM Subst Source #

unifyl :: Exp0 -> [Ty0] -> [Ty0] -> TcM Subst Source #

unifyVar :: Exp0 -> MetaTv -> Ty0 -> TcM Subst Source #

occursCheck :: MetaTv -> Ty0 -> Bool Source #

ensureEqualTy :: Exp0 -> Ty0 -> Ty0 -> TcM () Source #

Orphan instances

FreeVars a => FreeVars (TyEnv a) Source #
Instance details Methods gFreeVars :: TyEnv a -> Set Var Source #