Enum minitt::check::tcm::TCE

pub enum TCE {
    Textual(String),
    UpdateGammaFailed(Pattern),
    CannotInfer(Expression),
    UnresolvedName(String),
    InvalidConstructor(String),
    MissingCase(String),
    UnexpectedCases(String),
    Unreachable(&'static str, u32, u32),
    WantSumBut(Either<Value, Expression>),
    DuplicateBranch(String),
    WantSigmaBut(Value),
    WantPiBut(Value, Expression),
    TypeMismatch(Value, Value),
    NotTypeType(Value),
    LevelMismatch(Level, Level),
    ReadBackTypeMismatch(NormalExpression, NormalExpression),
    Located(Box<TCE>, Pattern),
}

Type-Checking Error.

Variants

Textual(String)

UpdateGammaFailed(Pattern)

CannotInfer(Expression)

UnresolvedName(String)

InvalidConstructor(String)

MissingCase(String)

UnexpectedCases(String)

Unreachable(&'static str, u32, u32)

Reaching somewhere that is not expected to reach.

WantSumBut(Either<Value, Expression>)

DuplicateBranch(String)

WantSigmaBut(Value)

WantPiBut(Value, Expression)

We can get the argument of application here, to better report error.

TypeMismatch(Value, Value)

Actually first value, expected second value.

NotTypeType(Value)

Want a type's type, but unfortunately it's not.

LevelMismatch(Level, Level)

Actually first level, expected second level.

ReadBackTypeMismatch(NormalExpression, NormalExpression)

First argument is inferred value, second is expected.

Located(Box<TCE>, Pattern)

Implementations

impl TCE

pub fn default_error<T>(str: String) -> TCM<T>

Default TCE

Trait Implementations

impl Clone for TCE

fn clone(&self) -> TCE

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TCE

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for TCE

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.