| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Rzk.TypeCheck.Error
Contents
Description
Type errors, and how they are shown.
An error is captured at its own scope: it packages the context it was raised
in, existentially, so its scope index does not escape into the error type. The
old representation instead nested the error one Inc deeper at every binder
(ScopedTypeError) and unwound the whole stack at printing time, inventing a
name per binder as it went. That unwinding loop, and both of its
FIXME: very inefficient filter sites, are gone: the context already knows what
everything in scope is called (see Rzk.TypeCheck.Display).
The error type is therefore not scope-indexed, which is why entering a binder no longer has to re-index the error channel.
Synopsis
- data TypeError (n :: S)
- = TypeErrorOther String
- | TypeErrorUnify (TermT n) (TermT n) (TermT n)
- | TypeErrorUnifyTerms (TermT n) (TermT n)
- | TypeErrorNotPair (TermT n) (TermT n)
- | TypeErrorNotModal (Term n) TModality (TermT n)
- | TypeErrorModalityMismatch TModality TModality (Term n)
- | TypeErrorUnaccessibleVar (Name n) TModality TModality
- | TypeErrorNotTypeInModal (TermT n)
- | TypeErrorNotFunction (TermT n) (TermT n)
- | TypeErrorUnexpectedLambda (Term n) (TermT n)
- | TypeErrorUnexpectedPair (Term n) (TermT n)
- | TypeErrorUnexpectedRefl (Term n) (TermT n)
- | TypeErrorCannotInferBareLambda (Term n)
- | TypeErrorCannotInferBareRefl (Term n)
- | TypeErrorCannotInferHole (Term n)
- | TypeErrorUnsolvedHole (Maybe VarIdent) (TermT n)
- | TypeErrorUndefined VarIdent
- | TypeErrorTopeNotSatisfied [TermT n] (TermT n)
- | TypeErrorTopeContextDisjoint (TermT n) [TermT n]
- | TypeErrorTopesNotEquivalent (TermT n) (TermT n)
- | TypeErrorInvalidArgumentType (Term n) (TermT n)
- | TypeErrorDuplicateTopLevel [VarIdent] VarIdent
- | TypeErrorUnusedVariable (Name n) (TermT n)
- | TypeErrorUnusedUsedVariables [Name n] (Name n)
- | TypeErrorImplicitAssumption (Name n, TermT n) (Name n)
- | TypeErrorNotIntervalCube String (TermT n) (TermT n)
- | TypeErrorRepeatedBinder VarIdent [VarIdent]
- | TypeErrorMatchScrutineeNotData (TermT n) (TermT n)
- | TypeErrorMatchCannotInfer (Term n)
- | TypeErrorMatchMissingBranch VarIdent
- | TypeErrorMatchDuplicateBranch VarIdent
- | TypeErrorMatchUnknownBranch VarIdent [VarIdent]
- | TypeErrorMatchBranchArity VarIdent Int Int
- | TypeErrorReascribedTypeMismatch VarIdent (TermT n) (TermT n)
- data TypeErrorInScopedContext where
- TypeErrorInScopedContext :: forall (n :: S). Distinct n => Context n -> TypeError n -> TypeErrorInScopedContext
- ppModality :: TModality -> String
- data OutputDirection
- block :: OutputDirection -> [String] -> String
- namedBlock :: OutputDirection -> String -> [String] -> String
- ppTypeError :: forall (n :: S). Naming n -> TypeError n -> String
- ppAction :: forall (n :: S). Naming n -> Int -> Action n -> String
- ppContext :: forall (n :: S). OutputDirection -> Context n -> String
- ppTypeErrorInScopedContext :: OutputDirection -> TypeErrorInScopedContext -> String
Documentation
data TypeError (n :: S) Source #
Constructors
data TypeErrorInScopedContext where Source #
An error, together with the context it was raised in.
The scope index is existential: an error raised under a binder is already complete (its context says what its names are called), so it needs nothing from the enclosing scope and can be thrown straight through it.
Constructors
| TypeErrorInScopedContext :: forall (n :: S). Distinct n => Context n -> TypeError n -> TypeErrorInScopedContext |
ppModality :: TModality -> String Source #
Rendering
data OutputDirection Source #
Instances
| Eq OutputDirection Source # | |
Defined in Rzk.TypeCheck.Error Methods (==) :: OutputDirection -> OutputDirection -> Bool # (/=) :: OutputDirection -> OutputDirection -> Bool # | |
namedBlock :: OutputDirection -> String -> [String] -> String Source #
ppContext :: forall (n :: S). OutputDirection -> Context n -> String Source #
The context an error was raised in: where it happened, what was being checked, the tope context, the stack of judgements, and the hypotheses.
ppTypeErrorInScopedContext :: OutputDirection -> TypeErrorInScopedContext -> String Source #
An error, with the context it was raised in.