diff --git a/crates/flux-infer/src/infer.rs b/crates/flux-infer/src/infer.rs
index 8e3acfb65d..94b2ecae34 100644
--- a/crates/flux-infer/src/infer.rs
+++ b/crates/flux-infer/src/infer.rs
@@ -462,27 +462,31 @@ impl InferCtxtAt<'_, '_, '_, '_> {
Ok(())
}
- /// Relate types via subtyping for a function call. This is the same as [`InferCtxtAt::subtyping`]
- /// except that we also consider strong references.
- pub fn fun_arg_subtyping(
+ /// 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_with_env(
&mut self,
env: &mut impl LocEnv,
a: &Ty,
b: &Ty,
reason: ConstrReason,
) -> InferResult {
- let mut sub = Sub::new(reason, self.span);
- sub.fun_args(self.infcx, env, a, b)
+ let mut sub = Sub::new(env, reason, self.span);
+ sub.tys(self.infcx, a, b)
}
- /// Relate types via subtyping and returns coroutine obligations. See comment for [`Sub::obligations`].
+ /// 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 subtyping(
&mut self,
a: &Ty,
b: &Ty,
reason: ConstrReason,
) -> InferResult<Vec<Binder<rty::CoroutineObligPredicate>>> {
- let mut sub = Sub::new(reason, self.span);
+ let mut env = DummyEnv;
+ let mut sub = Sub::new(&mut env, reason, self.span);
sub.tys(self.infcx, a, b)?;
Ok(sub.obligations)
}
@@ -587,8 +591,33 @@ pub trait LocEnv {
fn get(&self, path: &Path) -> Ty;
}
+struct DummyEnv;
+
+impl LocEnv for DummyEnv {
+ fn ptr_to_ref(
+ &mut self,
+ _: &mut InferCtxtAt,
+ _: ConstrReason,
+ _: Region,
+ _: &Path,
+ _: Ty,
+ ) -> InferResult<Ty> {
+ bug!("call to `ptr_to_ref` on `DummyEnv`")
+ }
+
+ fn unfold_strg_ref(&mut self, _: &mut InferCtxt, _: &Path, _: &Ty) -> InferResult<Loc> {
+ bug!("call to `unfold_str_ref` on `DummyEnv`")
+ }
+
+ fn get(&self, _: &Path) -> Ty {
+ bug!("call to `get` on `DummyEnv`")
+ }
+}
+
/// Context used to relate two types `a` and `b` via subtyping
-struct Sub {
+struct Sub<'a, E> {
+ /// The environment to lookup locations pointed to by [`TyKind::Ptr`].
+ env: &'a mut E,
reason: ConstrReason,
span: Span,
/// FIXME(nilehmann) This is used to store coroutine obligations generated during subtyping when
@@ -597,46 +626,53 @@ struct Sub {
obligations: Vec<Binder<rty::CoroutineObligPredicate>>,
}
-impl Sub {
- fn new(reason: ConstrReason, span: Span) -> Self {
- Self { reason, span, obligations: vec![] }
+impl<'a, E: LocEnv> Sub<'a, E> {
+ fn new(env: &'a mut E, reason: ConstrReason, span: Span) -> Self {
+ Self { env, reason, span, obligations: vec![] }
}
fn tag(&self) -> Tag {
Tag::new(self.reason, self.span)
}
- fn fun_args(
- &mut self,
- infcx: &mut InferCtxt,
- env: &mut impl LocEnv,
- a: &Ty,
- b: &Ty,
- ) -> InferResult {
+ fn tys(&mut self, infcx: &mut InferCtxt, a: &Ty, b: &Ty) -> InferResult {
let infcx = &mut infcx.branch();
+
// infcx.push_trace(TypeTrace::tys(a, b));
+ // We *fully* unpack the lhs before continuing to be able to prove goals like this
+ // ∃a. (i32[a], ∃b. {i32[b] | a > b})} <: ∃a,b. ({i32[a] | b < a}, i32[b])
+ // See S4.5 in https://arxiv.org/pdf/2209.13000v1.pdf
+ let a = infcx.unpack(a);
match (a.kind(), b.kind()) {
+ (TyKind::Exists(..), _) => {
+ bug!("existentials should be removed by the unpacking");
+ }
+ (TyKind::Constr(..), _) => {
+ bug!("constraint types should removed by the unpacking");
+ }
+
(_, TyKind::Exists(ctor_b)) => {
- infcx.enter_exists(ctor_b, |infcx, ty_b| self.fun_args(infcx, env, a, &ty_b))
+ infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b))
}
(_, TyKind::Constr(pred_b, ty_b)) => {
infcx.check_pred(pred_b, self.tag());
- self.fun_args(infcx, env, a, ty_b)
+ self.tys(infcx, &a, ty_b)
}
+
(TyKind::Ptr(PtrKind::Mut(_), path1), TyKind::StrgRef(_, path2, ty2)) => {
// We should technically remove `path1` from `env`, but we are assuming that functions
// always give back ownership of the location so `path1` is going to be overwritten
// after the call anyways.
- let ty1 = env.get(path1);
+ let ty1 = self.env.get(path1);
infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
self.tys(infcx, &ty1, ty2)
}
(TyKind::StrgRef(_, path1, ty1), TyKind::StrgRef(_, path2, ty2)) => {
- // We has to unfold strong references prior to a subtyping check. Normally, when
+ // We have to unfold strong references prior to a subtyping check. Normally, when
// checking a function body, a `StrgRef` is automatically unfolded i.e. `x:&strg T`
// is turned into a `x:ptr(l); l: T` where `l` is some fresh location. However, we
- // need the below to do a similar unfolding in `check_fn_subtyping` where we just
+ // need the below to do a similar unfolding during function subtyping where we just
// have the super-type signature that needs to be unfolded. We also add the binding
// to the environment so that we can:
// (1) UPDATE the location after the call, and
@@ -644,8 +680,8 @@ impl Sub {
// Same as the `Ptr` case above we should remove the location from the environment
// after unfolding to consume it, but we are assuming functions always give back
// ownership.
- env.unfold_strg_ref(infcx, path1, ty1)?;
- let ty1 = env.get(path1);
+ self.env.unfold_strg_ref(infcx, path1, ty1)?;
+ let ty1 = self.env.get(path1);
infcx.unify_exprs(&path1.to_expr(), &path2.to_expr());
self.tys(infcx, &ty1, ty2)
}
@@ -657,37 +693,16 @@ impl Sub {
// we solve them.
self.idxs_eq(infcx, &Expr::unit(), idx);
- let mut at = infcx.at(self.span);
- env.ptr_to_ref(&mut at, self.reason, *re, path, bound.clone())?;
+ self.env.ptr_to_ref(
+ &mut infcx.at(self.span),
+ self.reason,
+ *re,
+ path,
+ bound.clone(),
+ )?;
Ok(())
}
- _ => self.tys(infcx, a, b),
- }
- }
- fn tys(&mut self, infcx: &mut InferCtxt, a: &Ty, b: &Ty) -> InferResult {
- let infcx = &mut infcx.branch();
-
- // infcx.push_trace(TypeTrace::tys(a, b));
-
- // We *fully* unpack the lhs before continuing to be able to prove goals like this
- // ∃a. (i32[a], ∃b. {i32[b] | a > b})} <: ∃a,b. ({i32[a] | b < a}, i32[b])
- // See S4.5 in https://arxiv.org/pdf/2209.13000v1.pdf
- let a = infcx.unpack(a);
- match (a.kind(), b.kind()) {
- (TyKind::Exists(..), _) => {
- bug!("existentials should be removed by the unpacking");
- }
- (TyKind::Constr(..), _) => {
- bug!("constraint types should removed by the unpacking");
- }
- (_, TyKind::Exists(ctor_b)) => {
- infcx.enter_exists(ctor_b, |infcx, ty_b| self.tys(infcx, &a, &ty_b))
- }
- (_, TyKind::Constr(pred_b, ty_b)) => {
- infcx.check_pred(pred_b, self.tag());
- self.tys(infcx, &a, ty_b)
- }
(TyKind::Indexed(bty_a, idx_a), TyKind::Indexed(bty_b, idx_b)) => {
self.btys(infcx, bty_a, bty_b)?;
self.idxs_eq(infcx, idx_a, idx_b);
diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs
index f432e5b598..3bb0187545 100644
--- a/crates/flux-refineck/src/checker.rs
+++ b/crates/flux-refineck/src/checker.rs
@@ -267,7 +267,7 @@ fn check_fn_subtyping(
}
for (actual, formal) in iter::zip(actuals, sub_sig.inputs()) {
let reason = ConstrReason::Subtype(SubtypeReason::Input);
- infcx.fun_arg_subtyping(&mut env, &actual, formal, reason)?;
+ infcx.subtyping_with_env(&mut env, &actual, formal, reason)?;
}
// we check the requires AFTER the actual-formal subtyping as the above may unfold stuff in the actuals
for requires in sub_sig.requires() {
@@ -807,7 +807,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
// Check arguments
for (actual, formal) in iter::zip(actuals, fn_sig.inputs()) {
- at.fun_arg_subtyping(env, &actual, formal, ConstrReason::Call)
+ at.subtyping_with_env(env, &actual, formal, ConstrReason::Call)
.with_span(span)?;
}
// Replace evars