Struct ImplicitParamInferer 

pub(crate) struct ImplicitParamInferer<'a, 'genv, 'tcx> {
    infcx: &'a mut InferCtxt<'genv, 'tcx>,
    errors: Errors<'genv>,
}

Before the main sort inference, we do a first traversal checking all implicitly scoped parameters declared with @ or # and infer their sort based on the type they are indexing, e.g., if n was declared as i32[@n], we infer int for n.

This prepass is necessary because sometimes the order in which we traverse expressions can affect what we can infer. By resolving implicit parameters first, we ensure more consistent and complete inference regardless of how expressions are later traversed.

It should be possible to improve sort checking (e.g., by allowing partially resolved sorts in function position) such that we don’t need this anymore.

Fields

infcx: &'a mut InferCtxt<'genv, 'tcx>

errors: Errors<'genv>

Implementations

impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>

pub(crate) fn infer( infcx: &'a mut InferCtxt<'genv, 'tcx>, node: &OwnerNode<'genv>, ) -> Result<(), ErrorGuaranteed>

fn infer_implicit_params(&mut self, idx: &Expr<'_>, expected: &Sort)

Trait Implementations

impl<'genv> Visitor<'genv> for ImplicitParamInferer<'_, 'genv, '_>

fn visit_ty(&mut self, ty: &Ty<'genv>)

fn visit_flux_item(&mut self, item: &FluxItem<'v>)

fn visit_qualifier(&mut self, qualifier: &Qualifier<'v>)

fn visit_sort_decl(&mut self, sort_decl: &SortDecl)

fn visit_func(&mut self, func: &SpecFunc<'v>)

fn visit_primop_prop(&mut self, prop: &PrimOpProp<'v>)

fn visit_node(&mut self, node: &OwnerNode<'v>)

fn visit_item(&mut self, item: &Item<'v>)

fn visit_trait_item(&mut self, trait_item: &TraitItem<'v>)

fn visit_impl_item(&mut self, impl_item: &ImplItem<'v>)

fn visit_foreign_item(&mut self, foreign_item: &ForeignItem<'v>)

fn visit_generics(&mut self, generics: &Generics<'v>)

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'v>)

fn visit_impl(&mut self, impl_: &Impl<'v>)

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'v>)

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'v>)

fn visit_struct_def(&mut self, struct_def: &StructDef<'v>)

fn visit_enum_def(&mut self, enum_def: &EnumDef<'v>)

fn visit_variant(&mut self, variant: &VariantDef<'v>)

fn visit_field_def(&mut self, field: &FieldDef<'v>)

fn visit_variant_ret(&mut self, ret: &VariantRet<'v>)

fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'v>)

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'v>)

fn visit_generic_bound(&mut self, bound: &GenericBound<'v>)

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'v>)

fn visit_fn_sig(&mut self, sig: &FnSig<'v>)

fn visit_fn_decl(&mut self, decl: &FnDecl<'v>)

fn visit_refine_param(&mut self, param: &RefineParam<'v>)

fn visit_requires(&mut self, requires: &Requires<'v>)

fn visit_ensures(&mut self, ensures: &Ensures<'v>)

fn visit_fn_output(&mut self, output: &FnOutput<'v>)

fn visit_generic_arg(&mut self, arg: &GenericArg<'v>)

fn visit_lifetime(&mut self, _lft: &Lifetime)

fn visit_bty(&mut self, bty: &BaseTy<'v>)

fn visit_qpath(&mut self, qpath: &QPath<'v>)

fn visit_path(&mut self, path: &Path<'v>)

fn visit_path_segment(&mut self, segment: &PathSegment<'v>)

fn visit_assoc_item_constraint(&mut self, constraint: &AssocItemConstraint<'v>)

fn visit_sort(&mut self, sort: &Sort<'v>)

fn visit_sort_path(&mut self, path: &SortPath<'v>)

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'v>)

fn visit_func_sort(&mut self, func: &FuncSort<'v>)

fn visit_expr(&mut self, expr: &Expr<'v>)

fn visit_field_expr(&mut self, expr: &FieldExpr<'v>)

fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'v>)

fn visit_literal(&mut self, _lit: &Lit)

fn visit_path_expr(&mut self, _path: &PathExpr<'v>)