Language.Reflection.Errors

ErrorHandler : Type

data Err : Type

Msg : String -> Err

InternalMsg : String -> Err

CantUnify : Bool -> TT -> TT -> Err -> List (TTName, TT) -> Int -> Err

InfiniteUnify : TTName -> TT -> List (TTName, TT) -> Err

CantConvert : TT -> TT -> List (TTName, TT) -> Err

CantSolveGoal : TT -> List (TTName, TT) -> Err

UnifyScope : TTName -> TTName -> TT -> List (TTName, TT) -> Err

CantInferType : String -> Err

NonFunctionType : TT -> TT -> Err

NotEquality : TT -> TT -> Err

TooManyArguments : TTName -> Err

CantIntroduce : TT -> Err

NoSuchVariable : TTName -> Err

WithFnType : TT -> Err

CantMatch : TT -> Err

NoTypeDecl : TTName -> Err

NotInjective : TT -> TT -> TT -> Err

CantResolve : TT -> Err -> Err

InvalidTCArg : TTName -> TT -> Err

CantResolveAlts : List TTName -> Err

NoValidAlts : List TTName -> Err

IncompleteTerm : TT -> Err

NoEliminator : String -> TT -> Err

UniverseError : Err

ProgramLineComment : Err

Inaccessible : TTName -> Err

UnknownImplicit : TTName -> TTName -> Err

NonCollapsiblePostulate : TTName -> Err

AlreadyDefined : TTName -> Err

ProofSearchFail : Err -> Err

NoRewriting : TT -> TT -> TT -> Err

ProviderError : String -> Err

LoadingFailed : String -> Err -> Err