Don't use Free variables internally, substitute at the end

charon-ml/src/generated/Generated_Types.ml

@@ -56,18 +56,26 @@ and de_bruijn_id = int
 (** Type-level variable.
 
     Variables are bound in groups. Each item has a top-level binding group in its `generic_params`
-    field, and then inner binders are possible using the `RegionBinder<T>` type. Each variable is
-    linked to exactly one binder. The `Id` then identifies the specific variable among all those
-    bound in that group.
-
-    We distinguish the top-level (item-level) binder from others: a `Free` variable indicates a
-    variable bound at the item level; a `Bound` variable indicates a variable bound at an inner
-    binder, using a de Bruijn index (i.e. counting binders from the innermost out).
-
-    This distinction is not necessary (we could use bound variables only) but is practical.
+    field, and then inner binders are possible using the `RegionBinder<T>` and `Binder<T>` types.
+    Each variable is linked to exactly one binder. The `Id` then identifies the specific variable
+    among all those bound in that group.
 
     For instance, we have the following:
     ```text
+    fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
+         ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
+           |       inner binder  |       |     inner binder  |        |        |
+     top-level binder            |       |                   |        |        |
+                           Bound(1, b)   |              Bound(2, b)   |     Bound(0, d)
+                                         |                            |
+                                     Bound(0, c)                 Bound(1, c)
+    ```
+
+    To make consumption easier for projects that don't do heavy substitution, a micro-pass at the
+    end changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be
+    `Free`. This is an optional pass, we may add a flag to deactivate it. The example above
+    becomes:
+    ```text
     fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
          ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
            |       inner binder  |       |     inner binder  |        |        |
@@ -83,7 +91,9 @@ and 'a0 de_bruijn_var =
   | Bound of de_bruijn_id * 'a0
       (** A variable attached to the nth binder, counting from the innermost. *)
   | Free of 'a0
-      (** A variable attached to the outermost binder (the one on the item). *)
+      (** A variable attached to the outermost binder (the one on the item). As explained above, This
+          is not used in charon internals, only as a micro-pass before exporting the crate data.
+       *)
 
 and type_var_id = TypeVarId.id
 and const_generic_var_id = ConstGenericVarId.id

charon/Charon.toml

@@ -9,20 +9,22 @@ include = [
     "alloc::alloc::Global",
     "alloc::string::String",
     "alloc::vec::Vec",
+    "core::cmp::Ordering",
+    "core::ops::control_flow::ControlFlow",
     "core::option::Option",
-    "std::path::PathBuf",
-    "crate::options::CliOpts",
     "crate::ast",
-    "crate::ast::krate",
     "crate::ast::expressions",
     "crate::ast::gast",
+    "crate::ast::krate",
     "crate::ast::llbc_ast",
     "crate::ast::meta",
     "crate::ast::names",
     "crate::ast::types",
     "crate::ast::ullbc_ast",
     "crate::ast::values",
     "crate::ids::vector::Vector",
-    "crate::transform::reorder_decls::GDeclarationGroup",
+    "crate::options::CliOpts",
     "crate::transform::reorder_decls::DeclarationGroup",
+    "crate::transform::reorder_decls::GDeclarationGroup",
+    "std::path::PathBuf",
 ]

charon/src/ast/krate.rs

@@ -175,6 +175,15 @@ impl TranslatedCrate {
             .iter()
             .flat_map(|id| Some((*id, self.get_item(*id)?)))
     }
+    pub fn all_items_mut(&mut self) -> impl Iterator<Item = AnyTransItemMut<'_>> {
+        self.type_decls
+            .iter_mut()
+            .map(AnyTransItemMut::Type)
+            .chain(self.fun_decls.iter_mut().map(AnyTransItemMut::Fun))
+            .chain(self.global_decls.iter_mut().map(AnyTransItemMut::Global))
+            .chain(self.trait_decls.iter_mut().map(AnyTransItemMut::TraitDecl))
+            .chain(self.trait_impls.iter_mut().map(AnyTransItemMut::TraitImpl))
+    }
 }
 
 impl<'ctx> AnyTransItem<'ctx> {
@@ -223,6 +232,16 @@ impl<'ctx> AnyTransItem<'ctx> {
 }
 
 impl<'ctx> AnyTransItemMut<'ctx> {
+    pub fn as_ref(&self) -> AnyTransItem<'_> {
+        match self {
+            AnyTransItemMut::Type(d) => AnyTransItem::Type(d),
+            AnyTransItemMut::Fun(d) => AnyTransItem::Fun(d),
+            AnyTransItemMut::Global(d) => AnyTransItem::Global(d),
+            AnyTransItemMut::TraitDecl(d) => AnyTransItem::TraitDecl(d),
+            AnyTransItemMut::TraitImpl(d) => AnyTransItem::TraitImpl(d),
+        }
+    }
+
     /// The generic parameters of this item.
     pub fn generic_params(&mut self) -> &mut GenericParams {
         match self {

charon/src/ast/types/vars.rs

@@ -28,22 +28,30 @@ pub struct DeBruijnId {
 /// Type-level variable.
 ///
 /// Variables are bound in groups. Each item has a top-level binding group in its `generic_params`
-/// field, and then inner binders are possible using the `RegionBinder<T>` type. Each variable is
-/// linked to exactly one binder. The `Id` then identifies the specific variable among all those
-/// bound in that group.
-///
-/// We distinguish the top-level (item-level) binder from others: a `Free` variable indicates a
-/// variable bound at the item level; a `Bound` variable indicates a variable bound at an inner
-/// binder, using a de Bruijn index (i.e. counting binders from the innermost out).
-///
-/// This distinction is not necessary (we could use bound variables only) but is practical.
+/// field, and then inner binders are possible using the `RegionBinder<T>` and `Binder<T>` types.
+/// Each variable is linked to exactly one binder. The `Id` then identifies the specific variable
+/// among all those bound in that group.
 ///
 /// For instance, we have the following:
 /// ```text
 /// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
 ///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
 ///        |       inner binder  |       |     inner binder  |        |        |
 ///  top-level binder            |       |                   |        |        |
+///                        Bound(1, b)   |              Bound(2, b)   |     Bound(0, d)
+///                                      |                            |
+///                                  Bound(0, c)                 Bound(1, c)
+/// ```
+///
+/// To make consumption easier for projects that don't do heavy substitution, a micro-pass at the
+/// end changes the variables bound at the top-level (i.e. in the `GenericParams` of items) to be
+/// `Free`. This is an optional pass, we may add a flag to deactivate it. The example above
+/// becomes:
+/// ```text
+/// fn f<'a, 'b>(x: for<'c> fn(&'b u8, &'c u16, for<'d> fn(&'b u32, &'c u64, &'d u128)) -> u64) {}
+///      ^^^^^^         ^^       ^       ^          ^^       ^        ^        ^
+///        |       inner binder  |       |     inner binder  |        |        |
+///  top-level binder            |       |                   |        |        |
 ///                           Free(b)    |                Free(b)     |     Bound(0, d)
 ///                                      |                            |
 ///                                  Bound(0, c)                 Bound(1, c)
@@ -54,7 +62,8 @@ pub struct DeBruijnId {
 pub enum DeBruijnVar<Id> {
     /// A variable attached to the nth binder, counting from the innermost.
     Bound(DeBruijnId, Id),
-    /// A variable attached to the outermost binder (the one on the item).
+    /// A variable attached to the outermost binder (the one on the item). As explained above, This
+    /// is not used in charon internals, only as a micro-pass before exporting the crate data.
     Free(Id),
 }
 

charon/src/ast/types_utils.rs

@@ -74,27 +74,36 @@ impl GenericParams {
         GenericArgs {
             regions: self
                 .regions
-                .iter_indexed()
-                .map(|(id, _)| Region::Var(DeBruijnVar::free(id)))
-                .collect(),
+                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::new_at_zero(id))),
             types: self
                 .types
-                .iter_indexed()
-                .map(|(id, _)| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty())
-                .collect(),
+                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::new_at_zero(id)).into_ty()),
             const_generics: self
                 .const_generics
-                .iter_indexed()
-                .map(|(id, _)| ConstGeneric::Var(DeBruijnVar::free(id)))
-                .collect(),
-            trait_refs: self
-                .trait_clauses
-                .iter_indexed()
-                .map(|(id, clause)| TraitRef {
-                    kind: TraitRefKind::Clause(DeBruijnVar::free(id)),
-                    trait_decl_ref: clause.trait_.clone(),
-                })
-                .collect(),
+                .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::new_at_zero(id))),
+            trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef {
+                kind: TraitRefKind::Clause(DeBruijnVar::new_at_zero(id)),
+                trait_decl_ref: clause.trait_.clone(),
+            }),
+        }
+    }
+
+    /// Like `identity_args`, but uses free variables instead of bound ones.
+    pub fn free_identity_args(&self) -> GenericArgs {
+        GenericArgs {
+            regions: self
+                .regions
+                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::free(id))),
+            types: self
+                .types
+                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::free(id)).into_ty()),
+            const_generics: self
+                .const_generics
+                .map_ref_indexed(|id, _| ConstGeneric::Var(DeBruijnVar::free(id))),
+            trait_refs: self.trait_clauses.map_ref_indexed(|id, clause| TraitRef {
+                kind: TraitRefKind::Clause(DeBruijnVar::free(id)),
+                trait_decl_ref: clause.trait_.clone(),
+            }),
         }
     }
 }
@@ -588,10 +597,7 @@ impl<'a> SubstVisitor<'a> {
     }
 
     fn should_subst<Id: Copy>(&self, var: DeBruijnVar<Id>) -> Option<Id> {
-        match var {
-            DeBruijnVar::Free(id) => Some(id),
-            DeBruijnVar::Bound(..) => None,
-        }
+        var.bound_at_depth(self.binder_depth)
     }
 
     fn enter_poly_trait_decl_ref(&mut self, _: &mut PolyTraitDeclRef) {

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -1085,11 +1085,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
     /// Make a `DeBruijnVar`, where we use `Free` for the outermost binder and `Bound` for the
     /// others.
     fn bind_var<Id: Copy>(&self, dbid: usize, varid: Id) -> DeBruijnVar<Id> {
-        if dbid == self.binding_levels.len() - 1 {
-            DeBruijnVar::free(varid)
-        } else {
-            DeBruijnVar::bound(DeBruijnId::new(dbid), varid)
-        }
+        DeBruijnVar::bound(DeBruijnId::new(dbid), varid)
     }
 
     pub(crate) fn lookup_bound_region(

charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs

@@ -1509,7 +1509,7 @@ impl<'tcx, 'ctx> BodyTransCtx<'tcx, 'ctx> {
                                 .innermost_generics_mut()
                                 .regions
                                 .push_with(|index| RegionVar { index, name: None });
-                            let r = Region::Var(DeBruijnVar::free(rid));
+                            let r = Region::Var(DeBruijnVar::new_at_zero(rid));
                             let mutability = if kind == ClosureKind::Fn {
                                 RefKind::Shared
                             } else {

charon/src/ids/vector.rs

@@ -153,6 +153,18 @@ where
         }
     }
 
+    /// Map each entry to a new one, keeping the same ids.
+    pub fn map_ref_indexed<'a, U>(&'a self, mut f: impl FnMut(I, &'a T) -> U) -> Vector<I, U> {
+        Vector {
+            vector: self
+                .vector
+                .iter_enumerated()
+                .map(|(i, x_opt)| x_opt.as_ref().map(|x| f(i, x)))
+                .collect(),
+            real_len: self.real_len,
+        }
+    }
+
     /// Iter over the nonempty slots.
     pub fn iter(&self) -> impl Iterator<Item = &T> + Clone {
         self.vector.iter().flat_map(|opt| opt.as_ref())

charon/src/pretty/formatter.rs

@@ -284,6 +284,7 @@ impl<'a> Formatter<RegionDbVar> for FmtCtx<'a> {
             None => format!("wrong_region('_{var})"),
             Some(v) => match &v.name {
                 Some(name) => name.to_string(),
+                None if dbid == self.generics.len() - 1 => format!("'_{varid}"),
                 None => format!("'_{var}"),
             },
         }
@@ -354,6 +355,7 @@ impl<'a> Formatter<ClauseDbVar> for FmtCtx<'a> {
             .and_then(|generics| generics.trait_clauses.get(varid))
         {
             None => format!("missing_clause_var({var})"),
+            Some(_) if dbid == self.generics.len() - 1 => format!("@TraitClause{varid}"),
             Some(_) => format!("@TraitClause{var}"),
         }
     }

charon/src/transform/mod.rs

@@ -24,6 +24,7 @@ pub mod reorder_decls;
 pub mod simplify_constants;
 pub mod skip_trait_refs_when_known;
 pub mod ullbc_to_llbc;
+pub mod unbind_item_vars;
 pub mod update_block_indices;
 pub mod update_closure_signatures;
 
@@ -118,6 +119,8 @@ pub static LLBC_PASSES: &[Pass] = &[
     StructuredBody(&recover_body_comments::Transform),
     // Check that all supplied generic types match the corresponding generic parameters.
     NonBody(&check_generics::Check),
+    // Use `DeBruijnVar::Free` for the variables bound in item signatures.
+    NonBody(&unbind_item_vars::Check),
 ];
 
 #[derive(Clone, Copy)]

charon/src/transform/unbind_item_vars.rs

@@ -0,0 +1,27 @@
+//! Check that all supplied generic types match the corresponding generic parameters.
+
+use derive_visitor::DriveMut;
+
+use crate::ast::types_utils::SubstVisitor;
+
+use super::{ctx::TransformPass, TransformCtx};
+
+pub struct Check;
+impl TransformPass for Check {
+    fn transform_ctx(&self, ctx: &mut TransformCtx) {
+        for mut item in ctx.translated.all_items_mut() {
+            let args = item.generic_params().free_identity_args();
+            let mut visitor = SubstVisitor::new(&args);
+            item.drive_mut(&mut visitor);
+        }
+        for decl in &ctx.translated.fun_decls {
+            if let Ok(body_id) = decl.body {
+                if let Some(body) = ctx.translated.bodies.get_mut(body_id) {
+                    let args = decl.signature.generics.free_identity_args();
+                    let mut visitor = SubstVisitor::new(&args);
+                    body.drive_mut(&mut visitor);
+                }
+            }
+        }
+    }
+}

charon/src/transform/update_closure_signatures.rs

@@ -25,7 +25,7 @@ impl<'a> InsertRegions<'a> {
             let index = self
                 .regions
                 .push_with(|index| RegionVar { index, name: None });
-            *r = Region::Var(DeBruijnVar::free(index));
+            *r = Region::Var(DeBruijnVar::bound(DeBruijnId::new(self.depth), index));
         }
     }
 

charon/tests/ui/hide-marker-traits.out

@@ -0,0 +1,22 @@
+# Final LLBC before serialization:
+
+trait test_crate::Idx<Self>
+
+struct test_crate::IndexVec<I>
+  where
+      [@TraitClause1]: test_crate::Idx<I>,
+ =
+{
+  i: I,
+}
+
+struct test_crate::Vector<I>
+  where
+      [@TraitClause1]: test_crate::Idx<I>,
+ =
+{
+  vector: test_crate::IndexVec<I>[@TraitClause1],
+}
+
+
+

charon/tests/ui/hide-marker-traits.rs

@@ -0,0 +1,17 @@
+//@ charon-args=--hide-marker-traits
+//! Reproduces a crash when substituting variables with the `--hide-marker-traits` option.
+trait Idx {}
+
+pub struct IndexVec<I>
+where
+    I: Idx,
+{
+    i: I,
+}
+
+pub struct Vector<I>
+where
+    I: Idx,
+{
+    vector: IndexVec<I>,
+}