flux_refineck::checker

Function check_fn_subtyping

Source
fn check_fn_subtyping(
    infcx: &mut InferCtxt<'_, '_, '_>,
    def_id: &DefId,
    sub_sig: EarlyBinder<PolyFnSig>,
    sub_args: &[GenericArg],
    super_sig: EarlyBinder<PolyFnSig>,
    super_args: Option<(&GenericArgs, &RefineArgs)>,
    overflow_checking: bool,
    span: Span,
) -> Result<(), CheckerError>
Expand description

The function check_fn_subtyping does a function subtyping check between the sub-type (T_f) corresponding to the type of def_id @ args and the super-type (T_g) corresponding to the oblig_sig. This subtyping is handled as akin to the code

T_f := (S1,…,Sn) -> S T_g := (T1,…,Tn) -> T T_f <: T_g

fn g(x1:T1,…,xn:Tn) -> T { f(x1,…,xn) }