Enum voile::check::monad::error::TCE

pub enum TCE {
    Textual(String),
    CannotInfer(Loc, Abs),
    CannotUnify(Val, Val),
    NotSigma(Loc, TVal),
    NotPi(Loc, TVal),
    NotSubtype(TVal, TVal),
    NotTypeAbs(Loc, Abs),
    NotTypeVal(Loc, Val),
    NotRowType(VarRec, Loc, Val),
    NotEmpty(Loc, Val),
    NotRecVal(Loc, Val),
    NotUniverseVal(Loc, Val),
    TypeNotInGamma(Loc),
    OverlappingVariant(Loc, String),
    DuplicateField(Loc, String),
    UnexpectedVariant(Loc, String),
    MissingVariant(VarRec, String),
    DbiOverflow(DBI, DBI),
    LevelMismatch(Loc, Level, Level),
    LookUpFailed(Ident),
    Wrapped(Box<Self>, Loc),
    ReDefine(Loc, Loc),
    MetaRecursion(MI),
    MetaWithNonVar(Loc),
    MetaUnsolved(MI),
}

Type-Checking Error.

Variants

Textual(String)

CannotInfer(Loc, Abs)

CannotUnify(Val, Val)

NotSigma(Loc, TVal)

NotPi(Loc, TVal)

NotSubtype(TVal, TVal)

Expected the first TVal to be the subtype of the second TVal.

NotTypeAbs(Loc, Abs)

NotTypeVal(Loc, Val)

NotRowType(VarRec, Loc, Val)

NotEmpty(Loc, Val)

NotRecVal(Loc, Val)

NotUniverseVal(Loc, Val)

TypeNotInGamma(Loc)

OverlappingVariant(Loc, String)

DuplicateField(Loc, String)

UnexpectedVariant(Loc, String)

MissingVariant(VarRec, String)

DbiOverflow(DBI, DBI)

Maximum DBI vs. Requested DBI

LevelMismatch(Loc, Level, Level)

Expected the first level to be smaller than second. The String represents the expression.

LookUpFailed(Ident)

Cannot find the definition.

Wrapped(Box<Self>, Loc)

ReDefine(Loc, Loc)

The definition at the first Loc will hide the definition at the second Loc.

MetaRecursion(MI)

Recursive metas are disallowed.

MetaWithNonVar(Loc)

Meta solution should be passed with bound variables only.

MetaUnsolved(MI)

Unsolved metas are reported as errors.

Implementations

impl TCE

pub fn wrap(self, info: Loc) -> Self

pub fn duplicate_field(ident: Ident) -> Self

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<(), FmtError>

Formats the value using the given formatter.

impl Eq for TCE

impl PartialEq<TCE> for TCE

fn eq(&self, other: &TCE) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &TCE) -> bool

This method tests for !=.

impl StructuralEq for TCE

impl StructuralPartialEq for TCE