From 57de9c98368057dec224c2e4189722a8061c675a Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Wed, 22 May 2024 13:13:44 -0700 Subject: [PATCH 01/25] add stuff to generic_const test --- tests/tests/todo/generic_const.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/tests/todo/generic_const.rs b/tests/tests/todo/generic_const.rs index 76e99e0f44..60a7924077 100644 --- a/tests/tests/todo/generic_const.rs +++ b/tests/tests/todo/generic_const.rs @@ -5,3 +5,16 @@ pub fn from_array(items: [i32; N]) -> Vec { fn test() -> Vec { from_array([1, 2, 3]) } + + +fn bad(arr: &[i32; N]) -> i32 { + arr[0] //~ ERROR refinement type +} + +fn good(arr: &[i32; N]) -> i32 { + if (N > 0) { + arr[0] //~ ERROR refinement type + } else { + 99 + } +} From a383d2a55796690383f9bbeab18d3de3d59ada95 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Fri, 19 Jul 2024 17:14:06 -0700 Subject: [PATCH 02/25] next: onto lower type --- crates/flux-fhir-analysis/src/conv/mod.rs | 33 ++++++++++++++++++++++- crates/flux-middle/src/fhir.rs | 5 ++++ crates/flux-middle/src/fhir/lift.rs | 9 +++++++ crates/flux-middle/src/fhir/visit.rs | 4 +++ crates/flux-middle/src/rty/fold.rs | 27 +++++++++++++++++-- crates/flux-middle/src/rty/mod.rs | 27 ++++++++++++++++++- crates/flux-middle/src/rty/pretty.rs | 15 +++++++++++ crates/flux-middle/src/sort_of.rs | 1 + crates/flux-refineck/src/type_env.rs | 1 + 9 files changed, 118 insertions(+), 4 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 123f43e101..37fc00a5e2 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -435,6 +435,20 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { Ok(clauses) } + fn conv_poly_trait_ref_dyn( + poly_trait_ref: &fhir::PolyTraitRef, + ) -> QueryResult { + let trait_segment = poly_trait_ref.trait_ref.last_segment(); + + if !poly_trait_ref.bound_generic_params.is_empty() || !trait_segment.args.is_empty() { + bug!("unexpected! conv_poly_dyn_trait_ref") + } + + let trait_ref = + rty::TraitRef { def_id: poly_trait_ref.trait_def_id(), args: List::empty() }; + Ok(rty::PolyTraitRef { trait_ref, bound_generic_params: List::empty() }) + } + /// Converts a `T: Trait` bound fn conv_poly_trait_ref( &mut self, @@ -453,8 +467,8 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { vec![self.ty_to_generic_arg(self_param.kind, bounded_ty_span, bounded_ty)?]; self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; self.fill_generic_args_defaults(trait_id, &mut args)?; - let trait_ref = rty::TraitRef { def_id: trait_id, args: args.into() }; + let pred = rty::TraitPredicate { trait_ref: trait_ref.clone() }; let vars = poly_trait_ref .bound_generic_params @@ -788,6 +802,23 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let alias_ty = rty::AliasTy::new(def_id, args, refine_args); Ok(rty::Ty::alias(rty::AliasKind::Opaque, alias_ty)) } + fhir::TyKind::TraitObject(poly_traits, lft, syn) => { + let poly_traits: List = poly_traits + .iter() + .map(|poly_trait| Self::conv_poly_trait_ref_dyn(poly_trait)) + .try_collect()?; + let region = self.conv_lifetime(env, *lft); + let syn = Self::conv_trait_object_syntax(syn); + Ok(rty::Ty::trait_object(poly_traits, region, syn)) + } + } + } + + fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> rty::TraitObjectSyntax { + match syn { + rustc_ast::TraitObjectSyntax::Dyn => rty::TraitObjectSyntax::Dyn, + rustc_ast::TraitObjectSyntax::DynStar => rty::TraitObjectSyntax::DynStar, + rustc_ast::TraitObjectSyntax::None => rty::TraitObjectSyntax::None, } } diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 53debd2536..c3aeb20b69 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -25,6 +25,7 @@ use flux_common::{bug, span_bug}; use flux_syntax::surface::ParamMode; pub use flux_syntax::surface::{BinOp, UnOp}; use itertools::Itertools; +use rustc_ast::TraitObjectSyntax; use rustc_data_structures::fx::{FxIndexMap, FxIndexSet}; use rustc_hash::FxHashMap; pub use rustc_hir::PrimTy; @@ -538,6 +539,7 @@ pub enum TyKind<'fhir> { Array(&'fhir Ty<'fhir>, ConstArg), RawPtr(&'fhir Ty<'fhir>, Mutability), OpaqueDef(ItemId, &'fhir [GenericArg<'fhir>], &'fhir [RefineArg<'fhir>], bool), + TraitObject(&'fhir [PolyTraitRef<'fhir>], Lifetime, TraitObjectSyntax), Never, Hole(FhirId), } @@ -1243,6 +1245,9 @@ impl fmt::Debug for Ty<'_> { "impl trait " ) } + TyKind::TraitObject(poly_traits, _lft, _syntax) => { + write!(f, "dyn {poly_traits:?}") + } } } } diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index 5566bce5fb..3ee5de5f6e 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -394,6 +394,15 @@ impl<'a, 'genv, 'tcx> LiftCtxt<'a, 'genv, 'tcx> { let args = self.lift_generic_args(args)?; fhir::TyKind::OpaqueDef(item_id, args, &[], in_trait_def) } + hir::TyKind::TraitObject(poly_traits, lft, syntax) => { + let poly_traits = try_alloc_slice!(self.genv, poly_traits, |poly_trait| { + self.lift_poly_trait_ref(*poly_trait) + })?; + + let lft = self.lift_lifetime(lft)?; + fhir::TyKind::TraitObject(poly_traits, lft, syntax) + // return self.emit_unsupported(&format!("unsupported type: {ty:#?}",)); + } _ => { return self.emit_unsupported(&format!( "unsupported type: `{}`", diff --git a/crates/flux-middle/src/fhir/visit.rs b/crates/flux-middle/src/fhir/visit.rs index f39b05ba22..48432012f9 100644 --- a/crates/flux-middle/src/fhir/visit.rs +++ b/crates/flux-middle/src/fhir/visit.rs @@ -385,6 +385,10 @@ pub fn walk_ty<'v, V: Visitor<'v>>(vis: &mut V, ty: &Ty<'v>) { } TyKind::Never => {} TyKind::Hole(_) => {} + TyKind::TraitObject(poly_traits, lft, _) => { + walk_list!(vis, visit_poly_trait_ref, poly_traits); + vis.visit_lifetime(&lft); + } } } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 50a0f79906..baf3e401a1 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -17,8 +17,8 @@ use super::{ AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Const, CoroutineObligPredicate, Ensures, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, Opaqueness, OutlivesPredicate, PolyFuncSort, - ProjectionPredicate, PtrKind, Qualifier, ReBound, Region, Sort, SubsetTy, TraitPredicate, - TraitRef, Ty, TyKind, + PolyTraitRef, ProjectionPredicate, PtrKind, Qualifier, ReBound, Region, Sort, SubsetTy, + TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -488,6 +488,21 @@ impl TypeFoldable for TraitRef { } } +impl TypeVisitable for PolyTraitRef { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + self.trait_ref.visit_with(visitor) + } +} + +impl TypeFoldable for PolyTraitRef { + fn try_fold_with(&self, folder: &mut F) -> Result { + Ok(PolyTraitRef { + bound_generic_params: self.bound_generic_params.clone(), + trait_ref: self.trait_ref.try_fold_with(folder)?, + }) + } +} + impl TypeVisitable for CoroutineObligPredicate { fn visit_with(&self, visitor: &mut V) -> ControlFlow { self.upvar_tys.visit_with(visitor)?; @@ -940,6 +955,7 @@ impl TypeSuperVisitable for BaseTy { | BaseTy::Closure(_, _) | BaseTy::Never | BaseTy::Param(_) => ControlFlow::Continue(()), + BaseTy::TraitObject(poly_traits, _, _) => poly_traits.visit_with(visitor), } } } @@ -979,6 +995,13 @@ impl TypeSuperFoldable for BaseTy { args.try_fold_with(folder)?, ) } + BaseTy::TraitObject(poly_traits, region, syn) => { + BaseTy::TraitObject( + poly_traits.try_fold_with(folder)?, + region.try_fold_with(folder)?, + *syn, + ) + } }; Ok(bty) } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index f4da559281..7b93d53c76 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -13,7 +13,6 @@ mod pretty; pub mod projections; pub mod refining; pub mod subst; - use std::{borrow::Cow, hash::Hash, iter, slice, sync::LazyLock}; pub use evars::{EVar, EVarGen}; @@ -230,6 +229,19 @@ impl TraitRef { } } +#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub struct PolyTraitRef { + pub bound_generic_params: List, + pub trait_ref: TraitRef, +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum TraitObjectSyntax { + Dyn, + DynStar, + None, +} + #[derive(PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable)] pub struct ProjectionPredicate { pub projection_ty: AliasTy, @@ -622,6 +634,14 @@ impl Ty { Self::alias(AliasKind::Projection, alias_ty) } + pub fn trait_object( + poly_traits: impl Into>, + region: Region, + syn: TraitObjectSyntax, + ) -> Ty { + BaseTy::TraitObject(poly_traits.into(), region, syn).to_ty() + } + pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty { TyKind::StrgRef(re, path, ty).intern() } @@ -951,6 +971,7 @@ pub enum BaseTy { Never, Closure(DefId, /* upvar_tys */ List), Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List), + TraitObject(List, Region, TraitObjectSyntax), Param(ParamTy), } @@ -1099,6 +1120,7 @@ impl BaseTy { | BaseTy::Array(_, _) | BaseTy::Closure(_, _) | BaseTy::Coroutine(..) + | BaseTy::TraitObject(_, _, _) | BaseTy::Never => Sort::unit(), } } @@ -1131,6 +1153,7 @@ impl BaseTy { BaseTy::Array(_, _) => todo!(), BaseTy::Never => tcx.types.never, BaseTy::Closure(_, _) => todo!(), + BaseTy::TraitObject(_, _, _) => todo!(), BaseTy::Coroutine(def_id, resume_ty, upvars) => { todo!("Generator {def_id:?} {resume_ty:?} {upvars:?}") // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg)); @@ -2055,6 +2078,8 @@ impl_slice_internable!( InferMode, Sort, GenericParamDef, + TraitRef, + PolyTraitRef, Clause, PolyVariant, Invariant, diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index 5493c65ecd..e5911b395a 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -337,6 +337,18 @@ impl Pretty for List { } } +impl Pretty for PolyTraitRef { + fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(cx, f); + // let vars = &self.bound_generic_params; + // TODO + // if !vars.is_empty() { + // w!("for <{:?}>", join!(", ", vars)) + // } + w!("{:?}", &self.trait_ref.def_id) + } +} + impl Pretty for BaseTy { fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { define_scoped!(cx, f); @@ -388,6 +400,9 @@ impl Pretty for BaseTy { } Ok(()) } + BaseTy::TraitObject(poly_traits, _, _) => { + w!("dyn {:?}", join!(", ", poly_traits)) + } } } } diff --git a/crates/flux-middle/src/sort_of.rs b/crates/flux-middle/src/sort_of.rs index f8498c3af0..edf42397aa 100644 --- a/crates/flux-middle/src/sort_of.rs +++ b/crates/flux-middle/src/sort_of.rs @@ -104,6 +104,7 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { | fhir::TyKind::Ref(_, _) | fhir::TyKind::Tuple(_) | fhir::TyKind::Array(_, _) + | fhir::TyKind::TraitObject(_, _, _) | fhir::TyKind::Never => Ok(Some(rty::Sort::unit())), fhir::TyKind::Hole(_) | fhir::TyKind::StrgRef(..) diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 3af5e9e643..b930681b8c 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -373,6 +373,7 @@ impl BasicBlockEnvShape { | BaseTy::Char | BaseTy::Never | BaseTy::Closure(_, _) + | BaseTy::TraitObject(_, _, _) | BaseTy::Coroutine(..) => bty.clone(), } } From 40861adc3967b0294e846f38e230b721b9347f2d Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Mon, 22 Jul 2024 16:16:03 -0700 Subject: [PATCH 03/25] next: onto lower type --- crates/flux-fhir-analysis/src/conv/mod.rs | 10 +++---- crates/flux-middle/src/rty/mod.rs | 18 +++++++----- crates/flux-middle/src/rty/refining.rs | 19 ++++++++++++- crates/flux-middle/src/rustc/lowering.rs | 5 ++++ crates/flux-middle/src/rustc/ty.rs | 34 ++++++++++++++++++++--- crates/flux-middle/src/rustc/ty/subst.rs | 22 ++++++++++++++- 6 files changed, 90 insertions(+), 18 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 37fc00a5e2..3b1ce10d92 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -24,7 +24,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc, + rustc::{self, ty::TraitObjectSyntax}, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -814,11 +814,11 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { } } - fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> rty::TraitObjectSyntax { + fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> TraitObjectSyntax { match syn { - rustc_ast::TraitObjectSyntax::Dyn => rty::TraitObjectSyntax::Dyn, - rustc_ast::TraitObjectSyntax::DynStar => rty::TraitObjectSyntax::DynStar, - rustc_ast::TraitObjectSyntax::None => rty::TraitObjectSyntax::None, + rustc_ast::TraitObjectSyntax::Dyn => TraitObjectSyntax::Dyn, + rustc_ast::TraitObjectSyntax::DynStar => TraitObjectSyntax::DynStar, + rustc_ast::TraitObjectSyntax::None => TraitObjectSyntax::None, } } diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 7b93d53c76..5fd35f8470 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -57,7 +57,11 @@ use crate::{ intern::{impl_internable, impl_slice_internable, Interned, List}, queries::QueryResult, rty::subst::SortSubst, - rustc::{self, mir::Place, ty::VariantDef}, + rustc::{ + self, + mir::Place, + ty::{TraitObjectSyntax, VariantDef}, + }, }; #[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)] @@ -235,12 +239,12 @@ pub struct PolyTraitRef { pub trait_ref: TraitRef, } -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub enum TraitObjectSyntax { - Dyn, - DynStar, - None, -} +// #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +// pub enum TraitObjectSyntax { +// Dyn, +// DynStar, +// None, +// } #[derive(PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable)] pub struct ProjectionPredicate { diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index f95a857a62..290ddd383b 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -6,7 +6,7 @@ use itertools::Itertools; use rustc_hir::def_id::DefId; use rustc_middle::ty::{ClosureKind, ParamTy}; -use super::fold::TypeFoldable; +use super::{fold::TypeFoldable, PolyTraitRef}; use crate::{ global_env::GlobalEnv, intern::List, @@ -170,6 +170,16 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::ClauseKind::FnTrait(pred)) } + pub fn refine_poly_trait_ref( + &self, + poly_trait_ref: &rustc::ty::PolyTraitRef, + ) -> QueryResult { + assert!(poly_trait_ref.bound_generic_params.is_empty()); + let bound_generic_params = List::empty(); + let trait_ref = self.refine_trait_ref(&poly_trait_ref.trait_ref)?; + Ok(PolyTraitRef { bound_generic_params, trait_ref }) + } + pub fn refine_trait_ref(&self, trait_ref: &rustc::ty::TraitRef) -> QueryResult { let trait_ref = rty::TraitRef { def_id: trait_ref.def_id, @@ -358,6 +368,13 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::RawPtr(ty, mu) => { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } + rustc::ty::TyKind::TraitObject(poly_traits, r, syntax) => { + let poly_traits = poly_traits + .iter() + .map(|ty| self.refine_poly_trait_ref(ty)) + .try_collect()?; + rty::BaseTy::TraitObject(poly_traits, *r, *syntax) + } }; Ok(TyOrBase::Base((self.refine)(bty))) } diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index d4fd85c4b9..7f95d1abba 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -740,6 +740,11 @@ pub(crate) fn lower_ty<'tcx>( let args = lower_generic_args(tcx, args)?; Ok(Ty::mk_generator_witness(*did, args)) } + rustc_ty::Dynamic(predicates, region, kind) => { + Err(UnsupportedReason::new(format!( + "DYN preds=`{predicates:?}`, reg={region:?}, kind={kind:?}" + ))) + } _ => Err(UnsupportedReason::new(format!("unsupported type `{ty:?}`"))), } } diff --git a/crates/flux-middle/src/rustc/ty.rs b/crates/flux-middle/src/rustc/ty.rs index 20d068e660..5560f8ca2b 100644 --- a/crates/flux-middle/src/rustc/ty.rs +++ b/crates/flux-middle/src/rustc/ty.rs @@ -43,7 +43,7 @@ pub enum BoundVariableKind { Region(BoundRegionKind), } -#[derive(Debug, Hash, Eq, PartialEq)] +#[derive(Debug, Hash, Eq, PartialEq, TyEncodable, TyDecodable)] pub struct GenericParamDef { pub def_id: DefId, pub index: u32, @@ -57,7 +57,7 @@ impl GenericParamDef { } } -#[derive(Debug, Hash, Eq, PartialEq, Clone, Copy)] +#[derive(Debug, Hash, Eq, PartialEq, Clone, Copy, TyEncodable, TyDecodable)] pub enum GenericParamDefKind { Type { has_default: bool }, Lifetime, @@ -93,7 +93,7 @@ pub struct TraitPredicate { pub trait_ref: TraitRef, } -#[derive(PartialEq, Eq, Hash, Debug)] +#[derive(PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)] pub struct TraitRef { pub def_id: DefId, pub args: GenericArgs, @@ -182,6 +182,20 @@ pub enum TyKind { CoroutineWitness(DefId, GenericArgs), Alias(AliasKind, AliasTy), RawPtr(Ty, Mutability), + TraitObject(List, Region, TraitObjectSyntax), +} + +#[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub struct PolyTraitRef { + pub bound_generic_params: List, + pub trait_ref: TraitRef, +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum TraitObjectSyntax { + Dyn, + DynStar, + None, } #[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] @@ -630,6 +644,14 @@ impl Ty { TyKind::Param(param).intern() } + pub fn mk_trait_object( + poly_traits: impl Into>, + r: Region, + syn: TraitObjectSyntax, + ) -> Ty { + TyKind::TraitObject(poly_traits.into(), r, syn).intern() + } + pub fn mk_ref(region: Region, ty: Ty, mutability: Mutability) -> Ty { TyKind::Ref(region, ty, mutability).intern() } @@ -721,13 +743,14 @@ impl Ty { TyKind::Coroutine(_, _) => todo!(), TyKind::CoroutineWitness(_, _) => todo!(), TyKind::Alias(_, _) => todo!(), + TyKind::TraitObject(_, _, _) => todo!(), }; rustc_ty::Ty::new(tcx, kind) } } impl_internable!(TyS, AdtDefData); -impl_slice_internable!(Ty, GenericArg, GenericParamDef, BoundVariableKind, Clause); +impl_slice_internable!(Ty, GenericArg, GenericParamDef, BoundVariableKind, Clause, PolyTraitRef); impl fmt::Debug for GenericArg { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { @@ -836,6 +859,9 @@ impl fmt::Debug for Ty { write!(f, ")")?; Ok(()) } + TyKind::TraitObject(poly_traits, _r, _syn) => { + write!(f, "dyn {poly_traits:?}") + } } } } diff --git a/crates/flux-middle/src/rustc/ty/subst.rs b/crates/flux-middle/src/rustc/ty/subst.rs index 90222d449c..9708c4ac2a 100644 --- a/crates/flux-middle/src/rustc/ty/subst.rs +++ b/crates/flux-middle/src/rustc/ty/subst.rs @@ -1,5 +1,8 @@ use super::{Binder, Const, ConstKind, FnSig, GenericArg, Region, Ty, TyKind}; -use crate::intern::{Internable, List}; +use crate::{ + intern::{Internable, List}, + rustc::ty::{PolyTraitRef, TraitRef}, +}; pub(super) trait Subst { fn subst(&self, args: &[GenericArg]) -> Self; @@ -40,6 +43,9 @@ impl Subst for Ty { TyKind::RawPtr(ty, mutbl) => Ty::mk_raw_ptr(ty.subst(args), *mutbl), TyKind::Param(param_ty) => args[param_ty.index as usize].expect_type().clone(), TyKind::FnPtr(fn_sig) => Ty::mk_fn_ptr(fn_sig.subst(args)), + TyKind::TraitObject(poly_trait_refs, re, syn) => { + Ty::mk_trait_object(poly_trait_refs.subst(args), *re, *syn) + } TyKind::Bool | TyKind::Uint(_) | TyKind::Str @@ -51,6 +57,20 @@ impl Subst for Ty { } } +impl Subst for TraitRef { + fn subst(&self, args: &[GenericArg]) -> Self { + let def_id = self.def_id; + TraitRef { def_id, args: self.args.subst(args) } + } +} + +impl Subst for PolyTraitRef { + fn subst(&self, args: &[GenericArg]) -> Self { + assert!(self.bound_generic_params.is_empty()); + PolyTraitRef { trait_ref: self.trait_ref.subst(args), bound_generic_params: List::empty() } + } +} + impl Subst for GenericArg { fn subst(&self, args: &[GenericArg]) -> Self { match self { From e763accbc659baf5cd9d984f7f715f3d6aec0ce4 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Mon, 22 Jul 2024 17:06:19 -0700 Subject: [PATCH 04/25] next: onto lower type --- crates/flux-middle/src/rustc/lowering.rs | 44 +++++++++++++++++++++--- 1 file changed, 39 insertions(+), 5 deletions(-) diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 7f95d1abba..72fd279f7e 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -26,8 +26,8 @@ use super::{ ty::{ AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind, Const, ConstKind, FieldDef, FnSig, GenericArg, GenericParamDef, GenericParamDefKind, - GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, TraitPredicate, TraitRef, Ty, - TypeOutlivesPredicate, VariantDef, + GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, PolyTraitRef, TraitObjectSyntax, + TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, }, }; use crate::{ @@ -741,9 +741,19 @@ pub(crate) fn lower_ty<'tcx>( Ok(Ty::mk_generator_witness(*did, args)) } rustc_ty::Dynamic(predicates, region, kind) => { - Err(UnsupportedReason::new(format!( - "DYN preds=`{predicates:?}`, reg={region:?}, kind={kind:?}" - ))) + let region = lower_region(region)?; + let kind = lower_dyn_kind(kind)?; + let poly_traits = List::from_vec( + predicates + .iter() + .map(|pred| lower_existential_predicate(tcx, pred)) + .try_collect()?, + ); + + Ok(Ty::mk_trait_object(poly_traits, region, kind)) + // Err(UnsupportedReason::new(format!( + // "DYN preds=`{predicates:?}`, reg={region:?}, kind={kind:?}" + // ))) } _ => Err(UnsupportedReason::new(format!("unsupported type `{ty:?}`"))), } @@ -777,6 +787,23 @@ fn lower_field(f: &rustc_ty::FieldDef) -> FieldDef { FieldDef { did: f.did, name: f.name } } +pub fn lower_existential_predicate<'tcx>( + tcx: TyCtxt<'tcx>, + pred: rustc_ty::Binder>, +) -> Result { + assert!(pred.bound_vars().is_empty()); + let pred = pred.skip_binder(); + let bound_generic_params = List::empty(); + if let rustc_ty::ExistentialPredicate::Trait(trait_ref) = pred { + let def_id = trait_ref.def_id; + let args = lower_generic_args(tcx, trait_ref.args)?; + let trait_ref = TraitRef { def_id, args }; + Ok(PolyTraitRef { bound_generic_params, trait_ref }) + } else { + Err(UnsupportedReason::new(format!("unsupported existential predicate `{pred:?}`"))) + } +} + pub fn lower_generic_args<'tcx>( tcx: TyCtxt<'tcx>, args: rustc_middle::ty::GenericArgsRef<'tcx>, @@ -799,6 +826,13 @@ fn lower_generic_arg<'tcx>( } } +fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { + match kind { + rustc_ty::DynKind::Dyn => Ok(TraitObjectSyntax::Dyn), + rustc_ty::DynKind::DynStar => Ok(TraitObjectSyntax::DynStar), + } +} + fn lower_region(region: &rustc_middle::ty::Region) -> Result { use rustc_middle::ty::RegionKind; match region.kind() { From d3af0039d3735ec53c4ae5e5f2a635dacad008cb Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 10:17:36 -0700 Subject: [PATCH 05/25] next: into constraint_gen --- .../flux-fhir-analysis/src/conv/fill_holes.rs | 12 +++++++ crates/flux-refineck/src/checker.rs | 31 ++++++++++++++----- 2 files changed, 36 insertions(+), 7 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/fill_holes.rs b/crates/flux-fhir-analysis/src/conv/fill_holes.rs index 4738ef6a44..17bb9e3f58 100644 --- a/crates/flux-fhir-analysis/src/conv/fill_holes.rs +++ b/crates/flux-fhir-analysis/src/conv/fill_holes.rs @@ -216,6 +216,18 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { (rty::BaseTy::Param(pty_a), ty::TyKind::Param(pty_b)) => { debug_assert_eq!(pty_a, pty_b); } + ( + rty::BaseTy::TraitObject(poly_trait_refs, re_a, _), + ty::TyKind::TraitObject(poly_trait_refs_b, re_b, _), + ) => { + self.zip_region(re_a, re_b); + debug_assert_eq!(poly_trait_refs.len(), poly_trait_refs_b.len()); + // for (poly_trait_ref_a, poly_trait_ref_b) in + // iter::zip(poly_trait_refs, poly_trait_refs_b) + // { + // self.zip_poly_trait_ref(poly_trait_ref_a, poly_trait_ref_b)?; + // } + } (rty::BaseTy::Closure(..), _) => { bug!("unexpected closure {a:?}"); } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 69f90e46dc..93df10e54a 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -960,18 +960,35 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { } } // &mut [T; n] -> &mut [T][n] and &[T; n] -> &[T][n] + // if let TyKind::Indexed(BaseTy::Ref(_, src_ty, src_mut), _) = from_kind + // && let TyKind::Indexed(BaseTy::Array(src_arr_ty, src_n), _) = src_ty.kind() + // && let rustc::ty::TyKind::Ref(dst_re, dst_ty, dst_mut) = to_kind + // && let rustc::ty::TyKind::Slice(_) = dst_ty.kind() + // && src_mut == dst_mut CastKind::Pointer(mir::PointerCast::Unsize) => { if let TyKind::Indexed(BaseTy::Ref(_, src_ty, src_mut), _) = from.kind() - && let TyKind::Indexed(BaseTy::Array(src_arr_ty, src_n), _) = src_ty.kind() + && let TyKind::Indexed(src_base_ty, _) = src_ty.kind() && let rustc::ty::TyKind::Ref(dst_re, dst_ty, dst_mut) = to.kind() - && let rustc::ty::TyKind::Slice(_) = dst_ty.kind() - && src_mut == dst_mut { - let idx = Expr::from_const(self.genv.tcx(), src_n); - let dst_slice = Ty::indexed(BaseTy::Slice(src_arr_ty.clone()), idx); - Ty::mk_ref(*dst_re, dst_slice, *dst_mut) + // &mut [T; n] -> &mut [T][n] and &[T; n] -> &[T][n] + if let rustc::ty::TyKind::Slice(_) = dst_ty.kind() + && let BaseTy::Array(src_arr_ty, src_n) = src_base_ty + && src_mut == dst_mut + { + let idx = Expr::from_const(self.genv.tcx(), src_n); + let dst_slice = Ty::indexed(BaseTy::Slice(src_arr_ty.clone()), idx); + Ty::mk_ref(*dst_re, dst_slice, *dst_mut) + } else + // &T -> & dyn U + if let rustc::ty::TyKind::TraitObject(_, _, _) = dst_ty.kind() { + self.genv + .refine_default(&self.generics, to) + .with_span(self.body.span())? + } else { + tracked_span_bug!("unsupported Unsize cast: from {from:?} to {to:?}") + } } else { - tracked_span_bug!("unsupported Unsize cast") + tracked_span_bug!("unsupported Unsize cast: from {from:?} to {to:?}") } } CastKind::FloatToInt From 961aa8d49eb72c16b56d4a668348fb65572da222 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 10:26:40 -0700 Subject: [PATCH 06/25] next: into constraint_gen --- tests/tests/todo/dyn00.rs | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 tests/tests/todo/dyn00.rs diff --git a/tests/tests/todo/dyn00.rs b/tests/tests/todo/dyn00.rs new file mode 100644 index 0000000000..4c46a48765 --- /dev/null +++ b/tests/tests/todo/dyn00.rs @@ -0,0 +1,24 @@ +#![allow(unused)] + +trait Animal { + fn noise(&self); +} + +struct Cow {} + +impl Animal for Cow { + fn noise(&self) { + println!("moooooo!"); + } +} + +#[flux::trusted] +fn make_two_noises(animal: &dyn Animal) { + animal.noise(); + animal.noise(); +} + +fn main() { + let cow = Cow {}; + make_two_noises(&cow); +} From 942704a75b65d2bdbdff98a6c9a0607a34b069e1 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 10:29:01 -0700 Subject: [PATCH 07/25] yay, dyn00 works (doesn't keel over) --- crates/flux-refineck/src/checker.rs | 6 ------ crates/flux-refineck/src/constraint_gen.rs | 3 ++- 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 93df10e54a..116aa76dfd 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -959,12 +959,6 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { } } } - // &mut [T; n] -> &mut [T][n] and &[T; n] -> &[T][n] - // if let TyKind::Indexed(BaseTy::Ref(_, src_ty, src_mut), _) = from_kind - // && let TyKind::Indexed(BaseTy::Array(src_arr_ty, src_n), _) = src_ty.kind() - // && let rustc::ty::TyKind::Ref(dst_re, dst_ty, dst_mut) = to_kind - // && let rustc::ty::TyKind::Slice(_) = dst_ty.kind() - // && src_mut == dst_mut CastKind::Pointer(mir::PointerCast::Unsize) => { if let TyKind::Indexed(BaseTy::Ref(_, src_ty, src_mut), _) = from.kind() && let TyKind::Indexed(src_base_ty, _) = src_ty.kind() diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 615da96d95..6911f364c5 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -583,7 +583,8 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { (BaseTy::Bool, BaseTy::Bool) | (BaseTy::Str, BaseTy::Str) | (BaseTy::Char, BaseTy::Char) - | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) => Ok(()), + | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) + | (BaseTy::TraitObject(_, _, _), BaseTy::TraitObject(_, _, _)) => Ok(()), (BaseTy::Closure(did1, tys1), BaseTy::Closure(did2, tys2)) if did1 == did2 => { debug_assert_eq!(tys1.len(), tys2.len()); for (ty1, ty2) in iter::zip(tys1, tys2) { From 1e4f71c64b6bac2deec40ba8160cef216d98e95e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 10:35:54 -0700 Subject: [PATCH 08/25] yay, dyn00 works (doesn't keel over) --- tests/tests/{todo => pos/surface}/dyn00.rs | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename tests/tests/{todo => pos/surface}/dyn00.rs (100%) diff --git a/tests/tests/todo/dyn00.rs b/tests/tests/pos/surface/dyn00.rs similarity index 100% rename from tests/tests/todo/dyn00.rs rename to tests/tests/pos/surface/dyn00.rs From 64650cee5f36696ade3089de577b967aac549c76 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 10:56:25 -0700 Subject: [PATCH 09/25] yay, dyn01 checks/fails as expected --- tests/tests/neg/surface/dyn01.rs | 36 ++++++++++++++++++++++++++++++++ tests/tests/pos/surface/dyn00.rs | 1 - 2 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 tests/tests/neg/surface/dyn01.rs diff --git a/tests/tests/neg/surface/dyn01.rs b/tests/tests/neg/surface/dyn01.rs new file mode 100644 index 0000000000..f821ed0ed3 --- /dev/null +++ b/tests/tests/neg/surface/dyn01.rs @@ -0,0 +1,36 @@ +#![allow(unused)] + +// ------------------------------------------------------ + +trait Shape { + #[flux::sig(fn(self: _) -> i32{v: 0 <= v})] + fn vertices(&self) -> i32; +} + +// ------------------------------------------------------ + +struct Circle {} + +impl Shape for Circle { + fn vertices(&self) -> i32 { + 0 + } +} + +// ------------------------------------------------------ + +#[flux::sig(fn(shape: _) -> i32{v: 0 <= v})] +fn count(shape: &dyn Shape) -> i32 { + shape.vertices() +} + +#[flux::sig(fn(shape: _) -> i32{v: 10 <= v})] +fn count_bad(shape: &dyn Shape) -> i32 { + shape.vertices() //~ ERROR: refinement type +} + +fn main() { + let c = Circle {}; + count(&c); + count_bad(&c); +} diff --git a/tests/tests/pos/surface/dyn00.rs b/tests/tests/pos/surface/dyn00.rs index 4c46a48765..6be59a67dd 100644 --- a/tests/tests/pos/surface/dyn00.rs +++ b/tests/tests/pos/surface/dyn00.rs @@ -12,7 +12,6 @@ impl Animal for Cow { } } -#[flux::trusted] fn make_two_noises(animal: &dyn Animal) { animal.noise(); animal.noise(); From 23c745369bec99cf6bee49dd84c8547fbeac39bc Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 11:06:29 -0700 Subject: [PATCH 10/25] clippy --- crates/flux-fhir-analysis/src/conv/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 3b1ce10d92..6b9748e038 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -441,7 +441,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let trait_segment = poly_trait_ref.trait_ref.last_segment(); if !poly_trait_ref.bound_generic_params.is_empty() || !trait_segment.args.is_empty() { - bug!("unexpected! conv_poly_dyn_trait_ref") + bug!("unexpected! conv_poly_dyn_trait_ref"); } let trait_ref = From 886ad1eb3576418cbf52117f0c6b44d7a990609e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 15:43:37 -0700 Subject: [PATCH 11/25] update pseudocode in README --- crates/flux-fhir-analysis/src/conv/mod.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 6b9748e038..ce8fdb70ff 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -440,8 +440,11 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { ) -> QueryResult { let trait_segment = poly_trait_ref.trait_ref.last_segment(); - if !poly_trait_ref.bound_generic_params.is_empty() || !trait_segment.args.is_empty() { - bug!("unexpected! conv_poly_dyn_trait_ref"); + if !poly_trait_ref.bound_generic_params.is_empty() { + bug!("unexpected! conv_poly_dyn_trait_ref {:?}", poly_trait_ref.bound_generic_params); + } + if !trait_segment.args.is_empty() { + bug!("unexpected! conv_poly_dyn_trait_ref {:?}", trait_segment.args); } let trait_ref = From 8ed155c91dcdb6cfceef524486a2ce1c81d85794 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 16:19:20 -0700 Subject: [PATCH 12/25] allow region vars in dyn --- crates/flux-fhir-analysis/src/conv/mod.rs | 61 +++++++++++++++-------- tests/tests/pos/surface/dyn03.rs | 11 ++++ 2 files changed, 50 insertions(+), 22 deletions(-) create mode 100644 tests/tests/pos/surface/dyn03.rs diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index ce8fdb70ff..5bdf62c77c 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -9,7 +9,6 @@ //! 3. Refinements are well-sorted. mod fill_holes; - use std::{borrow::Borrow, iter}; use flux_common::{bug, iter::IterExt, span_bug}; @@ -24,7 +23,10 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc::{self, ty::TraitObjectSyntax}, + rustc::{ + self, + ty::{Region, TraitObjectSyntax}, + }, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -35,7 +37,7 @@ use rustc_hir::{ }; use rustc_middle::{ middle::resolve_bound_vars::ResolvedArg, - ty::{self, AssocItem, AssocKind, BoundVar}, + ty::{self, AssocItem, AssocKind, BoundVar, EarlyParamRegion}, }; use rustc_span::{ symbol::{kw, Ident}, @@ -436,19 +438,25 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { } fn conv_poly_trait_ref_dyn( + &mut self, + env: &mut Env, poly_trait_ref: &fhir::PolyTraitRef, ) -> QueryResult { let trait_segment = poly_trait_ref.trait_ref.last_segment(); if !poly_trait_ref.bound_generic_params.is_empty() { - bug!("unexpected! conv_poly_dyn_trait_ref {:?}", poly_trait_ref.bound_generic_params); - } - if !trait_segment.args.is_empty() { - bug!("unexpected! conv_poly_dyn_trait_ref {:?}", trait_segment.args); + bug!( + "unexpected! conv_poly_dyn_trait_ref bound_generic_params={:?}", + poly_trait_ref.bound_generic_params + ); } + // if !trait_segment.args.is_empty() { + // bug!("unexpected! conv_poly_dyn_trait_ref args={:?}", trait_segment.args); + // } - let trait_ref = - rty::TraitRef { def_id: poly_trait_ref.trait_def_id(), args: List::empty() }; + let def_id = poly_trait_ref.trait_def_id(); + let args = self.conv_generic_args(env, def_id, trait_segment.args)?; + let trait_ref = rty::TraitRef { def_id, args: args.into() }; Ok(rty::PolyTraitRef { trait_ref, bound_generic_params: List::empty() }) } @@ -808,7 +816,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { fhir::TyKind::TraitObject(poly_traits, lft, syn) => { let poly_traits: List = poly_traits .iter() - .map(|poly_trait| Self::conv_poly_trait_ref_dyn(poly_trait)) + .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) .try_collect()?; let region = self.conv_lifetime(env, *lft); let syn = Self::conv_trait_object_syntax(syn); @@ -1182,20 +1190,29 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { ) -> QueryResult { let generics = self.genv.generics_of(def_id)?; for param in generics.params.iter().skip(into.len()) { - if let rty::GenericParamDefKind::Type { has_default } = param.kind { - debug_assert!(has_default); - let tcx = self.genv.tcx(); - let ty = self - .genv - .type_of(param.def_id)? - .instantiate(tcx, into, &[]) - .to_ty(); - into.push(rty::GenericArg::Ty(ty)); - } else { - bug!("unexpected generic param: {param:?}"); + match param.kind { + rty::GenericParamDefKind::Type { has_default } => { + debug_assert!(has_default); + let tcx = self.genv.tcx(); + let ty = self + .genv + .type_of(param.def_id)? + .instantiate(tcx, into, &[]) + .to_ty(); + into.push(rty::GenericArg::Ty(ty)); + } + rty::GenericParamDefKind::Lifetime => { + let region = Region::ReEarlyParam(EarlyParamRegion { + index: param.index, + name: param.name, + }); + into.push(rty::GenericArg::Lifetime(region)); + } + _ => { + bug!("unexpected generic param: {param:?}"); + } } } - Ok(()) } diff --git a/tests/tests/pos/surface/dyn03.rs b/tests/tests/pos/surface/dyn03.rs new file mode 100644 index 0000000000..e24b9c931f --- /dev/null +++ b/tests/tests/pos/surface/dyn03.rs @@ -0,0 +1,11 @@ +#![allow(dead_code)] + +pub struct Cow {} + +pub trait CowContainer<'apple> { + fn get_cow(&self) -> &'apple Cow; +} + +pub struct CowCell<'banana> { + inner: &'banana dyn CowContainer<'banana>, +} From 193032b0b87fca07c2c721452ecfcbeec344924b Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 17:03:10 -0700 Subject: [PATCH 13/25] allow region vars in dyn --- crates/flux-fhir-analysis/src/conv/mod.rs | 15 ++++++++++----- tests/tests/pos/surface/dyn02.rs | 8 ++++++++ 2 files changed, 18 insertions(+), 5 deletions(-) create mode 100644 tests/tests/pos/surface/dyn02.rs diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 5bdf62c77c..1d6cd24c97 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -450,13 +450,17 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { poly_trait_ref.bound_generic_params ); } - // if !trait_segment.args.is_empty() { - // bug!("unexpected! conv_poly_dyn_trait_ref args={:?}", trait_segment.args); - // } + if !trait_segment.args.is_empty() { + bug!("unexpected! conv_poly_dyn_trait_ref args={:?}", trait_segment.args); + } let def_id = poly_trait_ref.trait_def_id(); - let args = self.conv_generic_args(env, def_id, trait_segment.args)?; - let trait_ref = rty::TraitRef { def_id, args: args.into() }; + + let mut into = vec![]; + self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; + // let args = self.conv_generic_args(env, def_id, trait_segment.args)?; + + let trait_ref = rty::TraitRef { def_id, args: into.into() }; Ok(rty::PolyTraitRef { trait_ref, bound_generic_params: List::empty() }) } @@ -1192,6 +1196,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { for param in generics.params.iter().skip(into.len()) { match param.kind { rty::GenericParamDefKind::Type { has_default } => { + // println!("TRACE: fill_generic_args_defaults: {def_id:?} param = {:?}", param); debug_assert!(has_default); let tcx = self.genv.tcx(); let ty = self diff --git a/tests/tests/pos/surface/dyn02.rs b/tests/tests/pos/surface/dyn02.rs new file mode 100644 index 0000000000..fe0dd607c8 --- /dev/null +++ b/tests/tests/pos/surface/dyn02.rs @@ -0,0 +1,8 @@ +pub trait Animal { + fn noise(&self); +} + +#[flux::trusted] +pub fn get_animal() -> &'static dyn Animal { + unimplemented!() +} From cbeaf3bbd860923cba2b6f2a7792fa66e98c0dce Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 23 Jul 2024 17:05:41 -0700 Subject: [PATCH 14/25] allow region vars in dyn --- crates/flux-fhir-analysis/src/conv/mod.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 1d6cd24c97..951e78703b 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -450,15 +450,10 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { poly_trait_ref.bound_generic_params ); } - if !trait_segment.args.is_empty() { - bug!("unexpected! conv_poly_dyn_trait_ref args={:?}", trait_segment.args); - } let def_id = poly_trait_ref.trait_def_id(); - let mut into = vec![]; self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; - // let args = self.conv_generic_args(env, def_id, trait_segment.args)?; let trait_ref = rty::TraitRef { def_id, args: into.into() }; Ok(rty::PolyTraitRef { trait_ref, bound_generic_params: List::empty() }) From eacee3ccfd5c5364c181f7430175b38b40e6c641 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jul 2024 09:43:05 -0700 Subject: [PATCH 15/25] Update crates/flux-middle/src/fhir/lift.rs Co-authored-by: Nico Lehmann --- crates/flux-middle/src/fhir/lift.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index 3ee5de5f6e..297a2f2d02 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -401,7 +401,6 @@ impl<'a, 'genv, 'tcx> LiftCtxt<'a, 'genv, 'tcx> { let lft = self.lift_lifetime(lft)?; fhir::TyKind::TraitObject(poly_traits, lft, syntax) - // return self.emit_unsupported(&format!("unsupported type: {ty:#?}",)); } _ => { return self.emit_unsupported(&format!( From e80341974575b68ed7260fa2e2d230465ebb859f Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jul 2024 11:57:07 -0700 Subject: [PATCH 16/25] use Dynamic instead of PolyTraitRef --- .../flux-fhir-analysis/src/conv/fill_holes.rs | 9 +--- crates/flux-fhir-analysis/src/conv/mod.rs | 27 ++++++----- crates/flux-middle/src/fhir/lift.rs | 1 - crates/flux-middle/src/rty/fold.rs | 46 +++++++++++++------ crates/flux-middle/src/rty/mod.rs | 34 ++++++++------ crates/flux-middle/src/rty/pretty.rs | 21 ++++----- crates/flux-middle/src/rty/refining.rs | 38 ++++++++++----- crates/flux-middle/src/rustc/lowering.rs | 38 ++++++++------- crates/flux-middle/src/rustc/ty.rs | 41 +++++++++++------ crates/flux-middle/src/rustc/ty/subst.rs | 27 +++++++---- crates/flux-refineck/src/checker.rs | 2 +- crates/flux-refineck/src/constraint_gen.rs | 2 +- crates/flux-refineck/src/type_env.rs | 2 +- 13 files changed, 169 insertions(+), 119 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/fill_holes.rs b/crates/flux-fhir-analysis/src/conv/fill_holes.rs index 17bb9e3f58..bdbda23cd3 100644 --- a/crates/flux-fhir-analysis/src/conv/fill_holes.rs +++ b/crates/flux-fhir-analysis/src/conv/fill_holes.rs @@ -217,16 +217,11 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { debug_assert_eq!(pty_a, pty_b); } ( - rty::BaseTy::TraitObject(poly_trait_refs, re_a, _), - ty::TyKind::TraitObject(poly_trait_refs_b, re_b, _), + rty::BaseTy::Dynamic(poly_trait_refs, re_a, _), + ty::TyKind::Dynamic(poly_trait_refs_b, re_b, _), ) => { self.zip_region(re_a, re_b); debug_assert_eq!(poly_trait_refs.len(), poly_trait_refs_b.len()); - // for (poly_trait_ref_a, poly_trait_ref_b) in - // iter::zip(poly_trait_refs, poly_trait_refs_b) - // { - // self.zip_poly_trait_ref(poly_trait_ref_a, poly_trait_ref_b)?; - // } } (rty::BaseTy::Closure(..), _) => { bug!("unexpected closure {a:?}"); diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 951e78703b..a9babcf1bb 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -11,7 +11,7 @@ mod fill_holes; use std::{borrow::Borrow, iter}; -use flux_common::{bug, iter::IterExt, span_bug}; +use flux_common::{bug, iter::IterExt, span_bug, tracked_span_bug}; use flux_middle::{ fhir::{self, ExprRes, FhirId, FluxOwnerId}, global_env::GlobalEnv, @@ -25,7 +25,7 @@ use flux_middle::{ }, rustc::{ self, - ty::{Region, TraitObjectSyntax}, + ty::{DynKind, Region}, }, }; use itertools::Itertools; @@ -441,7 +441,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { &mut self, env: &mut Env, poly_trait_ref: &fhir::PolyTraitRef, - ) -> QueryResult { + ) -> QueryResult> { let trait_segment = poly_trait_ref.trait_ref.last_segment(); if !poly_trait_ref.bound_generic_params.is_empty() { @@ -455,8 +455,9 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let mut into = vec![]; self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; - let trait_ref = rty::TraitRef { def_id, args: into.into() }; - Ok(rty::PolyTraitRef { trait_ref, bound_generic_params: List::empty() }) + let exi_trait_ref = rty::ExistentialTraitRef { def_id, args: into.into() }; + let exi_pred = rty::ExistentialPredicate::Trait(exi_trait_ref); + Ok(rty::Binder::new(exi_pred, List::empty())) } /// Converts a `T: Trait` bound @@ -813,22 +814,24 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { Ok(rty::Ty::alias(rty::AliasKind::Opaque, alias_ty)) } fhir::TyKind::TraitObject(poly_traits, lft, syn) => { - let poly_traits: List = poly_traits + let exi_preds: List<_> = poly_traits .iter() .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) .try_collect()?; let region = self.conv_lifetime(env, *lft); - let syn = Self::conv_trait_object_syntax(syn); - Ok(rty::Ty::trait_object(poly_traits, region, syn)) + let kind = Self::conv_trait_object_syntax(syn); + Ok(rty::Ty::dynamic(exi_preds, region, kind)) } } } - fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> TraitObjectSyntax { + fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> DynKind { match syn { - rustc_ast::TraitObjectSyntax::Dyn => TraitObjectSyntax::Dyn, - rustc_ast::TraitObjectSyntax::DynStar => TraitObjectSyntax::DynStar, - rustc_ast::TraitObjectSyntax::None => TraitObjectSyntax::None, + rustc_ast::TraitObjectSyntax::Dyn => DynKind::Dyn, + rustc_ast::TraitObjectSyntax::None => DynKind::None, + rustc_ast::TraitObjectSyntax::DynStar => { + tracked_span_bug!("dyn* traits not supported yet") + } } } diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index 3ee5de5f6e..297a2f2d02 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -401,7 +401,6 @@ impl<'a, 'genv, 'tcx> LiftCtxt<'a, 'genv, 'tcx> { let lft = self.lift_lifetime(lft)?; fhir::TyKind::TraitObject(poly_traits, lft, syntax) - // return self.emit_unsupported(&format!("unsupported type: {ty:#?}",)); } _ => { return self.emit_unsupported(&format!( diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index baf3e401a1..6068779b74 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -15,10 +15,10 @@ use super::{ projections, subst::EVarSubstFolder, AliasReft, AliasTy, BaseTy, BinOp, Binder, BoundVariableKind, Clause, ClauseKind, Const, - CoroutineObligPredicate, Ensures, Expr, ExprKind, FnOutput, FnSig, FnTraitPredicate, FuncSort, - GenericArg, Invariant, KVar, Lambda, Name, Opaqueness, OutlivesPredicate, PolyFuncSort, - PolyTraitRef, ProjectionPredicate, PtrKind, Qualifier, ReBound, Region, Sort, SubsetTy, - TraitPredicate, TraitRef, Ty, TyKind, + CoroutineObligPredicate, Ensures, ExistentialPredicate, ExistentialTraitRef, Expr, ExprKind, + FnOutput, FnSig, FnTraitPredicate, FuncSort, GenericArg, Invariant, KVar, Lambda, Name, + Opaqueness, OutlivesPredicate, PolyFuncSort, ProjectionPredicate, PtrKind, Qualifier, ReBound, + Region, Sort, SubsetTy, TraitPredicate, TraitRef, Ty, TyKind, }; use crate::{ global_env::GlobalEnv, @@ -488,18 +488,34 @@ impl TypeFoldable for TraitRef { } } -impl TypeVisitable for PolyTraitRef { +impl TypeVisitable for ExistentialTraitRef { fn visit_with(&self, visitor: &mut V) -> ControlFlow { - self.trait_ref.visit_with(visitor) + self.args.visit_with(visitor) } } -impl TypeFoldable for PolyTraitRef { +impl TypeFoldable for ExistentialTraitRef { fn try_fold_with(&self, folder: &mut F) -> Result { - Ok(PolyTraitRef { - bound_generic_params: self.bound_generic_params.clone(), - trait_ref: self.trait_ref.try_fold_with(folder)?, - }) + Ok(ExistentialTraitRef { def_id: self.def_id, args: self.args.try_fold_with(folder)? }) + } +} + +impl TypeVisitable for ExistentialPredicate { + fn visit_with(&self, visitor: &mut V) -> ControlFlow { + match self { + ExistentialPredicate::Trait(exi_trait_ref) => exi_trait_ref.visit_with(visitor), + } + } +} + +impl TypeFoldable for ExistentialPredicate { + fn try_fold_with(&self, folder: &mut F) -> Result { + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + let exi_trait_ref = exi_trait_ref.try_fold_with(folder)?; + Ok(ExistentialPredicate::Trait(exi_trait_ref)) + } + } } } @@ -955,7 +971,7 @@ impl TypeSuperVisitable for BaseTy { | BaseTy::Closure(_, _) | BaseTy::Never | BaseTy::Param(_) => ControlFlow::Continue(()), - BaseTy::TraitObject(poly_traits, _, _) => poly_traits.visit_with(visitor), + BaseTy::Dynamic(exi_preds, _, _) => exi_preds.visit_with(visitor), } } } @@ -995,9 +1011,9 @@ impl TypeSuperFoldable for BaseTy { args.try_fold_with(folder)?, ) } - BaseTy::TraitObject(poly_traits, region, syn) => { - BaseTy::TraitObject( - poly_traits.try_fold_with(folder)?, + BaseTy::Dynamic(exi_preds, region, syn) => { + BaseTy::Dynamic( + exi_preds.try_fold_with(folder)?, region.try_fold_with(folder)?, *syn, ) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 5fd35f8470..a0161a3417 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -60,7 +60,7 @@ use crate::{ rustc::{ self, mir::Place, - ty::{TraitObjectSyntax, VariantDef}, + ty::{DynKind, VariantDef}, }, }; @@ -239,12 +239,16 @@ pub struct PolyTraitRef { pub trait_ref: TraitRef, } -// #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -// pub enum TraitObjectSyntax { -// Dyn, -// DynStar, -// None, -// } +#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum ExistentialPredicate { + Trait(ExistentialTraitRef), +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub struct ExistentialTraitRef { + pub def_id: DefId, + pub args: GenericArgs, +} #[derive(PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable)] pub struct ProjectionPredicate { @@ -638,12 +642,12 @@ impl Ty { Self::alias(AliasKind::Projection, alias_ty) } - pub fn trait_object( - poly_traits: impl Into>, + pub fn dynamic( + preds: impl Into>>, region: Region, - syn: TraitObjectSyntax, + kind: DynKind, ) -> Ty { - BaseTy::TraitObject(poly_traits.into(), region, syn).to_ty() + BaseTy::Dynamic(preds.into(), region, kind).to_ty() } pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty { @@ -975,7 +979,7 @@ pub enum BaseTy { Never, Closure(DefId, /* upvar_tys */ List), Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List), - TraitObject(List, Region, TraitObjectSyntax), + Dynamic(List>, Region, DynKind), Param(ParamTy), } @@ -1124,7 +1128,7 @@ impl BaseTy { | BaseTy::Array(_, _) | BaseTy::Closure(_, _) | BaseTy::Coroutine(..) - | BaseTy::TraitObject(_, _, _) + | BaseTy::Dynamic(_, _, _) | BaseTy::Never => Sort::unit(), } } @@ -1157,7 +1161,7 @@ impl BaseTy { BaseTy::Array(_, _) => todo!(), BaseTy::Never => tcx.types.never, BaseTy::Closure(_, _) => todo!(), - BaseTy::TraitObject(_, _, _) => todo!(), + BaseTy::Dynamic(_, _, _) => todo!(), BaseTy::Coroutine(def_id, resume_ty, upvars) => { todo!("Generator {def_id:?} {resume_ty:?} {upvars:?}") // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg)); @@ -2083,7 +2087,7 @@ impl_slice_internable!( Sort, GenericParamDef, TraitRef, - PolyTraitRef, + Binder, Clause, PolyVariant, Invariant, diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index e5911b395a..c21cf698f7 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -337,15 +337,14 @@ impl Pretty for List { } } -impl Pretty for PolyTraitRef { - fn fmt(&self, cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { - define_scoped!(cx, f); - // let vars = &self.bound_generic_params; - // TODO - // if !vars.is_empty() { - // w!("for <{:?}>", join!(", ", vars)) - // } - w!("{:?}", &self.trait_ref.def_id) +impl Pretty for ExistentialPredicate { + fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result { + define_scoped!(_cx, f); + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + w!("{exi_trait_ref:?}") + } + } } } @@ -400,8 +399,8 @@ impl Pretty for BaseTy { } Ok(()) } - BaseTy::TraitObject(poly_traits, _, _) => { - w!("dyn {:?}", join!(", ", poly_traits)) + BaseTy::Dynamic(exi_preds, _, _) => { + w!("dyn {:?}", join!(", ", exi_preds)) } } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 290ddd383b..ca1fa51a77 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -6,7 +6,7 @@ use itertools::Itertools; use rustc_hir::def_id::DefId; use rustc_middle::ty::{ClosureKind, ParamTy}; -use super::{fold::TypeFoldable, PolyTraitRef}; +use super::fold::TypeFoldable; use crate::{ global_env::GlobalEnv, intern::List, @@ -170,14 +170,28 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { Ok(rty::ClauseKind::FnTrait(pred)) } - pub fn refine_poly_trait_ref( + pub fn refine_existential_predicate( &self, - poly_trait_ref: &rustc::ty::PolyTraitRef, - ) -> QueryResult { - assert!(poly_trait_ref.bound_generic_params.is_empty()); - let bound_generic_params = List::empty(); - let trait_ref = self.refine_trait_ref(&poly_trait_ref.trait_ref)?; - Ok(PolyTraitRef { bound_generic_params, trait_ref }) + exi_pred: &rustc::ty::Binder, + ) -> QueryResult> { + assert!(exi_pred.vars().is_empty()); + let exi_pred = match exi_pred.as_ref().skip_binder() { + rustc::ty::ExistentialPredicate::Trait(exi_trait_ref) => { + rty::ExistentialPredicate::Trait(self.refine_exi_trait_ref(&exi_trait_ref)?) + } + }; + Ok(rty::Binder::new(exi_pred, List::empty())) + } + + pub fn refine_exi_trait_ref( + &self, + exi_trait_ref: &rustc::ty::ExistentialTraitRef, + ) -> QueryResult { + let exi_trait_ref = rty::ExistentialTraitRef { + def_id: exi_trait_ref.def_id, + args: self.refine_generic_args(exi_trait_ref.def_id, &exi_trait_ref.args)?, + }; + Ok(exi_trait_ref) } pub fn refine_trait_ref(&self, trait_ref: &rustc::ty::TraitRef) -> QueryResult { @@ -368,12 +382,12 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::RawPtr(ty, mu) => { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } - rustc::ty::TyKind::TraitObject(poly_traits, r, syntax) => { - let poly_traits = poly_traits + rustc::ty::TyKind::Dynamic(exi_preds, r, kind) => { + let exi_preds = exi_preds .iter() - .map(|ty| self.refine_poly_trait_ref(ty)) + .map(|ty| self.refine_existential_predicate(ty)) .try_collect()?; - rty::BaseTy::TraitObject(poly_traits, *r, *syntax) + rty::BaseTy::Dynamic(exi_preds, *r, *kind) } }; Ok(TyOrBase::Base((self.refine)(bty))) diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 72fd279f7e..06301cc01c 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -25,15 +25,15 @@ use super::{ }, ty::{ AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind, - Const, ConstKind, FieldDef, FnSig, GenericArg, GenericParamDef, GenericParamDefKind, - GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, PolyTraitRef, TraitObjectSyntax, - TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, + Const, ConstKind, DynKind, ExistentialPredicate, FieldDef, FnSig, GenericArg, + GenericParamDef, GenericParamDefKind, GenericPredicates, Generics, OutlivesPredicate, + PolyFnSig, TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, }, }; use crate::{ const_eval::scalar_int_to_constant, intern::List, - rustc::ty::{AliasTy, ProjectionPredicate, Region}, + rustc::ty::{AliasTy, ExistentialTraitRef, ProjectionPredicate, Region}, }; pub struct LoweringCtxt<'a, 'sess, 'tcx> { @@ -743,17 +743,14 @@ pub(crate) fn lower_ty<'tcx>( rustc_ty::Dynamic(predicates, region, kind) => { let region = lower_region(region)?; let kind = lower_dyn_kind(kind)?; - let poly_traits = List::from_vec( + let exi_preds = List::from_vec( predicates .iter() .map(|pred| lower_existential_predicate(tcx, pred)) .try_collect()?, ); - Ok(Ty::mk_trait_object(poly_traits, region, kind)) - // Err(UnsupportedReason::new(format!( - // "DYN preds=`{predicates:?}`, reg={region:?}, kind={kind:?}" - // ))) + Ok(Ty::mk_dynamic(exi_preds, region, kind)) } _ => Err(UnsupportedReason::new(format!("unsupported type `{ty:?}`"))), } @@ -790,17 +787,16 @@ fn lower_field(f: &rustc_ty::FieldDef) -> FieldDef { pub fn lower_existential_predicate<'tcx>( tcx: TyCtxt<'tcx>, pred: rustc_ty::Binder>, -) -> Result { +) -> Result, UnsupportedReason> { assert!(pred.bound_vars().is_empty()); let pred = pred.skip_binder(); - let bound_generic_params = List::empty(); - if let rustc_ty::ExistentialPredicate::Trait(trait_ref) = pred { - let def_id = trait_ref.def_id; - let args = lower_generic_args(tcx, trait_ref.args)?; - let trait_ref = TraitRef { def_id, args }; - Ok(PolyTraitRef { bound_generic_params, trait_ref }) + if let rustc_ty::ExistentialPredicate::Trait(exi_trait_ref) = pred { + let def_id = exi_trait_ref.def_id; + let args = lower_generic_args(tcx, exi_trait_ref.args)?; + let exi_trait_ref = ExistentialTraitRef { def_id, args }; + Ok(Binder::bind_with_vars(ExistentialPredicate::Trait(exi_trait_ref), List::empty())) } else { - Err(UnsupportedReason::new(format!("unsupported existential predicate `{pred:?}`"))) + Err(UnsupportedReason::new(format!("Unsupported existential predicate `{pred:?}`"))) } } @@ -826,10 +822,12 @@ fn lower_generic_arg<'tcx>( } } -fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { +fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { match kind { - rustc_ty::DynKind::Dyn => Ok(TraitObjectSyntax::Dyn), - rustc_ty::DynKind::DynStar => Ok(TraitObjectSyntax::DynStar), + rustc_ty::DynKind::Dyn => Ok(DynKind::Dyn), + rustc_ty::DynKind::DynStar => { + Err(UnsupportedReason::new(format!("unsupported dyn kind `{kind:?}`"))) + } } } diff --git a/crates/flux-middle/src/rustc/ty.rs b/crates/flux-middle/src/rustc/ty.rs index 5560f8ca2b..3147e7e351 100644 --- a/crates/flux-middle/src/rustc/ty.rs +++ b/crates/flux-middle/src/rustc/ty.rs @@ -182,19 +182,23 @@ pub enum TyKind { CoroutineWitness(DefId, GenericArgs), Alias(AliasKind, AliasTy), RawPtr(Ty, Mutability), - TraitObject(List, Region, TraitObjectSyntax), + Dynamic(List>, Region, DynKind), } #[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub struct PolyTraitRef { - pub bound_generic_params: List, - pub trait_ref: TraitRef, +pub enum ExistentialPredicate { + Trait(ExistentialTraitRef), +} + +#[derive(PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)] +pub struct ExistentialTraitRef { + pub def_id: DefId, + pub args: GenericArgs, } -#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub enum TraitObjectSyntax { +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] +pub enum DynKind { Dyn, - DynStar, None, } @@ -644,12 +648,12 @@ impl Ty { TyKind::Param(param).intern() } - pub fn mk_trait_object( - poly_traits: impl Into>, + pub fn mk_dynamic( + exi_preds: impl Into>>, r: Region, - syn: TraitObjectSyntax, + kind: DynKind, ) -> Ty { - TyKind::TraitObject(poly_traits.into(), r, syn).intern() + TyKind::Dynamic(exi_preds.into(), r, kind).intern() } pub fn mk_ref(region: Region, ty: Ty, mutability: Mutability) -> Ty { @@ -743,14 +747,21 @@ impl Ty { TyKind::Coroutine(_, _) => todo!(), TyKind::CoroutineWitness(_, _) => todo!(), TyKind::Alias(_, _) => todo!(), - TyKind::TraitObject(_, _, _) => todo!(), + TyKind::Dynamic(_, _, _) => todo!(), }; rustc_ty::Ty::new(tcx, kind) } } impl_internable!(TyS, AdtDefData); -impl_slice_internable!(Ty, GenericArg, GenericParamDef, BoundVariableKind, Clause, PolyTraitRef); +impl_slice_internable!( + Ty, + GenericArg, + GenericParamDef, + BoundVariableKind, + Clause, + Binder, +); impl fmt::Debug for GenericArg { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { @@ -859,8 +870,8 @@ impl fmt::Debug for Ty { write!(f, ")")?; Ok(()) } - TyKind::TraitObject(poly_traits, _r, _syn) => { - write!(f, "dyn {poly_traits:?}") + TyKind::Dynamic(exi_preds, _r, _syn) => { + write!(f, "dyn {exi_preds:?}") } } } diff --git a/crates/flux-middle/src/rustc/ty/subst.rs b/crates/flux-middle/src/rustc/ty/subst.rs index 9708c4ac2a..b1c5be919c 100644 --- a/crates/flux-middle/src/rustc/ty/subst.rs +++ b/crates/flux-middle/src/rustc/ty/subst.rs @@ -1,7 +1,10 @@ -use super::{Binder, Const, ConstKind, FnSig, GenericArg, Region, Ty, TyKind}; +use super::{ + Binder, Const, ConstKind, ExistentialPredicate, ExistentialTraitRef, FnSig, GenericArg, Region, + Ty, TyKind, +}; use crate::{ intern::{Internable, List}, - rustc::ty::{PolyTraitRef, TraitRef}, + rustc::ty::TraitRef, }; pub(super) trait Subst { @@ -43,9 +46,7 @@ impl Subst for Ty { TyKind::RawPtr(ty, mutbl) => Ty::mk_raw_ptr(ty.subst(args), *mutbl), TyKind::Param(param_ty) => args[param_ty.index as usize].expect_type().clone(), TyKind::FnPtr(fn_sig) => Ty::mk_fn_ptr(fn_sig.subst(args)), - TyKind::TraitObject(poly_trait_refs, re, syn) => { - Ty::mk_trait_object(poly_trait_refs.subst(args), *re, *syn) - } + TyKind::Dynamic(exi_preds, re, syn) => Ty::mk_dynamic(exi_preds.subst(args), *re, *syn), TyKind::Bool | TyKind::Uint(_) | TyKind::Str @@ -64,10 +65,20 @@ impl Subst for TraitRef { } } -impl Subst for PolyTraitRef { +impl Subst for ExistentialTraitRef { + fn subst(&self, args: &[GenericArg]) -> Self { + let def_id = self.def_id; + ExistentialTraitRef { def_id, args: self.args.subst(args) } + } +} + +impl Subst for ExistentialPredicate { fn subst(&self, args: &[GenericArg]) -> Self { - assert!(self.bound_generic_params.is_empty()); - PolyTraitRef { trait_ref: self.trait_ref.subst(args), bound_generic_params: List::empty() } + match self { + ExistentialPredicate::Trait(exi_trait_ref) => { + ExistentialPredicate::Trait(exi_trait_ref.subst(args)) + } + } } } diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 116aa76dfd..49b92eac50 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -974,7 +974,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { Ty::mk_ref(*dst_re, dst_slice, *dst_mut) } else // &T -> & dyn U - if let rustc::ty::TyKind::TraitObject(_, _, _) = dst_ty.kind() { + if let rustc::ty::TyKind::Dynamic(_, _, _) = dst_ty.kind() { self.genv .refine_default(&self.generics, to) .with_span(self.body.span())? diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 6911f364c5..6fc97e01c4 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -584,7 +584,7 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { | (BaseTy::Str, BaseTy::Str) | (BaseTy::Char, BaseTy::Char) | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) - | (BaseTy::TraitObject(_, _, _), BaseTy::TraitObject(_, _, _)) => Ok(()), + | (BaseTy::Dynamic(_, _, _), BaseTy::Dynamic(_, _, _)) => Ok(()), (BaseTy::Closure(did1, tys1), BaseTy::Closure(did2, tys2)) if did1 == did2 => { debug_assert_eq!(tys1.len(), tys2.len()); for (ty1, ty2) in iter::zip(tys1, tys2) { diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index b930681b8c..1eecad36fe 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -373,7 +373,7 @@ impl BasicBlockEnvShape { | BaseTy::Char | BaseTy::Never | BaseTy::Closure(_, _) - | BaseTy::TraitObject(_, _, _) + | BaseTy::Dynamic(_, _, _) | BaseTy::Coroutine(..) => bty.clone(), } } From ae2dde81298d5f419b31fd7681ad21b2792a2faa Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jul 2024 12:05:02 -0700 Subject: [PATCH 17/25] use Dynamic instead of PolyTraitRef --- crates/flux-middle/src/rty/refining.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index ca1fa51a77..7314eba45e 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -177,7 +177,7 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { assert!(exi_pred.vars().is_empty()); let exi_pred = match exi_pred.as_ref().skip_binder() { rustc::ty::ExistentialPredicate::Trait(exi_trait_ref) => { - rty::ExistentialPredicate::Trait(self.refine_exi_trait_ref(&exi_trait_ref)?) + rty::ExistentialPredicate::Trait(self.refine_exi_trait_ref(exi_trait_ref)?) } }; Ok(rty::Binder::new(exi_pred, List::empty())) From 01c4724ccd3ab35ed2718e0f311f5c6bce746a2e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jul 2024 15:45:28 -0700 Subject: [PATCH 18/25] remove DynKind (only support Dyn) else panic --- .../flux-fhir-analysis/src/conv/fill_holes.rs | 4 +-- crates/flux-fhir-analysis/src/conv/mod.rs | 22 ++++----------- crates/flux-middle/src/rty/fold.rs | 10 ++----- crates/flux-middle/src/rty/mod.rs | 27 +++++++++--------- crates/flux-middle/src/rty/pretty.rs | 2 +- crates/flux-middle/src/rty/refining.rs | 4 +-- crates/flux-middle/src/rustc/lowering.rs | 28 +++++++++---------- crates/flux-middle/src/rustc/ty.rs | 20 ++++--------- crates/flux-middle/src/rustc/ty/subst.rs | 2 +- crates/flux-refineck/src/checker.rs | 2 +- crates/flux-refineck/src/constraint_gen.rs | 2 +- crates/flux-refineck/src/type_env.rs | 2 +- 12 files changed, 50 insertions(+), 75 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/fill_holes.rs b/crates/flux-fhir-analysis/src/conv/fill_holes.rs index bdbda23cd3..288ec0096a 100644 --- a/crates/flux-fhir-analysis/src/conv/fill_holes.rs +++ b/crates/flux-fhir-analysis/src/conv/fill_holes.rs @@ -217,8 +217,8 @@ impl<'genv, 'tcx> Zipper<'genv, 'tcx> { debug_assert_eq!(pty_a, pty_b); } ( - rty::BaseTy::Dynamic(poly_trait_refs, re_a, _), - ty::TyKind::Dynamic(poly_trait_refs_b, re_b, _), + rty::BaseTy::Dynamic(poly_trait_refs, re_a), + ty::TyKind::Dynamic(poly_trait_refs_b, re_b), ) => { self.zip_region(re_a, re_b); debug_assert_eq!(poly_trait_refs.len(), poly_trait_refs_b.len()); diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index a9babcf1bb..2126178b76 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -23,10 +23,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc::{ - self, - ty::{DynKind, Region}, - }, + rustc::{self, ty::Region}, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -819,18 +816,11 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) .try_collect()?; let region = self.conv_lifetime(env, *lft); - let kind = Self::conv_trait_object_syntax(syn); - Ok(rty::Ty::dynamic(exi_preds, region, kind)) - } - } - } - - fn conv_trait_object_syntax(syn: &rustc_ast::TraitObjectSyntax) -> DynKind { - match syn { - rustc_ast::TraitObjectSyntax::Dyn => DynKind::Dyn, - rustc_ast::TraitObjectSyntax::None => DynKind::None, - rustc_ast::TraitObjectSyntax::DynStar => { - tracked_span_bug!("dyn* traits not supported yet") + if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) { + Ok(rty::Ty::dynamic(exi_preds, region)) + } else { + tracked_span_bug!("dyn* traits not supported yet") + } } } } diff --git a/crates/flux-middle/src/rty/fold.rs b/crates/flux-middle/src/rty/fold.rs index 6068779b74..1b5088e3eb 100644 --- a/crates/flux-middle/src/rty/fold.rs +++ b/crates/flux-middle/src/rty/fold.rs @@ -971,7 +971,7 @@ impl TypeSuperVisitable for BaseTy { | BaseTy::Closure(_, _) | BaseTy::Never | BaseTy::Param(_) => ControlFlow::Continue(()), - BaseTy::Dynamic(exi_preds, _, _) => exi_preds.visit_with(visitor), + BaseTy::Dynamic(exi_preds, _) => exi_preds.visit_with(visitor), } } } @@ -1011,12 +1011,8 @@ impl TypeSuperFoldable for BaseTy { args.try_fold_with(folder)?, ) } - BaseTy::Dynamic(exi_preds, region, syn) => { - BaseTy::Dynamic( - exi_preds.try_fold_with(folder)?, - region.try_fold_with(folder)?, - *syn, - ) + BaseTy::Dynamic(exi_preds, region) => { + BaseTy::Dynamic(exi_preds.try_fold_with(folder)?, region.try_fold_with(folder)?) } }; Ok(bty) diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index a0161a3417..91032db79d 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -57,11 +57,7 @@ use crate::{ intern::{impl_internable, impl_slice_internable, Interned, List}, queries::QueryResult, rty::subst::SortSubst, - rustc::{ - self, - mir::Place, - ty::{DynKind, VariantDef}, - }, + rustc::{self, mir::Place, ty::VariantDef}, }; #[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)] @@ -642,12 +638,8 @@ impl Ty { Self::alias(AliasKind::Projection, alias_ty) } - pub fn dynamic( - preds: impl Into>>, - region: Region, - kind: DynKind, - ) -> Ty { - BaseTy::Dynamic(preds.into(), region, kind).to_ty() + pub fn dynamic(preds: impl Into>>, region: Region) -> Ty { + BaseTy::Dynamic(preds.into(), region).to_ty() } pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty { @@ -979,7 +971,7 @@ pub enum BaseTy { Never, Closure(DefId, /* upvar_tys */ List), Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List), - Dynamic(List>, Region, DynKind), + Dynamic(List>, Region), Param(ParamTy), } @@ -1128,7 +1120,7 @@ impl BaseTy { | BaseTy::Array(_, _) | BaseTy::Closure(_, _) | BaseTy::Coroutine(..) - | BaseTy::Dynamic(_, _, _) + | BaseTy::Dynamic(_, _) | BaseTy::Never => Sort::unit(), } } @@ -1161,7 +1153,14 @@ impl BaseTy { BaseTy::Array(_, _) => todo!(), BaseTy::Never => tcx.types.never, BaseTy::Closure(_, _) => todo!(), - BaseTy::Dynamic(_, _, _) => todo!(), + BaseTy::Dynamic(_exi_preds, _re) => { + todo!() + // let preds = exi_preds + // .iter() + // .map(|pred| pred.to_rustc(tcx)) + // .collect_vec(); + // ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx), rustc_middle::ty::DynKind::Dyn) + } BaseTy::Coroutine(def_id, resume_ty, upvars) => { todo!("Generator {def_id:?} {resume_ty:?} {upvars:?}") // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg)); diff --git a/crates/flux-middle/src/rty/pretty.rs b/crates/flux-middle/src/rty/pretty.rs index c21cf698f7..44a02bc0bc 100644 --- a/crates/flux-middle/src/rty/pretty.rs +++ b/crates/flux-middle/src/rty/pretty.rs @@ -399,7 +399,7 @@ impl Pretty for BaseTy { } Ok(()) } - BaseTy::Dynamic(exi_preds, _, _) => { + BaseTy::Dynamic(exi_preds, _) => { w!("dyn {:?}", join!(", ", exi_preds)) } } diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs index 7314eba45e..05b1056e66 100644 --- a/crates/flux-middle/src/rty/refining.rs +++ b/crates/flux-middle/src/rty/refining.rs @@ -382,12 +382,12 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> { rustc::ty::TyKind::RawPtr(ty, mu) => { rty::BaseTy::RawPtr(self.as_default().refine_ty(ty)?, *mu) } - rustc::ty::TyKind::Dynamic(exi_preds, r, kind) => { + rustc::ty::TyKind::Dynamic(exi_preds, r) => { let exi_preds = exi_preds .iter() .map(|ty| self.refine_existential_predicate(ty)) .try_collect()?; - rty::BaseTy::Dynamic(exi_preds, *r, *kind) + rty::BaseTy::Dynamic(exi_preds, *r) } }; Ok(TyOrBase::Base((self.refine)(bty))) diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 06301cc01c..0bcfe38370 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -25,9 +25,9 @@ use super::{ }, ty::{ AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind, - Const, ConstKind, DynKind, ExistentialPredicate, FieldDef, FnSig, GenericArg, - GenericParamDef, GenericParamDefKind, GenericPredicates, Generics, OutlivesPredicate, - PolyFnSig, TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, + Const, ConstKind, ExistentialPredicate, FieldDef, FnSig, GenericArg, GenericParamDef, + GenericParamDefKind, GenericPredicates, Generics, OutlivesPredicate, PolyFnSig, + TraitPredicate, TraitRef, Ty, TypeOutlivesPredicate, VariantDef, }, }; use crate::{ @@ -740,9 +740,9 @@ pub(crate) fn lower_ty<'tcx>( let args = lower_generic_args(tcx, args)?; Ok(Ty::mk_generator_witness(*did, args)) } - rustc_ty::Dynamic(predicates, region, kind) => { + rustc_ty::Dynamic(predicates, region, rustc_ty::DynKind::Dyn) => { let region = lower_region(region)?; - let kind = lower_dyn_kind(kind)?; + let exi_preds = List::from_vec( predicates .iter() @@ -750,7 +750,7 @@ pub(crate) fn lower_ty<'tcx>( .try_collect()?, ); - Ok(Ty::mk_dynamic(exi_preds, region, kind)) + Ok(Ty::mk_dynamic(exi_preds, region)) } _ => Err(UnsupportedReason::new(format!("unsupported type `{ty:?}`"))), } @@ -822,14 +822,14 @@ fn lower_generic_arg<'tcx>( } } -fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { - match kind { - rustc_ty::DynKind::Dyn => Ok(DynKind::Dyn), - rustc_ty::DynKind::DynStar => { - Err(UnsupportedReason::new(format!("unsupported dyn kind `{kind:?}`"))) - } - } -} +// fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { +// match kind { +// rustc_ty::DynKind::Dyn => Ok(DynKind::Dyn), +// rustc_ty::DynKind::DynStar => { +// Err(UnsupportedReason::new(format!("unsupported dyn kind `{kind:?}`"))) +// } +// } +// } fn lower_region(region: &rustc_middle::ty::Region) -> Result { use rustc_middle::ty::RegionKind; diff --git a/crates/flux-middle/src/rustc/ty.rs b/crates/flux-middle/src/rustc/ty.rs index 3147e7e351..410b2d25b2 100644 --- a/crates/flux-middle/src/rustc/ty.rs +++ b/crates/flux-middle/src/rustc/ty.rs @@ -182,7 +182,7 @@ pub enum TyKind { CoroutineWitness(DefId, GenericArgs), Alias(AliasKind, AliasTy), RawPtr(Ty, Mutability), - Dynamic(List>, Region, DynKind), + Dynamic(List>, Region), } #[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] @@ -196,12 +196,6 @@ pub struct ExistentialTraitRef { pub args: GenericArgs, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub enum DynKind { - Dyn, - None, -} - #[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] pub struct AliasTy { pub args: GenericArgs, @@ -648,12 +642,8 @@ impl Ty { TyKind::Param(param).intern() } - pub fn mk_dynamic( - exi_preds: impl Into>>, - r: Region, - kind: DynKind, - ) -> Ty { - TyKind::Dynamic(exi_preds.into(), r, kind).intern() + pub fn mk_dynamic(exi_preds: impl Into>>, r: Region) -> Ty { + TyKind::Dynamic(exi_preds.into(), r).intern() } pub fn mk_ref(region: Region, ty: Ty, mutability: Mutability) -> Ty { @@ -747,7 +737,7 @@ impl Ty { TyKind::Coroutine(_, _) => todo!(), TyKind::CoroutineWitness(_, _) => todo!(), TyKind::Alias(_, _) => todo!(), - TyKind::Dynamic(_, _, _) => todo!(), + TyKind::Dynamic(_, _) => todo!(), }; rustc_ty::Ty::new(tcx, kind) } @@ -870,7 +860,7 @@ impl fmt::Debug for Ty { write!(f, ")")?; Ok(()) } - TyKind::Dynamic(exi_preds, _r, _syn) => { + TyKind::Dynamic(exi_preds, _r) => { write!(f, "dyn {exi_preds:?}") } } diff --git a/crates/flux-middle/src/rustc/ty/subst.rs b/crates/flux-middle/src/rustc/ty/subst.rs index b1c5be919c..cc52b761b2 100644 --- a/crates/flux-middle/src/rustc/ty/subst.rs +++ b/crates/flux-middle/src/rustc/ty/subst.rs @@ -46,7 +46,7 @@ impl Subst for Ty { TyKind::RawPtr(ty, mutbl) => Ty::mk_raw_ptr(ty.subst(args), *mutbl), TyKind::Param(param_ty) => args[param_ty.index as usize].expect_type().clone(), TyKind::FnPtr(fn_sig) => Ty::mk_fn_ptr(fn_sig.subst(args)), - TyKind::Dynamic(exi_preds, re, syn) => Ty::mk_dynamic(exi_preds.subst(args), *re, *syn), + TyKind::Dynamic(exi_preds, re) => Ty::mk_dynamic(exi_preds.subst(args), *re), TyKind::Bool | TyKind::Uint(_) | TyKind::Str diff --git a/crates/flux-refineck/src/checker.rs b/crates/flux-refineck/src/checker.rs index 49b92eac50..7585550e73 100644 --- a/crates/flux-refineck/src/checker.rs +++ b/crates/flux-refineck/src/checker.rs @@ -974,7 +974,7 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> { Ty::mk_ref(*dst_re, dst_slice, *dst_mut) } else // &T -> & dyn U - if let rustc::ty::TyKind::Dynamic(_, _, _) = dst_ty.kind() { + if let rustc::ty::TyKind::Dynamic(_, _) = dst_ty.kind() { self.genv .refine_default(&self.generics, to) .with_span(self.body.span())? diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index 6fc97e01c4..a92eaaa165 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -584,7 +584,7 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { | (BaseTy::Str, BaseTy::Str) | (BaseTy::Char, BaseTy::Char) | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) - | (BaseTy::Dynamic(_, _, _), BaseTy::Dynamic(_, _, _)) => Ok(()), + | (BaseTy::Dynamic(_, _), BaseTy::Dynamic(_, _)) => Ok(()), (BaseTy::Closure(did1, tys1), BaseTy::Closure(did2, tys2)) if did1 == did2 => { debug_assert_eq!(tys1.len(), tys2.len()); for (ty1, ty2) in iter::zip(tys1, tys2) { diff --git a/crates/flux-refineck/src/type_env.rs b/crates/flux-refineck/src/type_env.rs index 1eecad36fe..609ed25279 100644 --- a/crates/flux-refineck/src/type_env.rs +++ b/crates/flux-refineck/src/type_env.rs @@ -373,7 +373,7 @@ impl BasicBlockEnvShape { | BaseTy::Char | BaseTy::Never | BaseTy::Closure(_, _) - | BaseTy::Dynamic(_, _, _) + | BaseTy::Dynamic(_, _) | BaseTy::Coroutine(..) => bty.clone(), } } From 1acc11ce7d2dc50d13c8e8bad133ed23cf3b6d9d Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Thu, 25 Jul 2024 16:17:33 -0700 Subject: [PATCH 19/25] implement to_rustc for Dynamic/ExistentialPredicates --- crates/flux-middle/src/rty/mod.rs | 39 ++++++++++++++++++++----------- tests/tests/pos/surface/dyn04.rs | 10 ++++++++ 2 files changed, 36 insertions(+), 13 deletions(-) create mode 100644 tests/tests/pos/surface/dyn04.rs diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs index 91032db79d..011a10fed5 100644 --- a/crates/flux-middle/src/rty/mod.rs +++ b/crates/flux-middle/src/rty/mod.rs @@ -229,17 +229,30 @@ impl TraitRef { } } -#[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] -pub struct PolyTraitRef { - pub bound_generic_params: List, - pub trait_ref: TraitRef, -} - #[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] pub enum ExistentialPredicate { Trait(ExistentialTraitRef), } +impl Binder { + fn to_rustc<'tcx>( + &self, + tcx: TyCtxt<'tcx>, + ) -> rustc_middle::ty::Binder<'tcx, rustc_middle::ty::ExistentialPredicate<'tcx>> { + assert!(self.vars.is_empty()); + match self.value { + ExistentialPredicate::Trait(ref exi_trait_ref) => { + let exi_trait_ref = rustc_middle::ty::ExistentialTraitRef { + def_id: exi_trait_ref.def_id, + args: exi_trait_ref.args.to_rustc(tcx), + }; + let exi_pred = rustc_middle::ty::ExistentialPredicate::Trait(exi_trait_ref); + rustc_middle::ty::Binder::bind_with_vars(exi_pred, rustc_middle::ty::List::empty()) + } + } + } +} + #[derive(Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)] pub struct ExistentialTraitRef { pub def_id: DefId, @@ -1153,13 +1166,13 @@ impl BaseTy { BaseTy::Array(_, _) => todo!(), BaseTy::Never => tcx.types.never, BaseTy::Closure(_, _) => todo!(), - BaseTy::Dynamic(_exi_preds, _re) => { - todo!() - // let preds = exi_preds - // .iter() - // .map(|pred| pred.to_rustc(tcx)) - // .collect_vec(); - // ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx), rustc_middle::ty::DynKind::Dyn) + BaseTy::Dynamic(exi_preds, re) => { + let preds: Vec<_> = exi_preds + .iter() + .map(|pred| pred.to_rustc(tcx)) + .collect_vec(); + let preds = tcx.mk_poly_existential_predicates(&preds); + ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx), rustc_middle::ty::DynKind::Dyn) } BaseTy::Coroutine(def_id, resume_ty, upvars) => { todo!("Generator {def_id:?} {resume_ty:?} {upvars:?}") diff --git a/tests/tests/pos/surface/dyn04.rs b/tests/tests/pos/surface/dyn04.rs new file mode 100644 index 0000000000..34602e4272 --- /dev/null +++ b/tests/tests/pos/surface/dyn04.rs @@ -0,0 +1,10 @@ +pub trait Animal { + fn noise(&self); +} + +pub fn apply_closure_to_animal(closure: F, animal: &'static dyn Animal) +where + F: FnOnce(&dyn Animal), +{ + closure(animal); +} From 5409fef3f1aa637b3a57301df7f8d810d93c9af0 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 09:36:29 -0700 Subject: [PATCH 20/25] Update crates/flux-middle/src/rustc/lowering.rs Co-authored-by: Nico Lehmann --- crates/flux-middle/src/rustc/lowering.rs | 9 --------- 1 file changed, 9 deletions(-) diff --git a/crates/flux-middle/src/rustc/lowering.rs b/crates/flux-middle/src/rustc/lowering.rs index 0bcfe38370..c76509618a 100644 --- a/crates/flux-middle/src/rustc/lowering.rs +++ b/crates/flux-middle/src/rustc/lowering.rs @@ -822,15 +822,6 @@ fn lower_generic_arg<'tcx>( } } -// fn lower_dyn_kind(kind: &rustc_ty::DynKind) -> Result { -// match kind { -// rustc_ty::DynKind::Dyn => Ok(DynKind::Dyn), -// rustc_ty::DynKind::DynStar => { -// Err(UnsupportedReason::new(format!("unsupported dyn kind `{kind:?}`"))) -// } -// } -// } - fn lower_region(region: &rustc_middle::ty::Region) -> Result { use rustc_middle::ty::RegionKind; match region.kind() { From b60b1a94b78ed8055443cb58f6fe42f283f40056 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 09:40:27 -0700 Subject: [PATCH 21/25] check dyn exi-preds are equal during subtyping --- crates/flux-fhir-analysis/src/conv/mod.rs | 78 +++++----------------- crates/flux-refineck/src/constraint_gen.rs | 7 +- 2 files changed, 22 insertions(+), 63 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 2126178b76..123f43e101 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -9,9 +9,10 @@ //! 3. Refinements are well-sorted. mod fill_holes; + use std::{borrow::Borrow, iter}; -use flux_common::{bug, iter::IterExt, span_bug, tracked_span_bug}; +use flux_common::{bug, iter::IterExt, span_bug}; use flux_middle::{ fhir::{self, ExprRes, FhirId, FluxOwnerId}, global_env::GlobalEnv, @@ -23,7 +24,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc::{self, ty::Region}, + rustc, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -34,7 +35,7 @@ use rustc_hir::{ }; use rustc_middle::{ middle::resolve_bound_vars::ResolvedArg, - ty::{self, AssocItem, AssocKind, BoundVar, EarlyParamRegion}, + ty::{self, AssocItem, AssocKind, BoundVar}, }; use rustc_span::{ symbol::{kw, Ident}, @@ -434,29 +435,6 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { Ok(clauses) } - fn conv_poly_trait_ref_dyn( - &mut self, - env: &mut Env, - poly_trait_ref: &fhir::PolyTraitRef, - ) -> QueryResult> { - let trait_segment = poly_trait_ref.trait_ref.last_segment(); - - if !poly_trait_ref.bound_generic_params.is_empty() { - bug!( - "unexpected! conv_poly_dyn_trait_ref bound_generic_params={:?}", - poly_trait_ref.bound_generic_params - ); - } - - let def_id = poly_trait_ref.trait_def_id(); - let mut into = vec![]; - self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; - - let exi_trait_ref = rty::ExistentialTraitRef { def_id, args: into.into() }; - let exi_pred = rty::ExistentialPredicate::Trait(exi_trait_ref); - Ok(rty::Binder::new(exi_pred, List::empty())) - } - /// Converts a `T: Trait` bound fn conv_poly_trait_ref( &mut self, @@ -475,8 +453,8 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { vec![self.ty_to_generic_arg(self_param.kind, bounded_ty_span, bounded_ty)?]; self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; self.fill_generic_args_defaults(trait_id, &mut args)?; - let trait_ref = rty::TraitRef { def_id: trait_id, args: args.into() }; + let trait_ref = rty::TraitRef { def_id: trait_id, args: args.into() }; let pred = rty::TraitPredicate { trait_ref: trait_ref.clone() }; let vars = poly_trait_ref .bound_generic_params @@ -810,18 +788,6 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let alias_ty = rty::AliasTy::new(def_id, args, refine_args); Ok(rty::Ty::alias(rty::AliasKind::Opaque, alias_ty)) } - fhir::TyKind::TraitObject(poly_traits, lft, syn) => { - let exi_preds: List<_> = poly_traits - .iter() - .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) - .try_collect()?; - let region = self.conv_lifetime(env, *lft); - if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) { - Ok(rty::Ty::dynamic(exi_preds, region)) - } else { - tracked_span_bug!("dyn* traits not supported yet") - } - } } } @@ -1182,30 +1148,20 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { ) -> QueryResult { let generics = self.genv.generics_of(def_id)?; for param in generics.params.iter().skip(into.len()) { - match param.kind { - rty::GenericParamDefKind::Type { has_default } => { - // println!("TRACE: fill_generic_args_defaults: {def_id:?} param = {:?}", param); - debug_assert!(has_default); - let tcx = self.genv.tcx(); - let ty = self - .genv - .type_of(param.def_id)? - .instantiate(tcx, into, &[]) - .to_ty(); - into.push(rty::GenericArg::Ty(ty)); - } - rty::GenericParamDefKind::Lifetime => { - let region = Region::ReEarlyParam(EarlyParamRegion { - index: param.index, - name: param.name, - }); - into.push(rty::GenericArg::Lifetime(region)); - } - _ => { - bug!("unexpected generic param: {param:?}"); - } + if let rty::GenericParamDefKind::Type { has_default } = param.kind { + debug_assert!(has_default); + let tcx = self.genv.tcx(); + let ty = self + .genv + .type_of(param.def_id)? + .instantiate(tcx, into, &[]) + .to_ty(); + into.push(rty::GenericArg::Ty(ty)); + } else { + bug!("unexpected generic param: {param:?}"); } } + Ok(()) } diff --git a/crates/flux-refineck/src/constraint_gen.rs b/crates/flux-refineck/src/constraint_gen.rs index a92eaaa165..315a3487a4 100644 --- a/crates/flux-refineck/src/constraint_gen.rs +++ b/crates/flux-refineck/src/constraint_gen.rs @@ -583,8 +583,11 @@ impl<'a, 'genv, 'tcx> InferCtxt<'a, 'genv, 'tcx> { (BaseTy::Bool, BaseTy::Bool) | (BaseTy::Str, BaseTy::Str) | (BaseTy::Char, BaseTy::Char) - | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) - | (BaseTy::Dynamic(_, _), BaseTy::Dynamic(_, _)) => Ok(()), + | (BaseTy::RawPtr(_, _), BaseTy::RawPtr(_, _)) => Ok(()), + (BaseTy::Dynamic(preds1, _), BaseTy::Dynamic(preds2, _)) => { + assert_eq!(preds1, preds2); + Ok(()) + } (BaseTy::Closure(did1, tys1), BaseTy::Closure(did2, tys2)) if did1 == did2 => { debug_assert_eq!(tys1.len(), tys2.len()); for (ty1, ty2) in iter::zip(tys1, tys2) { From 6a755d58b5e9244fab337134b22be8d4f84b89dc Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 09:43:53 -0700 Subject: [PATCH 22/25] restore --- crates/flux-fhir-analysis/src/conv/mod.rs | 78 ++++++++++++++++++----- 1 file changed, 61 insertions(+), 17 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 123f43e101..2126178b76 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -9,10 +9,9 @@ //! 3. Refinements are well-sorted. mod fill_holes; - use std::{borrow::Borrow, iter}; -use flux_common::{bug, iter::IterExt, span_bug}; +use flux_common::{bug, iter::IterExt, span_bug, tracked_span_bug}; use flux_middle::{ fhir::{self, ExprRes, FhirId, FluxOwnerId}, global_env::GlobalEnv, @@ -24,7 +23,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc, + rustc::{self, ty::Region}, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -35,7 +34,7 @@ use rustc_hir::{ }; use rustc_middle::{ middle::resolve_bound_vars::ResolvedArg, - ty::{self, AssocItem, AssocKind, BoundVar}, + ty::{self, AssocItem, AssocKind, BoundVar, EarlyParamRegion}, }; use rustc_span::{ symbol::{kw, Ident}, @@ -435,6 +434,29 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { Ok(clauses) } + fn conv_poly_trait_ref_dyn( + &mut self, + env: &mut Env, + poly_trait_ref: &fhir::PolyTraitRef, + ) -> QueryResult> { + let trait_segment = poly_trait_ref.trait_ref.last_segment(); + + if !poly_trait_ref.bound_generic_params.is_empty() { + bug!( + "unexpected! conv_poly_dyn_trait_ref bound_generic_params={:?}", + poly_trait_ref.bound_generic_params + ); + } + + let def_id = poly_trait_ref.trait_def_id(); + let mut into = vec![]; + self.conv_generic_args_into(env, def_id, trait_segment.args, &mut into)?; + + let exi_trait_ref = rty::ExistentialTraitRef { def_id, args: into.into() }; + let exi_pred = rty::ExistentialPredicate::Trait(exi_trait_ref); + Ok(rty::Binder::new(exi_pred, List::empty())) + } + /// Converts a `T: Trait` bound fn conv_poly_trait_ref( &mut self, @@ -453,8 +475,8 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { vec![self.ty_to_generic_arg(self_param.kind, bounded_ty_span, bounded_ty)?]; self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?; self.fill_generic_args_defaults(trait_id, &mut args)?; - let trait_ref = rty::TraitRef { def_id: trait_id, args: args.into() }; + let pred = rty::TraitPredicate { trait_ref: trait_ref.clone() }; let vars = poly_trait_ref .bound_generic_params @@ -788,6 +810,18 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { let alias_ty = rty::AliasTy::new(def_id, args, refine_args); Ok(rty::Ty::alias(rty::AliasKind::Opaque, alias_ty)) } + fhir::TyKind::TraitObject(poly_traits, lft, syn) => { + let exi_preds: List<_> = poly_traits + .iter() + .map(|poly_trait| self.conv_poly_trait_ref_dyn(env, poly_trait)) + .try_collect()?; + let region = self.conv_lifetime(env, *lft); + if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) { + Ok(rty::Ty::dynamic(exi_preds, region)) + } else { + tracked_span_bug!("dyn* traits not supported yet") + } + } } } @@ -1148,20 +1182,30 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { ) -> QueryResult { let generics = self.genv.generics_of(def_id)?; for param in generics.params.iter().skip(into.len()) { - if let rty::GenericParamDefKind::Type { has_default } = param.kind { - debug_assert!(has_default); - let tcx = self.genv.tcx(); - let ty = self - .genv - .type_of(param.def_id)? - .instantiate(tcx, into, &[]) - .to_ty(); - into.push(rty::GenericArg::Ty(ty)); - } else { - bug!("unexpected generic param: {param:?}"); + match param.kind { + rty::GenericParamDefKind::Type { has_default } => { + // println!("TRACE: fill_generic_args_defaults: {def_id:?} param = {:?}", param); + debug_assert!(has_default); + let tcx = self.genv.tcx(); + let ty = self + .genv + .type_of(param.def_id)? + .instantiate(tcx, into, &[]) + .to_ty(); + into.push(rty::GenericArg::Ty(ty)); + } + rty::GenericParamDefKind::Lifetime => { + let region = Region::ReEarlyParam(EarlyParamRegion { + index: param.index, + name: param.name, + }); + into.push(rty::GenericArg::Lifetime(region)); + } + _ => { + bug!("unexpected generic param: {param:?}"); + } } } - Ok(()) } From eca76a0681883a9a9020a56c83a42fae54f3ac98 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 09:56:41 -0700 Subject: [PATCH 23/25] use span_bug --- crates/flux-fhir-analysis/src/conv/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 2126178b76..a6a90ac766 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -11,7 +11,7 @@ mod fill_holes; use std::{borrow::Borrow, iter}; -use flux_common::{bug, iter::IterExt, span_bug, tracked_span_bug}; +use flux_common::{bug, iter::IterExt, span_bug}; use flux_middle::{ fhir::{self, ExprRes, FhirId, FluxOwnerId}, global_env::GlobalEnv, @@ -819,7 +819,7 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { if matches!(syn, rustc_ast::TraitObjectSyntax::Dyn) { Ok(rty::Ty::dynamic(exi_preds, region)) } else { - tracked_span_bug!("dyn* traits not supported yet") + span_bug!(ty.span, "dyn* traits not supported yet") } } } From fa16a771417163708bd08d61faf3b9e396e5219a Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 09:58:40 -0700 Subject: [PATCH 24/25] dont fill lifetimes in fill_generic_args --- crates/flux-fhir-analysis/src/conv/mod.rs | 33 ++++++++--------------- 1 file changed, 11 insertions(+), 22 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index a6a90ac766..9886395045 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -1182,28 +1182,17 @@ impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx> { ) -> QueryResult { let generics = self.genv.generics_of(def_id)?; for param in generics.params.iter().skip(into.len()) { - match param.kind { - rty::GenericParamDefKind::Type { has_default } => { - // println!("TRACE: fill_generic_args_defaults: {def_id:?} param = {:?}", param); - debug_assert!(has_default); - let tcx = self.genv.tcx(); - let ty = self - .genv - .type_of(param.def_id)? - .instantiate(tcx, into, &[]) - .to_ty(); - into.push(rty::GenericArg::Ty(ty)); - } - rty::GenericParamDefKind::Lifetime => { - let region = Region::ReEarlyParam(EarlyParamRegion { - index: param.index, - name: param.name, - }); - into.push(rty::GenericArg::Lifetime(region)); - } - _ => { - bug!("unexpected generic param: {param:?}"); - } + if let rty::GenericParamDefKind::Type { has_default } = param.kind { + debug_assert!(has_default); + let tcx = self.genv.tcx(); + let ty = self + .genv + .type_of(param.def_id)? + .instantiate(tcx, into, &[]) + .to_ty(); + into.push(rty::GenericArg::Ty(ty)); + } else { + bug!("unexpected generic param: {param:?}"); } } Ok(()) From a83c11dd93d81144ab57eee999c2864043fecf67 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Sun, 28 Jul 2024 10:00:37 -0700 Subject: [PATCH 25/25] dont fill lifetimes in fill_generic_args --- crates/flux-fhir-analysis/src/conv/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 9886395045..0b6c8cd4ab 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -23,7 +23,7 @@ use flux_middle::{ refining::{self, Refiner}, AdtSortDef, ESpan, WfckResults, INNERMOST, }, - rustc::{self, ty::Region}, + rustc::{self}, }; use itertools::Itertools; use rustc_data_structures::fx::FxIndexMap; @@ -34,7 +34,7 @@ use rustc_hir::{ }; use rustc_middle::{ middle::resolve_bound_vars::ResolvedArg, - ty::{self, AssocItem, AssocKind, BoundVar, EarlyParamRegion}, + ty::{self, AssocItem, AssocKind, BoundVar}, }; use rustc_span::{ symbol::{kw, Ident},