Language.Lambda.SystemF.TypeCheck

Documentation

type UniqueSupply n = [n]

type Context' n t = Map n t

typecheck :: (Ord name, Pretty name) => SystemFExpr name -> Typecheck name (Ty name)

typecheckTopLevel :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckLet :: (Pretty name, Ord name) => Context name -> name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckExpr :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckVar :: Ord name => Context name -> name -> Typecheck name (Ty name)

typecheckVarAnn :: (Ord name, Pretty name) => Context name -> name -> Ty name -> Typecheck name (Ty name)

typecheckAbs :: (Ord name, Pretty name) => Context name -> name -> Ty name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckApp :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckTyAbs :: (Ord name, Pretty name) => Context name -> name -> SystemFExpr name -> Typecheck name (Ty name)

typecheckTyApp :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Ty name -> Typecheck name (Ty name)

typecheckVar' :: Ord name => Context name -> name -> Maybe (Ty name)

liftForAlls :: Ty name -> Ty name

liftForAlls' :: Ty name -> ([name], Ty name)

isTyEquivalent :: Ord name => Ty name -> Ty name -> Bool

areForAllsEquivalent :: Ord name => (name, Ty name) -> (name, Ty name) -> Bool

tyUnique :: Typecheck name name

tyMismatchError :: Pretty ty => ty -> ty -> LambdaException

tyAppMismatchError :: (Ord name, Pretty name) => Context name -> SystemFExpr name -> Ty name -> Typecheck name LambdaException