pub struct TypeApp {
pub head: TypeAtom,
pub rest: Vec<TypeAtom>,
}Expand description
txapp — a postfix type application arg1 arg2 … argN ctor, upstream’s
N-ary chain flattened into a greedy atom run (the way OpChain/PatCons
flatten their own left-recursions). head is always
present; when rest is non-empty the LAST atom is the
type constructor (a bare or Mod.-qualified name — list/option/
result/Eq.t/implicit) and every atom before it (including head)
is one of its arguments. This is unambiguous because SATySFi always
parenthesizes a nested single-argument application (('a list) list,
('a t) implicit — never 'a list list), so a flat run of atoms can
only be one constructor applied to the preceding arguments:
int→head = int,rest = [](a bare atom).'a option→head = 'a,rest = [option](one arg).'a 'e result→head = 'a,rest = ['e, result](satysfi-base’s two-parameterresult/either/t/map).('a Eq.t) implicit→head = ('a Eq.t),rest = [implicit](satysfi-base’s typeclass-dictionary marker).
Elaboration (typecheck::lower_type_app) does the head/args/ctor split;
the grammar itself is a plain, always-terminating greedy Vec<TypeAtom>
(each atom consumes ≥1 token, stopping at the first non-atom — ->,
*, ), ;, …). Both the unqualified and Mod.-qualified constructor
forms fall out for free, since a Mod.t ctor is just a
TypeAtom::NameMod like any other atom.
Fields§
§head: TypeAtom§rest: Vec<TypeAtom>Trait Implementations§
Source§impl<__SyanMacro_Atom> Parse<__SyanMacro_Atom> for TypeApp
impl<__SyanMacro_Atom> Parse<__SyanMacro_Atom> for TypeApp
Source§type Error = ParseError<<__SyanMacro_Atom as Spanned>::Span>
type Error = ParseError<<__SyanMacro_Atom as Spanned>::Span>
<FieldTy as Parse<Atom>>::Error: Into<…> predicate re-creates a projection cycle on a
recursive field (E0275), which decycle’s bound-peeling does not break.