Enum Solved 

pub enum Solved {
    Typed {
        term: Box<TypedTerm>,
        context: Vec<Predicate>,
    },
    NoBody,
    Untranslatable {
        span: NodeSpan,
    },
    UnboundName {
        name: String,
        span: NodeSpan,
    },
    Rejected,
}

What the typer has to say about one declaration.

A phase that answers with types has to answer for every declaration it was given, including the ones it could not type: a caller handed only the ones that worked cannot tell a declaration the typer verified from one it walked past, and emitting code for the second is a miscompile. So each way a declaration goes untyped gets a variant, and typer::type_check_recovering returns one entry per declaration either way.

Variants

Typed

The declaration’s typed term, with the final substitution applied to every node — the zonk. Its own tpe is the declaration’s type; each node below it carries the type inference solved for that sub-expression.

Boxed because a term carries a whole QualName — package included — for every union and constructor it names, and every other variant would otherwise pay for its size.

The term may hold a hole, with an error standing behind it, and a backend refuses it.

Fields

term: Box<TypedTerm>

context: Vec<Predicate>

What the declaration’s annotation required of its type variables, with the final substitution applied: Declaration::context.

NoBody

A declaration of a module foreign facade, whose body is a synthetic placeholder rather than anything the user wrote. Nothing about it is inferred.

This variant carries nothing, so Solved::typed answers None for it: the declaration’s type is the signature the facade declares, and it stays where canonicalization put it, on canonical::Value::TypedValue’s tpe. A consumer reading these entries is walking the same canonical::Module the map was solved from — type_check takes one and keys the map the way its values is keyed — so the signature is one lookup away, and repeating it here would be a second copy of it rather than something inference established. build is what reads it back out.

Untranslatable

value_to_term_and_annotation could not translate the declaration into the typer’s term language: a VarKernel reference, or a constructor naming a union the typer was given no declaration of. Nothing about the declaration was checked.

Not an Error: it is a gap in the typer rather than a mistake in the source. What it wants is a warning, which the compiler does not have yet (ERR-8, see docs/tickets/README.md) — hence the span, so that the warning has a caret the day it exists. Which of the constructs tripped it is not carried: value_to_term_and_annotation answers Option, so the reason does not survive the return.

Fields

span: NodeSpan

Where the declaration was written, annotation and body together — the only position available, since the construct that stopped the translation is not reported back.

UnboundName

Inference reached a name the typer’s environment does not hold, and nothing about the declaration was checked.

That environment holds a declared type for every value in reach that has one: the values and constructors every imported interface exposes, and this module’s own constructors and annotated declarations. A declaration of this module written without an annotation has no declared type, and a name reaching one lands here. That is not a mistake in the source, which is why this is not an Error either. A name that genuinely does not exist is caught earlier, by canonicalization, as canonical::Error::VariableNotFound, with a caret under the name.

Fields

name: String

The name as inference looked it up.

span: NodeSpan

Where it was written.

Rejected

Inference reported an error for this declaration.

The error itself is in TypeCheck::errors, beside the map this entry is in. The entry is what keeps the declaration from being merely absent, so a module with a type error still answers for every declaration it holds.

Implementations

impl Solved

pub fn typed(&self) -> Option<&TypedTerm>

The typed term, for a declaration that has one.

Trait Implementations

impl Debug for Solved

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

Formats the value using the given formatter.