Ignore lifetime parameters properly when numbering type params

src/analyze.rs

@@ -123,22 +123,12 @@ pub struct Analyzer<'tcx> {
     enum_defs: Rc<RefCell<HashMap<DefId, rty::EnumDatatypeDef>>>,
 }
 
-impl<'tcx> crate::refine::TemplateTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-
+impl<'tcx> crate::refine::TemplateRegistry for Analyzer<'tcx> {
     fn register_template<V>(&mut self, tmpl: rty::Template<V>) -> rty::RefinedType<V> {
         tmpl.into_refined_type(|pred_sig| self.generate_pred_var(pred_sig))
     }
 }
 
-impl<'tcx> crate::refine::UnrefinedTypeGenerator<'tcx> for Analyzer<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-}
-
 impl<'tcx> Analyzer<'tcx> {
     pub fn generate_pred_var(&mut self, sig: chc::PredSig) -> chc::PredVarId {
         self.system

src/analyze/basic_block.rs

@@ -14,7 +14,7 @@ use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{
     self, Assumption, BasicBlockType, Env, PlaceType, PlaceTypeBuilder, PlaceTypeVar, TempVarIdx,
-    TemplateTypeGenerator, UnrefinedTypeGenerator, Var,
+    TypeBuilder, Var,
 };
 use crate::rty::{
     self, ClauseBuilderExt as _, ClauseScope as _, ShiftExistential as _, Subtyping as _,
@@ -56,6 +56,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         self.ctx.basic_block_ty(self.local_def_id, bb)
     }
 
+    fn type_builder(&self) -> TypeBuilder<'tcx> {
+        TypeBuilder::new(self.tcx, self.local_def_id.to_def_id())
+    }
+
     fn bind_local(&mut self, local: Local, rty: rty::RefinedType<Var>) {
         let rty = if self.is_mut_local(local) {
             // elaboration:
@@ -219,26 +223,28 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                             .into_iter()
                             .map(|ty| rty::RefinedType::unrefined(ty.vacuous()));
 
-                        let params: IndexVec<_, _> = args
+                        let rty_args: IndexVec<_, _> = args
                             .types()
                             .map(|ty| {
-                                self.ctx
-                                    .build_template_ty_with_scope(&self.env)
-                                    .refined_ty(ty)
+                                self.type_builder()
+                                    .for_template(&mut self.ctx)
+                                    .with_scope(&self.env)
+                                    .build_refined(ty)
                             })
                             .collect();
                         for (field_pty, mut variant_rty) in
                             field_tys.clone().into_iter().zip(variant_rtys)
                         {
-                            variant_rty.instantiate_ty_params(params.clone());
+                            variant_rty.instantiate_ty_params(rty_args.clone());
                             let cs = self
                                 .env
                                 .relate_sub_refined_type(&field_pty.into(), &variant_rty.boxed());
                             self.ctx.extend_clauses(cs);
                         }
 
-                        let sort_args: Vec<_> = params.iter().map(|rty| rty.ty.to_sort()).collect();
-                        let ty = rty::EnumType::new(ty_sym.clone(), params).into();
+                        let sort_args: Vec<_> =
+                            rty_args.iter().map(|rty| rty.ty.to_sort()).collect();
+                        let ty = rty::EnumType::new(ty_sym.clone(), rty_args).into();
 
                         let mut builder = PlaceTypeBuilder::default();
                         let mut field_terms = Vec::new();
@@ -433,7 +439,11 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         let func_ty = match func.const_fn_def() {
             // TODO: move this to well-known defs?
             Some((def_id, args)) if self.is_box_new(def_id) => {
-                let inner_ty = self.ctx.build_template_ty().ty(args.type_at(0)).vacuous();
+                let inner_ty = self
+                    .type_builder()
+                    .for_template(&mut self.ctx)
+                    .build(args.type_at(0))
+                    .vacuous();
                 let param = rty::RefinedType::unrefined(inner_ty.clone());
                 let ret_term =
                     chc::Term::box_(chc::Term::var(rty::FunctionParamIdx::from(0_usize)));
@@ -444,7 +454,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 rty::FunctionType::new([param].into_iter().collect(), ret).into()
             }
             Some((def_id, args)) if self.is_mem_swap(def_id) => {
-                let inner_ty = self.ctx.unrefined_ty(args.type_at(0)).vacuous();
+                let inner_ty = self.type_builder().build(args.type_at(0)).vacuous();
                 let param1 =
                     rty::RefinedType::unrefined(rty::PointerType::mut_to(inner_ty.clone()).into());
                 let param2 =
@@ -531,7 +541,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     }
 
     fn add_prophecy_var(&mut self, statement_index: usize, ty: mir_ty::Ty<'tcx>) {
-        let ty = self.ctx.unrefined_ty(ty);
+        let ty = self.type_builder().build(ty);
         let temp_var = self.env.push_temp_var(ty.vacuous());
         self.prophecy_vars.insert(statement_index, temp_var);
         tracing::debug!(stmt_idx = %statement_index, temp_var = ?temp_var, "add_prophecy_var");
@@ -552,7 +562,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         referent: mir::Place<'tcx>,
         prophecy_ty: mir_ty::Ty<'tcx>,
     ) -> rty::RefinedType<Var> {
-        let prophecy_ty = self.ctx.unrefined_ty(prophecy_ty);
+        let prophecy_ty = self.type_builder().build(prophecy_ty);
         let prophecy = self.env.push_temp_var(prophecy_ty.vacuous());
         let place = self.elaborate_place_for_borrow(&referent);
         self.env.borrow_place(place, prophecy).into()
@@ -665,9 +675,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
             let decl = self.local_decls[destination].clone();
             let rty = self
-                .ctx
-                .build_template_ty_with_scope(&self.env)
-                .refined_ty(decl.ty);
+                .type_builder()
+                .for_template(&mut self.ctx)
+                .with_scope(&self.env)
+                .build_refined(decl.ty);
             self.type_call(func.clone(), args.clone().into_iter().map(|a| a.node), &rty);
             self.bind_local(destination, rty);
         }
@@ -738,9 +749,10 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     #[tracing::instrument(skip(self))]
     fn ret_template(&mut self) -> rty::RefinedType<Var> {
         let ret_ty = self.body.local_decls[mir::RETURN_PLACE].ty;
-        self.ctx
-            .build_template_ty_with_scope(&self.env)
-            .refined_ty(ret_ty)
+        self.type_builder()
+            .for_template(&mut self.ctx)
+            .with_scope(&self.env)
+            .build_refined(ret_ty)
     }
 
     // TODO: remove this

src/analyze/crate_.rs

@@ -11,7 +11,7 @@ use rustc_span::symbol::Ident;
 use crate::analyze;
 use crate::annot::{self, AnnotFormula, AnnotParser, ResolverExt as _};
 use crate::chc;
-use crate::refine::{self, TemplateTypeGenerator, UnrefinedTypeGenerator};
+use crate::refine::{self, TypeBuilder};
 use crate::rty::{self, ClauseBuilderExt as _};
 
 /// An implementation of local crate analysis.
@@ -132,13 +132,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
         let mut param_resolver = analyze::annot::ParamResolver::default();
         for (input_ident, input_ty) in self.tcx.fn_arg_names(def_id).iter().zip(sig.inputs()) {
-            let input_ty = self.ctx.unrefined_ty(*input_ty);
+            let input_ty = TypeBuilder::new(self.tcx, def_id).build(*input_ty);
             param_resolver.push_param(input_ident.name, input_ty.to_sort());
         }
 
         let mut require_annot = self.extract_require_annot(&param_resolver, def_id);
         let mut ensure_annot = {
-            let output_ty = self.ctx.unrefined_ty(sig.output());
+            let output_ty = TypeBuilder::new(self.tcx, def_id).build(sig.output());
             let resolver = annot::StackedResolver::default()
                 .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
                 .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
@@ -175,7 +175,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             self.trusted.insert(def_id);
         }
 
-        let mut builder = self.ctx.build_function_template_ty(sig);
+        let mut builder =
+            TypeBuilder::new(self.tcx, def_id).for_function_template(&mut self.ctx, sig);
         if let Some(AnnotFormula::Formula(require)) = require_annot {
             let formula = require.map_var(|idx| {
                 if idx.index() == sig.inputs().len() - 1 {
@@ -251,6 +252,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 continue;
             };
             let adt = self.tcx.adt_def(local_def_id);
+
             let name = refine::datatype_symbol(self.tcx, local_def_id.to_def_id());
             let variants: IndexVec<_, _> = adt
                 .variants()
@@ -264,7 +266,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                         .iter()
                         .map(|field| {
                             let field_ty = self.tcx.type_of(field.did).instantiate_identity();
-                            self.ctx.unrefined_ty(field_ty)
+                            TypeBuilder::new(self.tcx, local_def_id.to_def_id()).build(field_ty)
                         })
                         .collect();
                     rty::EnumVariantDef {
@@ -275,19 +277,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 })
                 .collect();
 
-            let ty_params = adt
-                .all_fields()
-                .map(|f| self.tcx.type_of(f.did).instantiate_identity())
-                .flat_map(|ty| {
-                    if let mir_ty::TyKind::Param(p) = ty.kind() {
-                        Some(p.index as usize)
-                    } else {
-                        None
-                    }
+            let generics = self.tcx.generics_of(local_def_id);
+            let ty_params = (0..generics.count())
+                .filter(|idx| {
+                    matches!(
+                        generics.param_at(*idx, self.tcx).kind,
+                        mir_ty::GenericParamDefKind::Type { .. }
+                    )
                 })
-                .max()
-                .map(|max| max + 1)
-                .unwrap_or(0);
+                .count();
             tracing::debug!(?local_def_id, ?name, ?ty_params, "ty_params count");
 
             let def = rty::EnumDatatypeDef {

src/analyze/local_def.rs

@@ -11,7 +11,7 @@ use rustc_span::def_id::LocalDefId;
 use crate::analyze;
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
-use crate::refine::{BasicBlockType, TemplateTypeGenerator};
+use crate::refine::{BasicBlockType, TypeBuilder};
 use crate::rty;
 
 /// An implementation of the typing of local definitions.
@@ -306,7 +306,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             }
             // function return type is basic block return type
             let ret_ty = self.body.local_decls[mir::RETURN_PLACE].ty;
-            let rty = self.ctx.basic_block_template_ty(live_locals, ret_ty);
+            let rty = TypeBuilder::new(self.tcx, self.local_def_id.to_def_id())
+                .for_template(&mut self.ctx)
+                .build_basic_block(live_locals, ret_ty);
             self.ctx.register_basic_block_ty(self.local_def_id, bb, rty);
         }
     }

src/refine.rs

@@ -8,7 +8,7 @@
 //! module and remove this one.
 
 mod template;
-pub use template::{TemplateScope, TemplateTypeGenerator, UnrefinedTypeGenerator};
+pub use template::{TemplateRegistry, TemplateScope, TypeBuilder};
 
 mod basic_block;
 pub use basic_block::BasicBlockType;

src/refine/env.rs

@@ -558,7 +558,8 @@ impl rty::ClauseScope for Env {
     }
 }
 
-impl refine::TemplateScope<Var> for Env {
+impl refine::TemplateScope for Env {
+    type Var = Var;
     fn build_template(&self) -> rty::TemplateBuilder<Var> {
         let mut builder = rty::TemplateBuilder::default();
         for (v, sort) in self.dependencies() {
@@ -930,7 +931,7 @@ impl Env {
                         .field_tys()
                         .map(|ty| rty::RefinedType::unrefined(ty.clone().vacuous()).boxed());
                     let got_tys = field_tys.iter().map(|ty| ty.clone().into());
-                    rty::unify_tys_params(expected_tys, got_tys).into_params(def.ty_params, |_| {
+                    rty::unify_tys_params(expected_tys, got_tys).into_args(def.ty_params, |_| {
                         panic!("var_type: should unify all params")
                     })
                 };