Agda-2.2.4: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe (ModuleName, Interface)
stScope :: ScopeInfo
stOptions :: CommandLineOptions
stStatistics :: Statistics
stTrace :: CallTrace
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: [String]
}
data FreshThings = Fresh {
fMeta :: MetaId
fInteraction :: InteractionId
fMutual :: MutualId
fName :: NameId
fCtx :: CtxId
fInteger :: Integer
}
initState :: TCState
stBuiltinThings :: TCState -> BuiltinThings PrimFun
type VisitedModules = Map ModuleName (Interface, ClockTime)
type DecodedModules = Map ModuleName (Interface, ClockTime)
data Interface = Interface {
iImportedModules :: [ModuleName]
iModuleName :: ModuleName
iScope :: Map ModuleName Scope
iSignature :: Signature
iBuiltin :: BuiltinThings String
iHaskellImports :: [String]
iHighlighting :: HighlightingInfo
}
data Closure a = Closure {
clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
clTrace :: CallTrace
clValue :: a
}
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)
type ConstraintClosure = Closure Constraint
data Constraint
= ValueCmp Comparison Type Term Term
| TypeCmp Comparison Type Type
| TelCmp Comparison Telescope Telescope
| SortCmp Comparison Sort Sort
| UnBlock MetaId
| Guarded Constraint Constraints
| IsEmpty Type
data Comparison
= CmpEq
| CmpLeq
type Constraints = [ConstraintClosure]
data Open a = OpenThing [CtxId] a
data Judgement t a
= HasType a t
| IsSort a
data MetaVariable = MetaVar {
mvInfo :: MetaInfo
mvPriority :: MetaPriority
mvJudgement :: Judgement Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaId
}
data MetaInstantiation
= InstV Term
| InstS Sort
| Open
| 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
| DTerm Term
defaultDisplayForm :: QName -> [Open DisplayForm]
data Definition = Defn {
defName :: QName
defType :: Type
defDisplay :: [Open DisplayForm]
defMutual :: MutualId
theDef :: Defn
}
type HaskellCode = String
type HaskellType = String
data HaskellRepresentation
= HsDefn HaskellType HaskellCode
| HsType HaskellType
data Polarity
= Covariant
| Contravariant
| Invariant
data Occurrence
= Positive
| Negative
| Unused
data Defn
= Axiom {
axHsDef :: Maybe HaskellRepresentation
}
| Function {
funClauses :: [Clause]
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: Delayed
}
| Datatype {
dataPars :: Nat
dataIxs :: Nat
dataInduction :: Induction
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataPolarity :: [Polarity]
dataArgOccurrences :: [Occurrence]
dataHsType :: Maybe HaskellType
dataAbstr :: IsAbstract
}
| Record {
recPars :: Nat
recClause :: Maybe Clause
recFields :: [QName]
recTel :: Telescope
recSort :: Sort
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recAbstr :: IsAbstract
}
| Constructor {
conPars :: Nat
conSrcCon :: QName
conData :: QName
conHsCode :: Maybe (HaskellType, HaskellCode)
conAbstr :: IsAbstract
conInd :: Induction
}
| Primitive {
primAbstr :: IsAbstract
primName :: String
primClauses :: [Clause]
}
newtype Fields = Fields [(Name, Type)]
data Reduced no yes
= NoReduction no
| YesReduction yes
data PrimFun = PrimFun {
primFunName :: QName
primFunArity :: Arity
primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term)
}
defClauses :: Definition -> [Clause]
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 Int
type Statistics = Map String Int
type CallTrace = Trace (Closure Call)
noTrace :: CallTrace
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 ())
| 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, Constraints))
| 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 ())
| CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
| ScopeCheckExpr Expr (Maybe Expr)
| ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
| ScopeCheckLHS Name Pattern (Maybe LHS)
| ScopeCheckDefinition NiceDefinition (Maybe Definition)
| forall a . TermFunDef Range Name [Clause] (Maybe a)
| forall a . SetRange Range (Maybe a)
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 :: [ModuleName]
envMutualBlock :: Maybe MutualId
envAbstractMode :: AbstractMode
envReplace :: Bool
envDisplayFormsEnabled :: Bool
envReifyInteractionPoints :: Bool
}
initEnv :: TCEnv
type Context = [ContextEntry]
data ContextEntry = Ctx {
ctxId :: CtxId
ctxEntry :: Arg (Name, Type)
}
newtype CtxId = CtxId Nat
type LetBindings = Map Name (Open (Term, 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 TypeError
= InternalError String
| NotImplemented String
| NotSupported String
| CompilationError String
| TerminationCheckFailed [([QName], [Range])]
| PropMustBeSingleton
| DataMustEndInSort Term
| ShouldEndInApplicationOfTheDatatype Type
| ShouldBeAppliedToTheDatatypeParameters Term Term
| ShouldBeApplicationOf Type QName
| ConstructorPatternInWrongDatatype QName QName
| DoesNotConstructAnElementOf QName Term
| DifferentArities
| WrongHidingInLHS Type
| WrongHidingInLambda Type
| WrongHidingInApplication Type
| DependentPatternMatchingOnCodata
| NotInductive Term
| UninstantiatedDotPattern Expr
| IlltypedPattern Pattern Type
| TooManyArgumentsInLHS Nat Type
| WrongNumberOfConstructorArguments QName Nat Nat
| ShouldBeEmpty Type [Pattern]
| ShouldBeASort Type
| ShouldBePi Type
| ShouldBeRecordType Type
| NotAProperTerm
| UnequalTerms Comparison Term Term Type
| UnequalTypes Comparison Type Type
| UnequalTelescopes Comparison Telescope Telescope
| UnequalHiding Type Type
| UnequalSorts Sort Sort
| 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
| CoverageCantSplitType Type
| NotStrictlyPositive QName [Occ]
| LocalVsImportedModuleClash ModuleName
| UnsolvedMetas [Range]
| UnsolvedConstraints Constraints
| CyclicModuleDependency [ModuleName]
| FileNotFound ModuleName [FilePath]
| ClashingFileNamesFor ModuleName [FilePath]
| ModuleNameDoesntMatchFileName ModuleName
| 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]
| InvalidPattern Pattern
| RepeatedVariablesInPattern [Name]
| NotAModuleExpr Expr
| NotAnExpression Expr
| NotAValidLetBinding NiceDeclaration
| NothingAppliedToHiddenArg Expr
| NoParseForApplication [Expr]
| AmbiguousParseForApplication [Expr] [Expr]
| NoParseForLHS Pattern
| AmbiguousParseForLHS Pattern [Pattern]
data TCErr
= TypeError TCState (Closure TypeError)
| Exception Range String
| PatternErr TCState
| AbortAssign TCState
newtype TCMT m a = TCM {
unTCM :: UndoT TCState (StateT TCState (ReaderT TCEnv (ErrorT TCErr 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
mapTCMT :: (m (Either TCErr ((a, [TCState]), TCState)) -> n (Either TCErr ((b, [TCState]), TCState))) -> TCMT m a -> TCMT n b
patternViolation :: MonadTCM tcm => tcm a
internalError :: MonadTCM tcm => String -> tcm a
typeError :: MonadTCM tcm => TypeError -> tcm a
handleTypeErrorException :: MonadTCM tcm => IO a -> tcm a
runTCM :: Monad m => TCMT m a -> m (Either TCErr a)
Type checking state
data TCState Source
Constructors
TCSt
stFreshThings :: FreshThings
stMetaStore :: MetaStore
stInteractionPoints :: InteractionPoints
stConstraints :: Constraints
stSignature :: Signature
stImports :: Signature
stImportedModules :: Set ModuleName
stVisitedModules :: VisitedModules
stDecodedModules :: DecodedModules
stCurrentModule :: Maybe (ModuleName, Interface)The current module is available after it has been type checked.
stScope :: ScopeInfo
stOptions :: CommandLineOptions
stStatistics :: Statistics
stTrace :: CallTracerecord what is happening (for error msgs)
stMutualBlocks :: Map MutualId (Set QName)
stLocalBuiltins :: BuiltinThings PrimFun
stImportedBuiltins :: BuiltinThings PrimFun
stHaskellImports :: [String]imports that should be generated by the compiler
show/hide Instances
data FreshThings Source
Constructors
Fresh
fMeta :: MetaId
fInteraction :: InteractionId
fMutual :: MutualId
fName :: NameId
fCtx :: CtxId
fInteger :: IntegerCan be used for various things.
show/hide Instances
initState :: TCStateSource
stBuiltinThings :: TCState -> BuiltinThings PrimFunSource
Interface
type VisitedModules = Map ModuleName (Interface, ClockTime)Source
type DecodedModules = Map ModuleName (Interface, ClockTime)Source
data Interface Source
Constructors
Interface
iImportedModules :: [ModuleName]
iModuleName :: ModuleName
iScope :: Map ModuleName Scope
iSignature :: Signature
iBuiltin :: BuiltinThings String
iHaskellImports :: [String]
iHighlighting :: HighlightingInfo
show/hide Instances
Closure
data Closure a Source
Constructors
Closure
clSignature :: Signature
clEnv :: TCEnv
clScope :: ScopeInfo
clTrace :: CallTrace
clValue :: a
show/hide Instances
buildClosure :: MonadTCM tcm => a -> tcm (Closure a)Source
Constraints
type ConstraintClosure = Closure ConstraintSource
data Constraint Source
Constructors
ValueCmp Comparison Type Term Term
TypeCmp Comparison Type Type
TelCmp Comparison Telescope Telescope
SortCmp Comparison Sort Sort
UnBlock MetaId
Guarded Constraint Constraints
IsEmpty Type
show/hide Instances
data Comparison Source
Constructors
CmpEq
CmpLeq
show/hide Instances
type Constraints = [ConstraintClosure]Source
Open things
data Open a Source
A thing tagged with the context it came from.
Constructors
OpenThing [CtxId] a
show/hide Instances
Judgements
data Judgement t a Source
Constructors
HasType a t
IsSort a
show/hide Instances
Meta variables
data MetaVariable Source
Constructors
MetaVar
mvInfo :: MetaInfo
mvPriority :: MetaPrioritysome metavariables are more eager to be instantiated
mvJudgement :: Judgement Type MetaId
mvInstantiation :: MetaInstantiation
mvListeners :: Set MetaIdmetavariables interested in what happens to this guy
show/hide Instances
data MetaInstantiation Source
Constructors
InstV Term
InstS Sort
Open
BlockedConst Term
PostponedTypeCheckingProblem (Closure (Expr, Type, TCM Bool))
show/hide Instances
newtype MetaPriority Source
Constructors
MetaPriority Int
show/hide Instances
type MetaInfo = Closure RangeSource
TODO: Not so nice.
type MetaStore = Map MetaId MetaVariableSource
normalMetaPriority :: MetaPrioritySource
lowMetaPriority :: MetaPrioritySource
highMetaPriority :: MetaPrioritySource
getMetaInfo :: MetaVariable -> MetaInfoSource
getMetaScope :: MetaVariable -> ScopeInfoSource
getMetaEnv :: MetaVariable -> TCEnvSource
getMetaSig :: MetaVariable -> SignatureSource
Interaction meta variables
type InteractionPoints = Map InteractionId MetaIdSource
newtype InteractionId Source
Constructors
InteractionId Nat
show/hide Instances
Signature
data Signature Source
Constructors
Sig
sigSections :: Sections
sigDefinitions :: Definitions
show/hide Instances
type Sections = Map ModuleName SectionSource
type Definitions = Map QName DefinitionSource
data Section Source
Constructors
Section
secTelescope :: Telescope
secFreeVars :: NatThis 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.
show/hide Instances
emptySignature :: SignatureSource
data DisplayForm Source
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.
show/hide Instances
data DisplayTerm Source
Constructors
DWithApp [DisplayTerm] Args
DTerm Term
show/hide Instances
defaultDisplayForm :: QName -> [Open DisplayForm]Source
data Definition Source
Constructors
Defn
defName :: QName
defType :: Type
defDisplay :: [Open DisplayForm]
defMutual :: MutualId
theDef :: Defn
show/hide Instances
type HaskellCode = StringSource
type HaskellType = StringSource
data HaskellRepresentation Source
Constructors
HsDefn HaskellType HaskellCode
HsType HaskellType
show/hide Instances
data Polarity Source
Constructors
Covariant
Contravariant
Invariant
show/hide Instances
data Occurrence Source
Positive means strictly positive and Negative means not strictly positive.
Constructors
Positive
Negative
Unused
show/hide Instances
data Defn Source
Constructors
Axiom
axHsDef :: Maybe HaskellRepresentation
Function
funClauses :: [Clause]
funInv :: FunctionInverse
funPolarity :: [Polarity]
funArgOccurrences :: [Occurrence]
funAbstr :: IsAbstract
funDelayed :: DelayedAre the clauses of this definition delayed?
Datatype
dataPars :: Nat
dataIxs :: Nat
dataInduction :: Induction
dataClause :: Maybe Clause
dataCons :: [QName]
dataSort :: Sort
dataPolarity :: [Polarity]
dataArgOccurrences :: [Occurrence]
dataHsType :: Maybe HaskellType
dataAbstr :: IsAbstract
Record
recPars :: Nat
recClause :: Maybe Clause
recFields :: [QName]
recTel :: Telescope
recSort :: Sort
recPolarity :: [Polarity]
recArgOccurrences :: [Occurrence]
recAbstr :: IsAbstract
Constructor
conPars :: Nat
conSrcCon :: QName
conData :: QName
conHsCode :: Maybe (HaskellType, HaskellCode)
conAbstr :: IsAbstract
conInd :: InductionInductive or coinductive?
Primitive
primAbstr :: IsAbstract
primName :: String
primClauses :: [Clause]
show/hide Instances
newtype Fields Source
Constructors
Fields [(Name, Type)]
show/hide Instances
data Reduced no yes Source
Constructors
NoReduction no
YesReduction yes
show/hide Instances
data PrimFun Source
Constructors
PrimFun
primFunName :: QName
primFunArity :: Arity
primFunImplementation :: MonadTCM tcm => [Arg Term] -> tcm (Reduced [Arg Term] Term)
show/hide Instances
defClauses :: Definition -> [Clause]Source
data Delayed Source
Used to specify whether something should be delayed.
Constructors
Delayed
NotDelayed
show/hide Instances
defDelayed :: Definition -> DelayedSource
Are the clauses of this definition delayed?
defAbstract :: Definition -> IsAbstractSource
Injectivity
data FunctionInverse Source
Constructors
NotInjective
Inverse (Map TermHead Clause)
show/hide Instances
data TermHead Source
Constructors
SortHead
PiHead
ConHead QName
show/hide Instances
Mutual blocks
newtype MutualId Source
Constructors
MutId Int
show/hide Instances
Statistics
type Statistics = Map String IntSource
Trace
type CallTrace = Trace (Closure Call)Source
noTrace :: CallTraceSource
data Call Source
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 ())
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, Constraints))
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 ())
CheckSectionApplication Range ModuleName Telescope ModuleName [NamedArg Expr] (Maybe ())
ScopeCheckExpr Expr (Maybe Expr)
ScopeCheckDeclaration NiceDeclaration (Maybe [Declaration])
ScopeCheckLHS Name Pattern (Maybe LHS)
ScopeCheckDefinition NiceDefinition (Maybe Definition)
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
show/hide Instances
Builtin things
type BuiltinThings pf = Map String (Builtin pf)Source
data Builtin pf Source
Constructors
Builtin Term
Prim pf
show/hide Instances
Type checking environment
data TCEnv Source
Constructors
TCEnv
envContext :: Context
envLetBindings :: LetBindings
envCurrentModule :: ModuleName
envAnonymousModules :: [(ModuleName, Nat)]anonymous modules and their number of free variables
envImportPath :: [ModuleName]to detect import cycles
envMutualBlock :: Maybe MutualIdthe current (if any) mutual block
envAbstractMode :: AbstractModeWhen 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.
envReplace :: BoolCoinductive constructor applications c args get replaced by a function application f tel, where tel corresponds to the current telescope and f is defined as f tel = c args. The initial occurrence of c in the body of f should not be replaced by yet another function application, though. To avoid that this happens the envReplace flag is set to False when f is checked.
envDisplayFormsEnabled :: BoolSometimes we want to disable display forms.
envReifyInteractionPoints :: Boolshould we try to recover interaction points when reifying? disabled when generating types for with functions
show/hide Instances
initEnv :: TCEnvSource
Context
type Context = [ContextEntry]Source
data ContextEntry Source
Constructors
Ctx
ctxId :: CtxId
ctxEntry :: Arg (Name, Type)
show/hide Instances
newtype CtxId Source
Constructors
CtxId Nat
show/hide Instances
Let bindings
type LetBindings = Map Name (Open (Term, Type))Source
Abstract mode
data AbstractMode Source
Constructors
AbstractModeabstract things in the current module can be accessed
ConcreteModeno abstract things can be accessed
IgnoreAbstractModeall abstract things can be accessed
show/hide Instances
Type checking errors
data Occ Source
Constructors
OccCon
occDatatype :: QName
occConstructor :: QName
occPosition :: OccPos
OccClause
occFunction :: QName
occClause :: Int
occPosition :: OccPos
data OccPos Source
Constructors
NonPositively
ArgumentTo Nat QName
data TypeError Source
Constructors
InternalError String
NotImplemented String
NotSupported String
CompilationError String
TerminationCheckFailed [([QName], [Range])]Parameterised on functions which failed to termination check (grouped if they are mutual), along with ranges for problematic call sites.
PropMustBeSingleton
DataMustEndInSort Term
ShouldEndInApplicationOfTheDatatype TypeThe target of a constructor isn't an application of its datatype. The Type records what it does target.
ShouldBeAppliedToTheDatatypeParameters Term TermThe 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 QNameExpected a type to be an application of a particular datatype.
ConstructorPatternInWrongDatatype QName QNameconstructor, datatype
DoesNotConstructAnElementOf QName Termconstructor, type
DifferentAritiesVarying number of arguments for a function.
WrongHidingInLHS TypeThe left hand side of a function definition has a hidden argument where a non-hidden was expected.
WrongHidingInLambda TypeExpected a non-hidden function and found a hidden lambda.
WrongHidingInApplication TypeA function is applied to a hidden argument where a non-hidden was expected.
DependentPatternMatchingOnCodata
NotInductive TermThe 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 TypeThe given type should have been a sort.
ShouldBePi TypeThe given type should have been a pi.
ShouldBeRecordType Type
NotAProperTerm
UnequalTerms Comparison Term Term Type
UnequalTypes Comparison Type Type
UnequalTelescopes Comparison Telescope Telescope
UnequalHiding Type TypeThe two function types have different hiding.
UnequalSorts Sort Sort
NotLeqSort Sort Sort
MetaCannotDependOn MetaId [Nat] NatThe 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
CoverageCantSplitType Type
NotStrictlyPositive QName [Occ]
LocalVsImportedModuleClash ModuleName
UnsolvedMetas [Range]
UnsolvedConstraints Constraints
CyclicModuleDependency [ModuleName]
FileNotFound ModuleName [FilePath]
ClashingFileNamesFor ModuleName [FilePath]
ModuleNameDoesntMatchFileName ModuleName
NoMatch given
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]
InvalidPattern Pattern
RepeatedVariablesInPattern [Name]
NotAModuleExpr ExprThe 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
NoParseForApplication [Expr]
AmbiguousParseForApplication [Expr] [Expr]
NoParseForLHS Pattern
AmbiguousParseForLHS Pattern [Pattern]
show/hide Instances
data TCErr Source
Constructors
TypeError TCState (Closure TypeError)
Exception Range String
PatternErr TCStatefor pattern violations
AbortAssign TCStateused to abort assignment to meta when there are instantiations
show/hide Instances
Type checking monad transformer
newtype TCMT m a Source
Constructors
TCM
unTCM :: UndoT TCState (StateT TCState (ReaderT TCEnv (ErrorT TCErr m))) a
show/hide Instances
type TCM = TCMT IOSource
class (Applicative tcm, MonadIO tcm, MonadReader TCEnv tcm, MonadState TCState tcm) => MonadTCM tcm whereSource
Methods
liftTCM :: TCM a -> tcm aSource
show/hide Instances
MonadTCM Unify
MonadIO m => MonadTCM (TCMT m)
(Error err, MonadTCM tcm) => MonadTCM (ErrorT err tcm)
(Error err, MonadTCM tcm) => MonadTCM (ExceptionT err tcm)
mapTCMT :: (m (Either TCErr ((a, [TCState]), TCState)) -> n (Either TCErr ((b, [TCState]), TCState))) -> TCMT m a -> TCMT n bSource
patternViolation :: MonadTCM tcm => tcm aSource
internalError :: MonadTCM tcm => String -> tcm aSource
typeError :: MonadTCM tcm => TypeError -> tcm aSource
handleTypeErrorException :: MonadTCM tcm => IO a -> tcm aSource
runTCM :: Monad m => TCMT m a -> m (Either TCErr a)Source
Running the type checking monad
Produced by Haddock version 2.4.2