Agda-2.3.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.TypeChecking.Monad.Base

Contents

- Type checking state
  - Interface
  - Closure
  - Constraints
- Open things
- Judgements
  - Meta variables
  - Interaction meta variables
  - Signature
  - Injectivity
  - Mutual blocks
  - Statistics
  - Trace
  - Builtin things
- Type checking environment
  - Context
  - Let bindings
  - Abstract mode
- Type checking errors
- Type checking monad transformer

Synopsis

- data TCState = TCSt {
  - stFreshThings :: FreshThings
  - stMetaStore :: MetaStore
  - stInteractionPoints :: InteractionPoints
  - stAwakeConstraints :: Constraints
  - stSleepingConstraints :: Constraints
  - stSignature :: Signature
  - stImports :: Signature
  - stImportedModules :: Set ModuleName
  - stModuleToSource :: ModuleToSource
  - stVisitedModules :: VisitedModules
  - stCurrentModule :: Maybe ModuleName
  - stScope :: ScopeInfo
  - stPragmaOptions :: PragmaOptions
  - stStatistics :: Statistics
  - stExtLambdaTele :: Map QName (Int, Int)
  - stMutualBlocks :: Map MutualId (Set QName)
  - stLocalBuiltins :: BuiltinThings PrimFun
  - stImportedBuiltins :: BuiltinThings PrimFun
  - stHaskellImports :: Set String
  - stPersistent :: PersistentTCState
  }
- data PersistentTCState = PersistentTCSt {
  - stDecodedModules :: DecodedModules
  - stPersistentOptions :: CommandLineOptions
  }
- data FreshThings = Fresh {
  - fMeta :: MetaId
  - fInteraction :: InteractionId
  - fMutual :: MutualId
  - fName :: NameId
  - fCtx :: CtxId
  - fProblem :: ProblemId
  - fInteger :: Integer
  }
- initState :: TCState
- stBuiltinThings :: TCState -> BuiltinThings PrimFun
- newtype ProblemId = ProblemId Nat
- data ModuleInfo = ModuleInfo {
  - miInterface :: Interface
  - miWarnings :: Bool
  - miTimeStamp :: ClockTime
  }
- type VisitedModules = Map TopLevelModuleName ModuleInfo
- type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)
- data Interface = Interface {
  - iImportedModules :: [ModuleName]
  - iModuleName :: ModuleName
  - iScope :: Map ModuleName Scope
  - iInsideScope :: ScopeInfo
  - iSignature :: Signature
  - iBuiltin :: BuiltinThings String
  - iHaskellImports :: Set String
  - iHighlighting :: HighlightingInfo
  - iPragmaOptions :: [OptionsPragma]
  }
- data Closure a = Closure {
  - clSignature :: Signature
  - clEnv :: TCEnv
  - clScope :: ScopeInfo
  - clValue :: a
  }
- buildClosure :: a -> TCM (Closure a)
- type Constraints = [ProblemConstraint]
- data ProblemConstraint = PConstr {
  - constraintProblem :: ProblemId
  - theConstraint :: Closure Constraint
  }
- data Constraint
  - = ValueCmp Comparison Type Term Term
  - | ElimCmp [Polarity] Type Term [Elim] [Elim]
  - | TypeCmp Comparison Type Type
  - | TelCmp Type Type Comparison Telescope Telescope
  - | SortCmp Comparison Sort Sort
  - | LevelCmp Comparison Level Level
  - | UnBlock MetaId
  - | Guarded Constraint ProblemId
  - | IsEmpty Type
  - | FindInScope MetaId
- data Comparison
  - = CmpEq
  - | CmpLeq
- data Open a = OpenThing [CtxId] a
- data Judgement t a
  - = HasType {
    - jMetaId :: a
    - jMetaType :: t
    }
  - | IsSort {
    - jMetaId :: a
    - jMetaType :: t
    }
- data MetaVariable = MetaVar {
  - mvInfo :: MetaInfo
  - mvPriority :: MetaPriority
  - mvPermutation :: Permutation
  - mvJudgement :: Judgement Type MetaId
  - mvInstantiation :: MetaInstantiation
  - mvListeners :: Set Listener
  - mvFrozen :: Frozen
  }
- data Listener
  - = EtaExpand MetaId
  - | CheckConstraint Nat ProblemConstraint
- data Frozen
  - = Frozen
  - | Instantiable
- data MetaInstantiation
  - = InstV Term
  - | InstS Term
  - | Open
  - | OpenIFS
  - | BlockedConst Term
  - | PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))
- newtype MetaPriority = MetaPriority Int
- type MetaInfo = Closure Range
- type MetaStore = Map MetaId MetaVariable
- normalMetaPriority :: MetaPriority
- lowMetaPriority :: MetaPriority
- highMetaPriority :: MetaPriority
- getMetaInfo :: MetaVariable -> MetaInfo
- getMetaScope :: MetaVariable -> ScopeInfo
- getMetaEnv :: MetaVariable -> TCEnv
- getMetaSig :: MetaVariable -> Signature
- type InteractionPoints = Map InteractionId MetaId
- newtype InteractionId = InteractionId Nat
- data Signature = Sig {
  - sigSections :: Sections
  - sigDefinitions :: Definitions
  }
- type Sections = Map ModuleName Section
- type Definitions = Map QName Definition
- data Section = Section {
  - secTelescope :: Telescope
  - secFreeVars :: Nat
  }
- emptySignature :: Signature
- data DisplayForm = Display Nat [Term] DisplayTerm
- data DisplayTerm
  - = DWithApp [DisplayTerm] Args
  - | DCon QName [Arg DisplayTerm]
  - | DDef QName [Arg DisplayTerm]
  - | DDot Term
  - | DTerm Term
- defaultDisplayForm :: QName -> [Open DisplayForm]
- data Definition = Defn {
  - defRelevance :: Relevance
  - defName :: QName
  - defType :: Type
  - defDisplay :: [Open DisplayForm]
  - defMutual :: MutualId
  - defCompiledRep :: CompiledRepresentation
  - theDef :: Defn
  }
- type HaskellCode = String
- type HaskellType = String
- type EpicCode = String
- type JSCode = Exp
- data HaskellRepresentation
  - = HsDefn HaskellType HaskellCode
  - | HsType HaskellType
- data Polarity
  - = Covariant
  - | Contravariant
  - | Invariant
- data CompiledRepresentation = CompiledRep {
  - compiledHaskell :: Maybe HaskellRepresentation
  - compiledEpic :: Maybe EpicCode
  - compiledJS :: Maybe JSCode
  }
- noCompiledRep :: CompiledRepresentation
- data Occurrence
  - = Positive
  - | Negative
  - | Unused
- data Defn
  - = Axiom
  - | Function {
    - funClauses :: [Clause]
    - funCompiled :: CompiledClauses
    - funInv :: FunctionInverse
    - funPolarity :: [Polarity]
    - funArgOccurrences :: [Occurrence]
    - funAbstr :: IsAbstract
    - funDelayed :: Delayed
    - funProjection :: Maybe (QName, Int)
    - funStatic :: Bool
    }
  - | Datatype {
    - dataPars :: Nat
    - dataIxs :: Nat
    - dataInduction :: Induction
    - dataClause :: Maybe Clause
    - dataCons :: [QName]
    - dataSort :: Sort
    - dataPolarity :: [Polarity]
    - dataArgOccurrences :: [Occurrence]
    - dataAbstr :: IsAbstract
    }
  - | Record {
    - recPars :: Nat
    - recClause :: Maybe Clause
    - recCon :: QName
    - recNamedCon :: Bool
    - recConType :: Type
    - recFields :: [Arg QName]
    - recTel :: Telescope
    - recPolarity :: [Polarity]
    - recArgOccurrences :: [Occurrence]
    - recEtaEquality :: Bool
    - recAbstr :: IsAbstract
    }
  - | Constructor {
    - conPars :: Nat
    - conSrcCon :: QName
    - conData :: QName
    - conAbstr :: IsAbstract
    - conInd :: Induction
    }
  - | Primitive {
    - primAbstr :: IsAbstract
    - primName :: String
    - primClauses :: Maybe [Clause]
    - primCompiled :: Maybe CompiledClauses
    }
- defIsRecord :: Defn -> Bool
- newtype Fields = Fields [(Name, Type)]
- data Reduced no yes
  - = NoReduction no
  - | YesReduction yes
- data IsReduced
  - = NotReduced
  - | Reduced (Blocked ())
- data MaybeReduced a = MaybeRed {
  - isReduced :: IsReduced
  - ignoreReduced :: a
  }
- type MaybeReducedArgs = [MaybeReduced (Arg Term)]
- notReduced :: a -> MaybeReduced a
- reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)
- data PrimFun = PrimFun {
  - primFunName :: QName
  - primFunArity :: Arity
  - primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)
  }
- defClauses :: Definition -> [Clause]
- defCompiled :: Definition -> Maybe CompiledClauses
- defJSDef :: Definition -> Maybe JSCode
- defEpicDef :: Definition -> Maybe EpicCode
- data Delayed
  - = Delayed
  - | NotDelayed
- defDelayed :: Definition -> Delayed
- defAbstract :: Definition -> IsAbstract
- data FunctionInverse
  - = NotInjective
  - | Inverse (Map TermHead Clause)
- data TermHead
  - = SortHead
  - | PiHead
  - | ConHead QName
- newtype MutualId = MutId Int32
- type Statistics = Map String Integer
- data Call
  - = CheckClause Type Clause (Maybe Clause)
  - | forall a . CheckPattern Pattern Telescope Type (Maybe a)
  - | CheckLetBinding LetBinding (Maybe ())
  - | InferExpr Expr (Maybe (Term, Type))
  - | CheckExpr Expr Type (Maybe Term)
  - | CheckDotPattern Expr Term (Maybe Constraints)
  - | CheckPatternShadowing Clause (Maybe ())
  - | IsTypeCall Expr Sort (Maybe Type)
  - | IsType_ Expr (Maybe Type)
  - | InferVar Name (Maybe (Term, Type))
  - | InferDef Range QName (Maybe (Term, Type))
  - | CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type))
  - | CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ())
  - | CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ())
  - | CheckConstructor QName Telescope Sort Constructor (Maybe ())
  - | CheckFunDef Range Name [Clause] (Maybe ())
  - | CheckPragma Range Pragma (Maybe ())
  - | CheckPrimitive Range Name Expr (Maybe ())
  - | CheckIsEmpty Type (Maybe ())
  - | CheckWithFunctionType Expr (Maybe ())
  - | CheckSectionApplication Range ModuleName ModuleApplication (Maybe ())
  - | ScopeCheckExpr Expr (Maybe Expr)
  - | ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
  - | ScopeCheckLHS Name Pattern (Maybe LHS)
  - | forall a . TermFunDef Range Name [Clause] (Maybe a)
  - | forall a . SetRange Range (Maybe a)
- data BuiltinDescriptor
  - = BuiltinData (TCM Type) [String]
  - | BuiltinDataCons (TCM Type)
  - | BuiltinPrim String (Term -> TCM ())
  - | BuiltinPostulate (TCM Type)
  - | BuiltinUnknown (Maybe (TCM Type)) (Term -> TCM ())
- data BuiltinInfo = BuiltinInfo {
  - builtinName :: String
  - builtinDesc :: BuiltinDescriptor
  }
- type BuiltinThings pf = Map String (Builtin pf)
- data Builtin pf
  - = Builtin Term
  - | Prim pf
- data TCEnv = TCEnv {
  - envContext :: Context
  - envLetBindings :: LetBindings
  - envCurrentModule :: ModuleName
  - envAnonymousModules :: [(ModuleName, Nat)]
  - envImportPath :: [TopLevelModuleName]
  - envMutualBlock :: Maybe MutualId
  - envSolvingConstraints :: Bool
  - envActiveProblems :: [ProblemId]
  - envAbstractMode :: AbstractMode
  - envTopLevel :: Bool
  - envRelevance :: Relevance
  - envDisplayFormsEnabled :: Bool
  - envReifyInteractionPoints :: Bool
  - envEtaContractImplicit :: Bool
  - envRange :: Range
  - envCall :: Maybe (Closure Call)
  }
- initEnv :: TCEnv
- type Context = [ContextEntry]
- data ContextEntry = Ctx {
  - ctxId :: CtxId
  - ctxEntry :: Arg (Name, Type)
  }
- newtype CtxId = CtxId Nat
- type LetBindings = Map Name (Open (Term, Arg Type))
- data AbstractMode
  - = AbstractMode
  - | ConcreteMode
  - | IgnoreAbstractMode
- data Occ
  - = OccCon {
    - occDatatype :: QName
    - occConstructor :: QName
    - occPosition :: OccPos
    }
  - | OccClause {
    - occFunction :: QName
    - occClause :: Int
    - occPosition :: OccPos
    }
- data OccPos
  - = NonPositively
  - | ArgumentTo Nat QName
- data CallInfo = CallInfo {
  - callInfoRange :: Range
  - callInfoCall :: String
  }
- data TerminationError = TerminationError {
  - termErrFunctions :: [QName]
  - termErrCalls :: [CallInfo]
  }
- data TypeError
  - = InternalError String
  - | NotImplemented String
  - | NotSupported String
  - | CompilationError String
  - | TerminationCheckFailed [TerminationError]
  - | PropMustBeSingleton
  - | DataMustEndInSort Term
  - | ShouldEndInApplicationOfTheDatatype Type
  - | ShouldBeAppliedToTheDatatypeParameters Term Term
  - | ShouldBeApplicationOf Type QName
  - | ConstructorPatternInWrongDatatype QName QName
  - | IndicesNotConstructorApplications [Arg Term]
  - | IndexVariablesNotDistinct [Arg Term]
  - | IndexFreeInParameter Nat [Arg Term]
  - | DoesNotConstructAnElementOf QName Term
  - | DifferentArities
  - | WrongHidingInLHS Type
  - | WrongHidingInLambda Type
  - | WrongHidingInApplication Type
  - | WrongIrrelevanceInLambda Type
  - | NotInductive Term
  - | UninstantiatedDotPattern Expr
  - | IlltypedPattern Pattern Type
  - | TooManyArgumentsInLHS Nat Type
  - | WrongNumberOfConstructorArguments QName Nat Nat
  - | ShouldBeEmpty Type [Pattern]
  - | ShouldBeASort Type
  - | ShouldBePi Type
  - | ShouldBeRecordType Type
  - | NotAProperTerm
  - | SplitOnIrrelevant Pattern (Arg Type)
  - | DefinitionIsIrrelevant QName
  - | VariableIsIrrelevant Name
  - | UnequalLevel Comparison Term Term
  - | UnequalTerms Comparison Term Term Type
  - | UnequalTypes Comparison Type Type
  - | UnequalTelescopes Comparison Telescope Telescope
  - | UnequalRelevance Type Type
  - | UnequalHiding Type Type
  - | UnequalSorts Sort Sort
  - | HeterogeneousEquality Term Type Term Type
  - | NotLeqSort Sort Sort
  - | MetaCannotDependOn MetaId [Nat] Nat
  - | MetaOccursInItself MetaId
  - | GenericError String
  - | BuiltinMustBeConstructor String Expr
  - | NoSuchBuiltinName String
  - | DuplicateBuiltinBinding String Term Term
  - | NoBindingForBuiltin String
  - | NoSuchPrimitiveFunction String
  - | ShadowedModule [ModuleName]
  - | BuiltinInParameterisedModule String
  - | NoRHSRequiresAbsurdPattern [NamedArg Pattern]
  - | AbsurdPatternRequiresNoRHS [NamedArg Pattern]
  - | TooFewFields QName [Name]
  - | TooManyFields QName [Name]
  - | DuplicateFields [Name]
  - | DuplicateConstructors [Name]
  - | UnexpectedWithPatterns [Pattern]
  - | WithClausePatternMismatch Pattern Pattern
  - | FieldOutsideRecord
  - | ModuleArityMismatch ModuleName Telescope [NamedArg Expr]
  - | IncompletePatternMatching Term Args
  - | CoverageFailure QName [[Arg Pattern]]
  - | UnreachableClauses QName [[Arg Pattern]]
  - | CoverageCantSplitOn QName Telescope Args Args
  - | CoverageCantSplitIrrelevantType Type
  - | CoverageCantSplitType Type
  - | NotStrictlyPositive QName [Occ]
  - | LocalVsImportedModuleClash ModuleName
  - | UnsolvedMetas [Range]
  - | UnsolvedConstraints Constraints
  - | CyclicModuleDependency [TopLevelModuleName]
  - | FileNotFound TopLevelModuleName [AbsolutePath]
  - | OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName
  - | AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath]
  - | ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath]
  - | ClashingFileNamesFor ModuleName [AbsolutePath]
  - | ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath
  - | BothWithAndRHS
  - | NotInScope [QName]
  - | NoSuchModule QName
  - | AmbiguousName QName [QName]
  - | AmbiguousModule QName [ModuleName]
  - | UninstantiatedModule QName
  - | ClashingDefinition QName QName
  - | ClashingModule ModuleName ModuleName
  - | ClashingImport Name QName
  - | ClashingModuleImport Name ModuleName
  - | PatternShadowsConstructor Name QName
  - | ModuleDoesntExport QName [ImportedName]
  - | DuplicateImports QName [ImportedName]
  - | InvalidPattern Pattern
  - | RepeatedVariablesInPattern [Name]
  - | NotAModuleExpr Expr
  - | NotAnExpression Expr
  - | NotAValidLetBinding NiceDeclaration
  - | NothingAppliedToHiddenArg Expr
  - | NothingAppliedToInstanceArg Expr
  - | NoParseForApplication [Expr]
  - | AmbiguousParseForApplication [Expr] [Expr]
  - | NoParseForLHS Pattern
  - | AmbiguousParseForLHS Pattern [Pattern]
  - | IFSNoCandidateInScope Type
  - | SafeFlagPostulate Name
  - | SafeFlagPragma [String]
  - | SafeFlagPrimTrustMe
- data TCErr'
  - = TypeError TCState (Closure TypeError)
  - | Exception Range String
  - | IOException Range IOException
  - | PatternErr TCState
- data TCErr = TCErr {
  - errHighlighting :: Maybe (HighlightingInfo, ModuleToSource)
  - errError :: TCErr'
  }
- newtype TCMT m a = TCM {
  - unTCM :: IORef TCState -> TCEnv -> m a
  }
- type TCM = TCMT IO
- class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where
  - liftTCM :: TCM a -> tcm a
- catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a
- mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a
- pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a
- patternViolation :: TCM a
- internalError :: MonadTCM tcm => String -> tcm a
- typeError :: MonadTCM tcm => TypeError -> tcm a
- runTCM :: TCMT IO a -> IO (Either TCErr a)
- runTCM' :: MonadIO m => TCMT m a -> m a
- extendlambdaname :: [Char]

# Type checking state

data TCState

Constructors

TCSt |
Fields stFreshThings :: FreshThings stMetaStore :: MetaStore stInteractionPoints :: InteractionPoints stAwakeConstraints :: Constraints stSleepingConstraints :: Constraints stSignature :: Signature stImports :: Signature stImportedModules :: Set ModuleName stModuleToSource :: ModuleToSource stVisitedModules :: VisitedModules stCurrentModule :: Maybe ModuleName The current module is available after it has been type checked. stScope :: ScopeInfo stPragmaOptions :: PragmaOptions Options applying to the current file. `OPTIONS` pragmas only affect this field. stStatistics :: Statistics stExtLambdaTele :: Map QName (Int, Int) stMutualBlocks :: Map MutualId (Set QName) stLocalBuiltins :: BuiltinThings PrimFun stImportedBuiltins :: BuiltinThings PrimFun stHaskellImports :: Set String Imports that should be generated by the compiler (this includes imports from imported modules). stPersistent :: PersistentTCState

Instances

MonadState TCState RecPatM |
MonadState TCState Unify |
HasFresh i FreshThings => HasFresh i TCState |
MonadIO m => MonadState TCState (TCMT m) |

data PersistentTCState

A part of the state which is not reverted when an error is thrown or the state is reset.

Constructors

PersistentTCSt |
Fields stDecodedModules :: DecodedModules stPersistentOptions :: CommandLineOptions Options which apply to all files, unless overridden.

data FreshThings

Constructors

Fresh |
Fields fMeta :: MetaId fInteraction :: InteractionId fMutual :: MutualId fName :: NameId fCtx :: CtxId fProblem :: ProblemId fInteger :: Integer Can be used for various things.

Instances

Show FreshThings |
HasFresh Integer FreshThings |
HasFresh NameId FreshThings |
HasFresh MetaId FreshThings |
HasFresh CtxId FreshThings |
HasFresh MutualId FreshThings |
HasFresh InteractionId FreshThings |
HasFresh ProblemId FreshThings |

initState :: TCState

stBuiltinThings :: TCState -> BuiltinThings PrimFun

newtype ProblemId

Constructors

ProblemId Nat |

Instances

Enum ProblemId |
Eq ProblemId |
Integral ProblemId |
Data ProblemId |
Num ProblemId |
Ord ProblemId |
Real ProblemId |
Show ProblemId |
Typeable ProblemId |
HasFresh ProblemId FreshThings |

## Interface

data ModuleInfo

Constructors

ModuleInfo |
Fields miInterface :: Interface miWarnings :: Bool `True` if warnings were encountered when the module was type checked. miTimeStamp :: ClockTime The modification time stamp of the interface file when the interface was read or written. Alternatively, if warnings were encountered (in which case there may not be any up-to-date interface file), the time at which the interface was produced (approximately).

type VisitedModules = Map TopLevelModuleName ModuleInfo

type DecodedModules = Map TopLevelModuleName (Interface, ClockTime)

data Interface

Constructors

Interface |
Fields iImportedModules :: [ModuleName] iModuleName :: ModuleName iScope :: Map ModuleName Scope iInsideScope :: ScopeInfo iSignature :: Signature iBuiltin :: BuiltinThings String iHaskellImports :: Set String Haskell imports listed in (transitively) imported modules are not included here. iHighlighting :: HighlightingInfo iPragmaOptions :: [OptionsPragma] Pragma options set in the file.

Instances

Data Interface |
Show Interface |
Typeable Interface |
EmbPrj Interface |
InstantiateFull Interface |

## Closure

data Closure a

Constructors

Closure |
Fields clSignature :: Signature clEnv :: TCEnv clScope :: ScopeInfo clValue :: a

Instances

Typeable1 Closure |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |
Data a => Data (Closure a) |
Show a => Show (Closure a) |
HasRange a => HasRange (Closure a) |
PrettyTCM a => PrettyTCM (Closure a) |
InstantiateFull a => InstantiateFull (Closure a) |
Normalise a => Normalise (Closure a) |
Reduce a => Reduce (Closure a) |
Instantiate a => Instantiate (Closure a) |
MentionsMeta a => MentionsMeta (Closure a) |

buildClosure :: a -> TCM (Closure a)

## Constraints

type Constraints = [ProblemConstraint]

data ProblemConstraint

Constructors

PConstr |
Fields constraintProblem :: ProblemId theConstraint :: Closure Constraint

Instances

Show ProblemConstraint |
Typeable ProblemConstraint |
PrettyTCM ProblemConstraint |
InstantiateFull ProblemConstraint |
Normalise ProblemConstraint |
MentionsMeta ProblemConstraint |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) |

data Constraint

Constructors

ValueCmp Comparison Type Term Term |
ElimCmp [Polarity] Type Term [Elim] [Elim] |
TypeCmp Comparison Type Type |
TelCmp Type Type Comparison Telescope Telescope | the two types are for the error message only
SortCmp Comparison Sort Sort |
LevelCmp Comparison Level Level |
UnBlock MetaId |
Guarded Constraint ProblemId |
IsEmpty Type |
FindInScope MetaId |

Instances

Eq Constraint |
Show Constraint |
Typeable Constraint |
Raise Constraint |
PrettyTCM Constraint |
InstantiateFull Constraint |
Normalise Constraint |
Reduce Constraint |
Instantiate Constraint |
MentionsMeta Constraint |
Reify Constraint (OutputConstraint Expr Expr) |

data Comparison

Constructors

CmpEq |
CmpLeq |

Instances

Eq Comparison |
Show Comparison |
Typeable Comparison |
PrettyTCM Comparison |

# Open things

data Open a

A thing tagged with the context it came from.

Constructors

OpenThing [CtxId] a |

Instances

Functor Open |
Typeable1 Open |
Data a => Data (Open a) |
Show a => Show (Open a) |
EmbPrj a => EmbPrj (Open a) |
InstantiateFull a => InstantiateFull (Open a) |

# Judgements

data Judgement t a

Constructors

HasType |
Fields jMetaId :: a jMetaType :: t
IsSort |
Fields jMetaId :: a jMetaType :: t

Instances

Typeable2 Judgement |
Functor (Judgement t) |
Foldable (Judgement t) |
Traversable (Judgement t) |
(Data t, Data a) => Data (Judgement t a) |
(Show t, Show a) => Show (Judgement t a) |
(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b) |
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |

## Meta variables

data MetaVariable

Constructors

MetaVar |
Fields mvInfo :: MetaInfo mvPriority :: MetaPriority some metavariables are more eager to be instantiated mvPermutation :: Permutation a metavariable doesn't have to depend on all variables in the context, this permutation will throw away the ones it does not depend on mvJudgement :: Judgement Type MetaId mvInstantiation :: MetaInstantiation mvListeners :: Set Listener meta variables scheduled for eta-expansion but blocked by this one mvFrozen :: Frozen are we past the point where we can instantiate this meta variable?

Instances

Typeable MetaVariable |
SetRange MetaVariable |
HasRange MetaVariable |

data Listener

Constructors

EtaExpand MetaId |
CheckConstraint Nat ProblemConstraint |

Instances

Eq Listener |
Ord Listener |
Typeable Listener |

data Frozen

Frozen meta variable cannot be instantiated by unification. This serves to prevent the completion of a definition by its use outside of the current block. (See issues 118, 288, 399).

Constructors

Frozen | Do not instantiate.
Instantiable |

Instances

Eq Frozen |
Show Frozen |

data MetaInstantiation

Constructors

InstV Term | solved by term
InstS Term | solved by `Lam .. Sort s`
Open | unsolved
OpenIFS | open, to be instantiated as implicit from scope
BlockedConst Term | solution blocked by unsolved constraints
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool)) |

Instances

Show MetaInstantiation |
Typeable MetaInstantiation |

newtype MetaPriority

Constructors

MetaPriority Int |

Instances

Eq MetaPriority |
Ord MetaPriority |
Show MetaPriority |

type MetaInfo = Closure Range

TODO: Not so nice.

type MetaStore = Map MetaId MetaVariable

normalMetaPriority :: MetaPriority

lowMetaPriority :: MetaPriority

highMetaPriority :: MetaPriority

getMetaInfo :: MetaVariable -> MetaInfo

getMetaScope :: MetaVariable -> ScopeInfo

getMetaEnv :: MetaVariable -> TCEnv

getMetaSig :: MetaVariable -> Signature

## Interaction meta variables

type InteractionPoints = Map InteractionId MetaId

newtype InteractionId

Constructors

InteractionId Nat |

Instances

Enum InteractionId |
Eq InteractionId |
Integral InteractionId |
Num InteractionId |
Ord InteractionId |
Real InteractionId |
Show InteractionId |
HasFresh InteractionId FreshThings |
ToConcrete InteractionId Expr |

## Signature

data Signature

Constructors

Sig |
Fields sigSections :: Sections sigDefinitions :: Definitions

Instances

Data Signature |
Show Signature |
Typeable Signature |
EmbPrj Signature |
InstantiateFull Signature |

type Sections = Map ModuleName Section

type Definitions = Map QName Definition

data Section

Constructors

Section |
Fields secTelescope :: Telescope secFreeVars :: Nat This is the number of parameters when we're inside the section and 0 outside. It's used to know how much of the context to apply function from the section to when translating from abstract to internal syntax.

Instances

Data Section |
Show Section |
Typeable Section |
EmbPrj Section |
InstantiateFull Section |

emptySignature :: Signature

data DisplayForm

Constructors

Display Nat [Term] DisplayTerm | The three arguments are: `n`: number of free variables; Patterns for arguments, one extra free var which represents pattern vars. There should `n` of them. Display form. `n` free variables.

Instances

Data DisplayForm |
Show DisplayForm |
Typeable DisplayForm |
Raise DisplayForm |
EmbPrj DisplayForm |
InstantiateFull DisplayForm |
Normalise DisplayForm |

data DisplayTerm

Constructors

DWithApp [DisplayTerm] Args |
DCon QName [Arg DisplayTerm] |
DDef QName [Arg DisplayTerm] |
DDot Term |
DTerm Term |

Instances

Data DisplayTerm |
Show DisplayTerm |
Typeable DisplayTerm |
Raise DisplayTerm |
Subst DisplayTerm |
Apply DisplayTerm |
EmbPrj DisplayTerm |
PrettyTCM DisplayTerm |
InstantiateFull DisplayTerm |
Reify DisplayTerm Expr |

defaultDisplayForm :: QName -> [Open DisplayForm]

data Definition

Constructors

Defn |
Fields defRelevance :: Relevance Some defs can be irrelevant (but not hidden). defName :: QName defType :: Type Type of the lifted definition. defDisplay :: [Open DisplayForm] defMutual :: MutualId defCompiledRep :: CompiledRepresentation theDef :: Defn

Instances

Data Definition |
Show Definition |
Typeable Definition |
Abstract Definition |
Apply Definition |
EmbPrj Definition |
InstantiateFull Definition |

type HaskellCode = String

type HaskellType = String

type EpicCode = String

type JSCode = Exp

data HaskellRepresentation

Constructors

HsDefn HaskellType HaskellCode |
HsType HaskellType |

Instances

Data HaskellRepresentation |
Show HaskellRepresentation |
Typeable HaskellRepresentation |
EmbPrj HaskellRepresentation |

data Polarity

Constructors

Covariant |
Contravariant |
Invariant |

Instances

Eq Polarity |
Data Polarity |
Show Polarity |
Typeable Polarity |
EmbPrj Polarity |

data CompiledRepresentation

Constructors

CompiledRep |
Fields compiledHaskell :: Maybe HaskellRepresentation compiledEpic :: Maybe EpicCode compiledJS :: Maybe JSCode

Instances

Data CompiledRepresentation |
Show CompiledRepresentation |
Typeable CompiledRepresentation |
EmbPrj CompiledRepresentation |

noCompiledRep :: CompiledRepresentation

data Occurrence

`Positive` means strictly positive and `Negative` means not strictly positive.

Constructors

Positive |
Negative |
Unused |

Instances

Eq Occurrence |
Data Occurrence |
Ord Occurrence |
Show Occurrence |
Typeable Occurrence |
SemiRing Occurrence |
EmbPrj Occurrence |

data Defn

Constructors

Axiom |
Function |
Fields funClauses :: [Clause] funCompiled :: CompiledClauses funInv :: FunctionInverse funPolarity :: [Polarity] funArgOccurrences :: [Occurrence] funAbstr :: IsAbstract funDelayed :: Delayed Are the clauses of this definition delayed? funProjection :: Maybe (QName, Int) Is it a record projection? If yes, then return the name of the record type and index of the record argument. Start counting with 1, because 0 means that it is already applied to the record. (Can happen in module instantiation.) This information is used in the termination checker. funStatic :: Bool Should calls to this function be normalised at compile-time?
Datatype |
Fields dataPars :: Nat dataIxs :: Nat dataInduction :: Induction dataClause :: Maybe Clause dataCons :: [QName] dataSort :: Sort dataPolarity :: [Polarity] dataArgOccurrences :: [Occurrence] dataAbstr :: IsAbstract
Record |
Fields recPars :: Nat recClause :: Maybe Clause recCon :: QName Constructor name. recNamedCon :: Bool recConType :: Type The record constructor's type. recFields :: [Arg QName] recTel :: Telescope The record field telescope recPolarity :: [Polarity] recArgOccurrences :: [Occurrence] recEtaEquality :: Bool recAbstr :: IsAbstract
Constructor |
Fields conPars :: Nat conSrcCon :: QName conData :: QName conAbstr :: IsAbstract conInd :: Induction Inductive or coinductive?
Primitive | Primitive or builtin functions.
Fields primAbstr :: IsAbstract primName :: String primClauses :: Maybe [Clause] `Nothing` for primitive functions, ``Just` something` for builtin functions. primCompiled :: Maybe CompiledClauses `Nothing` for primitive functions, ``Just` something` for builtin functions.

Instances

Data Defn |
Show Defn |
Typeable Defn |
Abstract Defn |
Apply Defn |
EmbPrj Defn |
InstantiateFull Defn |

defIsRecord :: Defn -> Bool

newtype Fields

Constructors

Fields [(Name, Type)] |

Instances

Data Fields |
Typeable Fields |

data Reduced no yes

Constructors

NoReduction no |
YesReduction yes |

Instances

Typeable2 Reduced |
Functor (Reduced no) |

data IsReduced

Constructors

NotReduced |
Reduced (Blocked ()) |

data MaybeReduced a

Constructors

MaybeRed |
Fields isReduced :: IsReduced ignoreReduced :: a

Instances

Functor MaybeReduced |

type MaybeReducedArgs = [MaybeReduced (Arg Term)]

notReduced :: a -> MaybeReduced a

reduced :: Blocked (Arg Term) -> MaybeReduced (Arg Term)

data PrimFun

Constructors

PrimFun |
Fields primFunName :: QName primFunArity :: Arity primFunImplementation :: [Arg Term] -> TCM (Reduced MaybeReducedArgs Term)

Instances

Typeable PrimFun |
Abstract PrimFun |
Apply PrimFun |

defClauses :: Definition -> [Clause]

defCompiled :: Definition -> Maybe CompiledClauses

defJSDef :: Definition -> Maybe JSCode

defEpicDef :: Definition -> Maybe EpicCode

data Delayed

Used to specify whether something should be delayed.

Constructors

Delayed |
NotDelayed |

Instances

Eq Delayed |
Data Delayed |
Show Delayed |
Typeable Delayed |
EmbPrj Delayed |

defDelayed :: Definition -> Delayed

Are the clauses of this definition delayed?

defAbstract :: Definition -> IsAbstract

## Injectivity

data FunctionInverse

Constructors

NotInjective |
Inverse (Map TermHead Clause) |

Instances

Data FunctionInverse |
Show FunctionInverse |
Typeable FunctionInverse |
Abstract FunctionInverse |
Apply FunctionInverse |
EmbPrj FunctionInverse |
InstantiateFull FunctionInverse |

data TermHead

Constructors

SortHead |
PiHead |
ConHead QName |

Instances

Eq TermHead |
Data TermHead |
Ord TermHead |
Show TermHead |
Typeable TermHead |
EmbPrj TermHead |

## Mutual blocks

newtype MutualId

Constructors

MutId Int32 |

Instances

Eq MutualId |
Data MutualId |
Num MutualId |
Ord MutualId |
Show MutualId |
Typeable MutualId |
EmbPrj MutualId |
HasFresh MutualId FreshThings |

## Statistics

type Statistics = Map String Integer

## Trace

data Call

Constructors

CheckClause Type Clause (Maybe Clause) |
forall a . CheckPattern Pattern Telescope Type (Maybe a) |
CheckLetBinding LetBinding (Maybe ()) |
InferExpr Expr (Maybe (Term, Type)) |
CheckExpr Expr Type (Maybe Term) |
CheckDotPattern Expr Term (Maybe Constraints) |
CheckPatternShadowing Clause (Maybe ()) |
IsTypeCall Expr Sort (Maybe Type) |
IsType_ Expr (Maybe Type) |
InferVar Name (Maybe (Term, Type)) |
InferDef Range QName (Maybe (Term, Type)) |
CheckArguments Range [NamedArg Expr] Type Type (Maybe (Args, Type)) |
CheckDataDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckRecDef Range Name [LamBinding] [Constructor] (Maybe ()) |
CheckConstructor QName Telescope Sort Constructor (Maybe ()) |
CheckFunDef Range Name [Clause] (Maybe ()) |
CheckPragma Range Pragma (Maybe ()) |
CheckPrimitive Range Name Expr (Maybe ()) |
CheckIsEmpty Type (Maybe ()) |
CheckWithFunctionType Expr (Maybe ()) |
CheckSectionApplication Range ModuleName ModuleApplication (Maybe ()) |
ScopeCheckExpr Expr (Maybe Expr) |
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration]) |
ScopeCheckLHS Name Pattern (Maybe LHS) |
forall a . TermFunDef Range Name [Clause] (Maybe a) |
forall a . SetRange Range (Maybe a) | used by `setCurrentRange` actually, `a` is Agda.Termination.TermCheck.CallGraph but I was to lazy to import the stuff here --Andreas,2007-5-29

Instances

Data Call |
Typeable Call |
HasRange Call |
PrettyTCM Call |

## Builtin things

data BuiltinDescriptor

Constructors

BuiltinData (TCM Type) [String] |
BuiltinDataCons (TCM Type) |
BuiltinPrim String (Term -> TCM ()) |
BuiltinPostulate (TCM Type) |
BuiltinUnknown (Maybe (TCM Type)) (Term -> TCM ()) |

data BuiltinInfo

Constructors

BuiltinInfo |
Fields builtinName :: String builtinDesc :: BuiltinDescriptor

type BuiltinThings pf = Map String (Builtin pf)

data Builtin pf

Constructors

Builtin Term |
Prim pf |

Instances

Functor Builtin |
Typeable1 Builtin |
Foldable Builtin |
Traversable Builtin |
Data pf => Data (Builtin pf) |
Show pf => Show (Builtin pf) |
EmbPrj a => EmbPrj (Builtin a) |
InstantiateFull a => InstantiateFull (Builtin a) |

# Type checking environment

data TCEnv

Constructors

TCEnv |
Fields envContext :: Context envLetBindings :: LetBindings envCurrentModule :: ModuleName envAnonymousModules :: [(ModuleName, Nat)] anonymous modules and their number of free variables envImportPath :: [TopLevelModuleName] to detect import cycles envMutualBlock :: Maybe MutualId the current (if any) mutual block envSolvingConstraints :: Bool Are we currently in the process of solving active constraints? envActiveProblems :: [ProblemId] envAbstractMode :: AbstractMode When checking the typesignature of a public definition or the body of a non-abstract definition this is true. To prevent information about abstract things leaking outside the module. envTopLevel :: Bool Are we at the top level when checking a declaration? In this case, we will freeze metas afterwards. envRelevance :: Relevance Are we checking an irrelevant argument? (=`Irrelevant`) Then top-level irrelevant declarations are enabled. Other value: `Relevant`, then only relevant decls. are avail. envDisplayFormsEnabled :: Bool Sometimes we want to disable display forms. envReifyInteractionPoints :: Bool should we try to recover interaction points when reifying? disabled when generating types for with functions envEtaContractImplicit :: Bool it's safe to eta contract implicit lambdas as long as we're not going to reify and retypecheck (like when doing with abstraction) envRange :: Range envCall :: Maybe (Closure Call) what we're doing at the moment

Instances

Data TCEnv |
Typeable TCEnv |
MonadReader TCEnv RecPatM |
MonadReader TCEnv Unify |
MonadIO m => MonadReader TCEnv (TCMT m) |

initEnv :: TCEnv

## Context

type Context = [ContextEntry]

data ContextEntry

Constructors

Ctx |
Fields ctxId :: CtxId ctxEntry :: Arg (Name, Type)

Instances

Data ContextEntry |
Typeable ContextEntry |
PrettyTCM Context |

newtype CtxId

Constructors

CtxId Nat |

Instances

Enum CtxId |
Eq CtxId |
Integral CtxId |
Data CtxId |
Num CtxId |
Ord CtxId |
Real CtxId |
Show CtxId |
Typeable CtxId |
EmbPrj CtxId |
HasFresh CtxId FreshThings |

## Let bindings

type LetBindings = Map Name (Open (Term, Arg Type))

## Abstract mode

data AbstractMode

Constructors

AbstractMode | abstract things in the current module can be accessed
ConcreteMode | no abstract things can be accessed
IgnoreAbstractMode | all abstract things can be accessed

Instances

Data AbstractMode |
Typeable AbstractMode |

# Type checking errors

data Occ

Constructors

OccCon |
Fields occDatatype :: QName occConstructor :: QName occPosition :: OccPos
OccClause |
Fields occFunction :: QName occClause :: Int occPosition :: OccPos

Instances

Show Occ |

data OccPos

Constructors

NonPositively |
ArgumentTo Nat QName |

Instances

Show OccPos |

data CallInfo

Information about a call.

Constructors

CallInfo |
Fields callInfoRange :: Range Range of the head identifier. callInfoCall :: String Formatted representation of the call. (`Doc` would perhaps be better here, but `Doc` doesn't come with an `Ord` instance.)

Instances

Eq CallInfo |
Ord CallInfo |
Show CallInfo |
Typeable CallInfo |

data TerminationError

Information about a mutual block which did not pass the termination checker.

Constructors

TerminationError |
Fields termErrFunctions :: [QName] The functions which failed to check. (May not include automatically generated functions.) termErrCalls :: [CallInfo] The problematic call sites.

Instances

Show TerminationError |
Typeable TerminationError |

data TypeError

Constructors

InternalError String |
NotImplemented String |
NotSupported String |
CompilationError String |
TerminationCheckFailed [TerminationError] |
PropMustBeSingleton |
DataMustEndInSort Term |
ShouldEndInApplicationOfTheDatatype Type | The target of a constructor isn't an application of its datatype. The `Type` records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term Term | The target of a constructor isn't its datatype applied to something that isn't the parameters. First term is the correct target and the second term is the actual target.
ShouldBeApplicationOf Type QName | Expected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QName | constructor, datatype
IndicesNotConstructorApplications [Arg Term] | Indices.
IndexVariablesNotDistinct [Arg Term] | Indices.
IndexFreeInParameter Nat [Arg Term] | Index (a variable), parameters.
DoesNotConstructAnElementOf QName Term | constructor, type
DifferentArities | Varying number of arguments for a function.
WrongHidingInLHS Type | The left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda Type | Expected a non-hidden function and found a hidden lambda.
WrongHidingInApplication Type | A function is applied to a hidden argument where a non-hidden was expected.
WrongIrrelevanceInLambda Type | Expected a relevant function and found an irrelevant lambda.
NotInductive Term | The term does not correspond to an inductive data type.
UninstantiatedDotPattern Expr |
IlltypedPattern Pattern Type |
TooManyArgumentsInLHS Nat Type |
WrongNumberOfConstructorArguments QName Nat Nat |
ShouldBeEmpty Type [Pattern] |
ShouldBeASort Type | The given type should have been a sort.
ShouldBePi Type | The given type should have been a pi.
ShouldBeRecordType Type |
NotAProperTerm |
SplitOnIrrelevant Pattern (Arg Type) |
DefinitionIsIrrelevant QName |
VariableIsIrrelevant Name |
UnequalLevel Comparison Term Term |
UnequalTerms Comparison Term Term Type |
UnequalTypes Comparison Type Type |
UnequalTelescopes Comparison Telescope Telescope |
UnequalRelevance Type Type | The two function types have different relevance.
UnequalHiding Type Type | The two function types have different hiding.
UnequalSorts Sort Sort |
HeterogeneousEquality Term Type Term Type | We ended up with an equality constraint where the terms have different types. This is not supported.
NotLeqSort Sort Sort |
MetaCannotDependOn MetaId [Nat] Nat | The arguments are the meta variable, the parameters it can depend on and the paratemeter that it wants to depend on.
MetaOccursInItself MetaId |
GenericError String |
BuiltinMustBeConstructor String Expr |
NoSuchBuiltinName String |
DuplicateBuiltinBinding String Term Term |
NoBindingForBuiltin String |
NoSuchPrimitiveFunction String |
ShadowedModule [ModuleName] |
BuiltinInParameterisedModule String |
NoRHSRequiresAbsurdPattern [NamedArg Pattern] |
AbsurdPatternRequiresNoRHS [NamedArg Pattern] |
TooFewFields QName [Name] |
TooManyFields QName [Name] |
DuplicateFields [Name] |
DuplicateConstructors [Name] |
UnexpectedWithPatterns [Pattern] |
WithClausePatternMismatch Pattern Pattern |
FieldOutsideRecord |
ModuleArityMismatch ModuleName Telescope [NamedArg Expr] |
IncompletePatternMatching Term Args |
CoverageFailure QName [[Arg Pattern]] |
UnreachableClauses QName [[Arg Pattern]] |
CoverageCantSplitOn QName Telescope Args Args |
CoverageCantSplitIrrelevantType Type |
CoverageCantSplitType Type |
NotStrictlyPositive QName [Occ] |
LocalVsImportedModuleClash ModuleName |
UnsolvedMetas [Range] |
UnsolvedConstraints Constraints |
CyclicModuleDependency [TopLevelModuleName] |
FileNotFound TopLevelModuleName [AbsolutePath] |
OverlappingProjects AbsolutePath TopLevelModuleName TopLevelModuleName |
AmbiguousTopLevelModuleName TopLevelModuleName [AbsolutePath] |
ModuleNameDoesntMatchFileName TopLevelModuleName [AbsolutePath] |
ClashingFileNamesFor ModuleName [AbsolutePath] |
ModuleDefinedInOtherFile TopLevelModuleName AbsolutePath AbsolutePath | Module name, file from which it was loaded, file which the include path says contains the module. Scope errors
BothWithAndRHS |
NotInScope [QName] |
NoSuchModule QName |
AmbiguousName QName [QName] |
AmbiguousModule QName [ModuleName] |
UninstantiatedModule QName |
ClashingDefinition QName QName |
ClashingModule ModuleName ModuleName |
ClashingImport Name QName |
ClashingModuleImport Name ModuleName |
PatternShadowsConstructor Name QName |
ModuleDoesntExport QName [ImportedName] |
DuplicateImports QName [ImportedName] |
InvalidPattern Pattern |
RepeatedVariablesInPattern [Name] |
NotAModuleExpr Expr | The expr was used in the right hand side of an implicit module definition, but it wasn't of the form `m Delta`.
NotAnExpression Expr |
NotAValidLetBinding NiceDeclaration |
NothingAppliedToHiddenArg Expr |
NothingAppliedToInstanceArg Expr |
NoParseForApplication [Expr] |
AmbiguousParseForApplication [Expr] [Expr] |
NoParseForLHS Pattern |
AmbiguousParseForLHS Pattern [Pattern] |
IFSNoCandidateInScope Type |
SafeFlagPostulate Name |
SafeFlagPragma [String] |
SafeFlagPrimTrustMe |

Instances

Show TypeError |
Typeable TypeError |
Error TypeError |
PrettyTCM TypeError |

data TCErr'

Type-checking errors.

Constructors

TypeError TCState (Closure TypeError) |
Exception Range String |
IOException Range IOException |
PatternErr TCState | for pattern violations

Instances

Show TCErr' |
Typeable TCErr' |
HasRange TCErr' |

data TCErr

Type-checking errors, potentially paired with relevant syntax highlighting information.

Constructors

TCErr |
Fields errHighlighting :: Maybe (HighlightingInfo, ModuleToSource) The `ModuleToSource` can be used to map the module names in the `HighlightingInfo` to file names. errError :: TCErr'

Instances

Show TCErr |
Typeable TCErr |
Exception TCErr |
Error TCErr |
HasRange TCErr |
PrettyTCM TCErr |
MonadError TCErr IM |
MonadError TCErr (TCMT IO) |

# Type checking monad transformer

newtype TCMT m a

Constructors

TCM |
Fields unTCM :: IORef TCState -> TCEnv -> m a

Instances

MonadTrans TCMT |
MonadError TCErr IM |
MonadError TCErr (TCMT IO) |
MonadIO m => MonadReader TCEnv (TCMT m) |
MonadIO m => MonadState TCState (TCMT m) |
MonadIO m => Monad (TCMT m) |
MonadIO m => Functor (TCMT m) |
MonadIO m => Applicative (TCMT m) |
MonadIO m => MonadIO (TCMT m) |
MonadIO m => MonadTCM (TCMT m) |

type TCM = TCMT IO

class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm where

Methods

liftTCM :: TCM a -> tcm a

Instances

MonadTCM RecPatM |
MonadTCM Unify |
MonadIO m => MonadTCM (TCMT m) |
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm) |
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm) |

catchError_ :: TCM a -> (TCErr -> TCM a) -> TCM a

Preserve the state of the failing computation.

mapTCMT :: (forall a. m a -> n a) -> TCMT m a -> TCMT n a

pureTCM :: MonadIO m => (TCState -> TCEnv -> a) -> TCMT m a

patternViolation :: TCM a

internalError :: MonadTCM tcm => String -> tcm a

typeError :: MonadTCM tcm => TypeError -> tcm a

runTCM :: TCMT IO a -> IO (Either TCErr a)

Running the type checking monad

runTCM' :: MonadIO m => TCMT m a -> m a

extendlambdaname :: [Char]

Base name for extended lambda patterns