Struct InferCtxtAt

pub struct InferCtxtAt<'a, 'infcx, 'genv, 'tcx> {
    pub infcx: &'a mut InferCtxt<'infcx, 'genv, 'tcx>,
    pub span: Span,
}

Fields

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

span: Span

Implementations

impl<'genv, 'tcx> InferCtxtAt<'_, '_, 'genv, 'tcx>

fn tag(&self, reason: ConstrReason) -> Tag

pub fn check_pred(&mut self, pred: impl Into<Expr>, reason: ConstrReason)

pub fn check_non_closure_clauses( &mut self, clauses: &[Clause], reason: ConstrReason, ) -> InferResult

pub fn subtyping_with_env( &mut self, env: &mut impl LocEnv, a: &Ty, b: &Ty, reason: ConstrReason, ) -> InferResult

Relate types via subtyping. This is the same as InferCtxtAt::subtyping except that we also require a LocEnv to handle pointers and strong references

pub fn subtyping( &mut self, a: &Ty, b: &Ty, reason: ConstrReason, ) -> InferResult<Vec<Binder<CoroutineObligPredicate>>>

Relate types via subtyping and returns coroutine obligations. This doesn’t handle subtyping when strong references are involved.

See comment for Sub::obligations.

pub fn check_constructor( &mut self, variant: EarlyBinder<PolyVariant>, generic_args: &[GenericArg], fields: &[Ty], reason: ConstrReason, ) -> InferResult<Ty>

pub fn ensure_resolved_evars<R>( &mut self, f: impl FnOnce(&mut InferCtxtAt<'_, '_, 'genv, 'tcx>) -> InferResult<R>, ) -> InferResult<R>

Methods from Deref<Target = InferCtxt<'a, 'genv, 'tcx>>

pub fn at(&mut self, span: Span) -> InferCtxtAt<'_, 'infcx, 'genv, 'tcx>

pub fn instantiate_refine_args( &mut self, callee_def_id: DefId, args: &[GenericArg], ) -> InferResult<List<Expr>>

pub fn instantiate_generic_args( &mut self, args: &[GenericArg], ) -> Vec<GenericArg>

pub fn fresh_infer_var(&self, sort: &Sort, mode: InferMode) -> Expr

pub fn fresh_infer_var_for_hole( &mut self, binders: &[BoundVariableKinds], kind: HoleKind, ) -> Expr

pub fn fresh_kvar( &self, binders: &[BoundVariableKinds], encoding: KVarEncoding, ) -> Expr

Generate a fresh kvar in the current scope. See KVarGen::fresh.

fn fresh_evar(&self) -> Expr

pub fn unify_exprs(&self, a: &Expr, b: &Expr)

fn enter_exists<T, U>( &mut self, t: &Binder<T>, f: impl FnOnce(&mut InferCtxt<'_, 'genv, 'tcx>, T) -> U, ) -> U

where T: TypeFoldable,

pub fn push_evar_scope(&mut self)

Used in conjunction with InferCtxt::pop_evar_scope to ensure evars are solved at the end of some scope, for example, to ensure all evars generated during a function call are solved after checking argument subtyping. These functions can be used in a stack-like fashion to create nested scopes.

pub fn pop_evar_scope(&mut self) -> InferResult

Pop a scope and check all evars have been solved. This only check evars generated from the last call to InferCtxt::push_evar_scope.

pub fn ensure_resolved_evars<R>( &mut self, f: impl FnOnce(&mut Self) -> InferResult<R>, ) -> InferResult<R>

Convenience method pairing InferCtxt::push_evar_scope and InferCtxt::pop_evar_scope.

pub fn fully_resolve_evars<T: TypeFoldable>(&self, t: &T) -> T

pub fn tcx(&self) -> TyCtxt<'tcx>

pub fn cursor(&self) -> &Cursor<'infcx>

pub fn change_item<'a>( &'a mut self, def_id: LocalDefId, region_infcx: &'a InferCtxt<'tcx>, ) -> InferCtxt<'a, 'genv, 'tcx>

pub fn move_to( &mut self, marker: &Marker, clear_children: bool, ) -> InferCtxt<'_, 'genv, 'tcx>

pub fn branch(&mut self) -> InferCtxt<'_, 'genv, 'tcx>

pub fn define_var(&mut self, sort: &Sort) -> Name

pub fn check_pred(&mut self, pred: impl Into<Expr>, tag: Tag)

pub fn assume_pred(&mut self, pred: impl Into<Expr>)

pub fn unpack(&mut self, ty: &Ty) -> Ty

pub fn marker(&self) -> Marker

pub fn hoister( &mut self, assume_invariants: bool, ) -> Hoister<Unpacker<'_, 'infcx>>

pub fn assume_invariants(&mut self, ty: &Ty)

fn check_impl( &mut self, pred1: impl Into<Expr>, pred2: impl Into<Expr>, tag: Tag, )

Trait Implementations

impl<'a, 'infcx, 'genv, 'tcx> Debug for InferCtxtAt<'a, 'infcx, 'genv, 'tcx>

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

Formats the value using the given formatter.

impl<'a, 'genv, 'tcx> Deref for InferCtxtAt<'_, 'a, 'genv, 'tcx>

type Target = InferCtxt<'a, 'genv, 'tcx>

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl DerefMut for InferCtxtAt<'_, '_, '_, '_>

fn deref_mut(&mut self) -> &mut Self::Target

Mutably dereferences the value.