flux_infer/
fn_subtyping.rs

1//! Subtyping between function signatures.
2//!
3//! This is used to check, e.g., that the signature of a trait method's implementation is a subtype
4//! of the trait method's signature, that a closure satisfies an `Fn` trait obligation, or that a fn
5//! pointer can be used where another fn pointer is expected.
6
7use std::iter;
8
9use flux_middle::{
10    queries::QueryErr,
11    rty::{
12        self, BaseTy, EarlyBinder, Expr, Mutability, Path, PolyFnSig, PtrKind, Ty, TyKind,
13        fold::{TypeFoldable, TypeFolder, TypeSuperFoldable},
14    },
15};
16use itertools::{Itertools, izip};
17use rustc_hir::def_id::DefId;
18use rustc_span::Span;
19
20use crate::{
21    infer::{ConstrReason, InferCtxt, InferResult, LocEnv, SubtypeReason},
22    projections::NormalizeExt as _,
23};
24
25/// `SubFn` lets us reuse _most_ of the same code for `check_fn_subtyping` for both the case where
26/// we have an early-bound function signature (e.g., for a trait method???) and versions without,
27/// e.g. a plain closure against its FnTraitPredicate obligation.
28#[derive(Debug)]
29pub enum SubFn {
30    Poly(DefId, EarlyBinder<rty::PolyFnSig>, rty::GenericArgs),
31    Mono(rty::PolyFnSig),
32}
33
34impl SubFn {
35    pub fn poly_sig(&self) -> &rty::PolyFnSig {
36        match self {
37            SubFn::Poly(_, sig, _) => sig.skip_binder_ref(),
38            SubFn::Mono(sig) => sig,
39        }
40    }
41}
42
43/// The function `check_fn_subtyping` does a function subtyping check between
44/// the sub-type (T_f) corresponding to the type of `def_id` @ `args` and the
45/// super-type (T_g) corresponding to the `oblig_sig`. This subtyping is handled
46/// as akin to the code
47///
48///   T_f := (S1,...,Sn) -> S
49///   T_g := (T1,...,Tn) -> T
50///   T_f <: T_g
51///
52///  fn g(x1:T1,...,xn:Tn) -> T {
53///      f(x1,...,xn)
54///  }
55///
56/// The `env` should be empty: it is used to hold the locations of the strong references in the
57/// signatures.
58pub fn check_fn_subtyping(
59    infcx: &mut InferCtxt,
60    env: &mut impl LocEnv,
61    sub_sig: SubFn,
62    super_sig: &rty::PolyFnSig,
63    span: Span,
64) -> InferResult {
65    let mut infcx = infcx.branch();
66    let mut infcx = infcx.at(span);
67    let tcx = infcx.genv.tcx();
68
69    let super_sig = super_sig
70        .try_replace_bound_vars(
71            |_| Ok::<_, QueryErr>(rty::ReErased),
72            |sort, _, kind| {
73                let sort =
74                    sort.deeply_normalize_sorts(infcx.def_id, infcx.genv, infcx.region_infcx)?;
75                Ok(Expr::fvar(infcx.define_bound_reft_var(&sort, kind)))
76            },
77        )?
78        .deeply_normalize(&mut infcx)?;
79
80    // 1. Unpack `T_g` input types
81    let actuals = super_sig
82        .inputs()
83        .iter()
84        .map(|ty| infcx.unpack(ty))
85        .collect_vec();
86
87    let actuals = unfold_local_ptrs(&mut infcx, env, sub_sig.poly_sig(), &actuals)?;
88    let actuals = infer_under_mut_ref_hack(&mut infcx, &actuals[..], sub_sig.poly_sig());
89
90    let output = infcx.ensure_resolved_evars(|infcx| {
91        // 2. Fresh names for `T_f` refine-params / Instantiate fn_def_sig and normalize it
92        // in subtyping_mono, skip next two steps...
93        let sub_sig = match sub_sig {
94            SubFn::Poly(def_id, early_sig, sub_args) => {
95                let refine_args = infcx.instantiate_refine_args(def_id, &sub_args)?;
96                early_sig.instantiate(tcx, &sub_args, &refine_args)
97            }
98            SubFn::Mono(sig) => sig,
99        };
100        // ... jump right here.
101        let sub_sig = sub_sig
102            .try_replace_bound_vars(
103                |_| Ok::<_, QueryErr>(rty::ReErased),
104                |sort, mode, _| {
105                    let sort =
106                        sort.deeply_normalize_sorts(infcx.def_id, infcx.genv, infcx.region_infcx)?;
107                    Ok(infcx.fresh_infer_var(&sort, mode))
108                },
109            )?
110            .deeply_normalize(infcx)?;
111
112        // 3. INPUT subtyping (g-input <: f-input)
113        for requires in super_sig.requires() {
114            infcx.assume_pred(requires);
115        }
116        infcx.check_pred(
117            Expr::implies(super_sig.no_panic(), sub_sig.no_panic()),
118            ConstrReason::Subtype(SubtypeReason::Input),
119        );
120        for (actual, formal) in iter::zip(actuals, sub_sig.inputs()) {
121            let reason = ConstrReason::Subtype(SubtypeReason::Input);
122            infcx.subtyping_with_env(env, &actual, formal, reason)?;
123        }
124        // we check the requires AFTER the actual-formal subtyping as the above may unfold stuff in
125        // the actuals
126        for requires in sub_sig.requires() {
127            let reason = ConstrReason::Subtype(SubtypeReason::Requires);
128            infcx.check_pred(requires, reason);
129        }
130
131        Ok(sub_sig.output())
132    })?;
133
134    let output = infcx
135        .fully_resolve_evars(&output)
136        .replace_bound_refts_with(|sort, _, kind| {
137            Expr::fvar(infcx.define_bound_reft_var(sort, kind))
138        });
139
140    // 4. OUTPUT subtyping (f_out <: g_out)
141    infcx.ensure_resolved_evars(|infcx| {
142        let super_output = super_sig
143            .output()
144            .replace_bound_refts_with(|sort, mode, _| infcx.fresh_infer_var(sort, mode));
145        let reason = ConstrReason::Subtype(SubtypeReason::Output);
146        infcx.subtyping(&output.ret, &super_output.ret, reason)?;
147
148        // 6. Update state with Output "ensures" and check super ensures
149        env.assume_ensures(infcx, &output.ensures, span);
150        env.fold_local_ptrs(infcx)?;
151        env.check_ensures(
152            infcx,
153            &super_output.ensures,
154            ConstrReason::Subtype(SubtypeReason::Ensures),
155        )
156    })
157}
158
159/// Temporarily (around a function call) convert an `&mut` to an `&strg` to allow for the call to be
160/// checked. This is done by unfolding the `&mut` into a local pointer at the call-site and then
161/// folding the pointer back into the `&mut` upon return.
162/// See also [`LocEnv::fold_local_ptrs`].
163///
164/// ```text
165///             unpack(T) = T'
166/// ---------------------------------------[local-unfold]
167/// Γ ; &mut T => Γ, l:[<: T] T' ; ptr(l)
168/// ```
169pub fn unfold_local_ptrs(
170    infcx: &mut InferCtxt,
171    env: &mut impl LocEnv,
172    fn_sig: &PolyFnSig,
173    actuals: &[Ty],
174) -> InferResult<Vec<Ty>> {
175    // We *only* need to know whether each input is a &strg or not
176    let fn_sig = fn_sig.skip_binder_ref();
177    let mut tys = vec![];
178    for (actual, input) in izip!(actuals, fn_sig.inputs()) {
179        let actual = if let (
180            TyKind::Indexed(BaseTy::Ref(re, bound, Mutability::Mut), _),
181            TyKind::StrgRef(_, _, _),
182        ) = (actual.kind(), input.kind())
183        {
184            let loc = env.unfold_local_ptr(infcx, bound)?;
185            let path1 = Path::new(loc, rty::List::empty());
186            Ty::ptr(PtrKind::Mut(*re), path1)
187        } else {
188            actual.clone()
189        };
190        tys.push(actual);
191    }
192    Ok(tys)
193}
194
195struct SkipConstr;
196
197impl TypeFolder for SkipConstr {
198    fn fold_ty(&mut self, ty: &rty::Ty) -> rty::Ty {
199        if let rty::TyKind::Constr(_, inner_ty) = ty.kind() {
200            inner_ty.fold_with(self)
201        } else {
202            ty.super_fold_with(self)
203        }
204    }
205}
206
207fn is_indexed_mut_skipping_constr(ty: &Ty) -> bool {
208    let ty = SkipConstr.fold_ty(ty);
209    if let rty::Ref!(_, inner_ty, Mutability::Mut) = ty.kind()
210        && let TyKind::Indexed(..) = inner_ty.kind()
211    {
212        true
213    } else {
214        false
215    }
216}
217
218/// HACK(nilehmann) This let us infer parameters under mutable references for the simple case
219/// where the formal argument is of the form `&mut B[@n]`, e.g., the type of the first argument
220/// to `RVec::get_mut` is `&mut RVec<T>[@n]`. We should remove this after we implement opening of
221/// mutable references.
222pub fn infer_under_mut_ref_hack(
223    rcx: &mut InferCtxt,
224    actuals: &[Ty],
225    fn_sig: &PolyFnSig,
226) -> Vec<Ty> {
227    iter::zip(actuals, fn_sig.skip_binder_ref().inputs())
228        .map(|(actual, formal)| {
229            if let rty::Ref!(re, deref_ty, Mutability::Mut) = actual.kind()
230                && is_indexed_mut_skipping_constr(formal)
231            {
232                rty::Ty::mk_ref(*re, rcx.unpack(deref_ty), Mutability::Mut)
233            } else {
234                actual.clone()
235            }
236        })
237        .collect()
238}
flux_infer/fn_subtyping.rs

flux_infer/
fn_subtyping.rs
