Agda.TypeChecking.Errors

Documentation

prettyError :: MonadTCM tcm => TCErr -> tcm String

class PrettyTCM a where

Methods

prettyTCM :: a -> TCM Doc

Instances

PrettyTCM Bool

PrettyTCM Range

PrettyTCM Interval

PrettyTCM Position

PrettyTCM Nat

PrettyTCM Relevance

PrettyTCM Name

PrettyTCM Permutation

PrettyTCM ModuleName

PrettyTCM QName

PrettyTCM Name

PrettyTCM Literal

PrettyTCM Expr

PrettyTCM Pattern

PrettyTCM ClauseBody

PrettyTCM MetaId

PrettyTCM Level

PrettyTCM Sort

PrettyTCM Telescope

PrettyTCM Type

PrettyTCM Elim

PrettyTCM Term

PrettyTCM ConHead

PrettyTCM TCErr

PrettyTCM TypeError

PrettyTCM SplitError

PrettyTCM CallInfo

PrettyTCM Context

PrettyTCM Call

PrettyTCM Occurrence

PrettyTCM RewriteRule

PrettyTCM DisplayTerm

PrettyTCM TypeCheckingProblem

PrettyTCM Comparison

PrettyTCM Constraint

PrettyTCM ProblemConstraint

PrettyTCM NamedClause

PrettyTCM PrettyContext

PrettyTCM AsBinding

PrettyTCM DotPatternInst

PrettyTCM DeBruijnPat

PrettyTCM Node

PrettyTCM OccursWhere

PrettyTCM HypSizeConstraint

PrettyTCM SizeConstraint

Assumes we are in the right context.

PrettyTCM SizeMeta

PrettyTCM SplitClause

For debugging only.

PrettyTCM a => PrettyTCM [a]

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Named_ a)

PrettyTCM a => PrettyTCM (Blocked a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Dom a)

(Reify a e, ToConcrete e c, Pretty c) => PrettyTCM (Arg a)

PrettyTCM a => PrettyTCM (MaybeReduced a)

PrettyTCM a => PrettyTCM (Closure a)

PrettyTCM a => PrettyTCM (HomHet a)

(PrettyTCM a, PrettyTCM b) => PrettyTCM (a, b)

(PrettyTCM n, PrettyTCM (WithNode n e)) => PrettyTCM (Graph n e)

(PrettyTCM a, PrettyTCM b) => PrettyTCM (Judgement a b)

PrettyTCM n => PrettyTCM (WithNode n Occurrence)

PrettyTCM n => PrettyTCM (WithNode n Edge)

tcErrString :: TCErr -> String

data Warnings

Warnings.

Invariant: The fields are never empty at the same time.

Constructors

Warnings

Fields

unsolvedMetaVariables :: [Range]

Meta-variable problems are reported as type errors unless optAllowUnsolved is True.

unsolvedConstraints :: Constraints

Same as unsolvedMetaVariables.

warningsToError :: Warnings -> TCM a

Turns warnings into an error. Even if several errors are possible only one is raised.