charon_lib/ast/
type_level.rs

1use derive_generic_visitor::*;
2use itertools::Itertools;
3use serde_state::{DeserializeState, SerializeState};
4use std::{collections::HashSet, mem};
5
6use crate::ast::*;
7
8pub mod regions;
9pub mod substitute;
10pub mod trait_proofs;
11pub mod types;
12pub mod vars;
13
14pub use regions::*;
15pub use substitute::*;
16pub use trait_proofs::*;
17pub use types::*;
18pub use vars::*;
19
20/// A set of generic arguments.
21#[derive(
22    Clone,
23    PartialEq,
24    Eq,
25    PartialOrd,
26    Ord,
27    Hash,
28    SerializeState,
29    DeserializeState,
30    Drive,
31    DriveMut,
32    DriveTwo,
33)]
34pub struct GenericArgs {
35    pub regions: IndexVec<RegionId, Region>,
36    pub types: IndexVec<TypeVarId, Ty>,
37    pub const_generics: IndexVec<ConstGenericVarId, ConstantExpr>,
38    pub trait_refs: IndexVec<TraitClauseId, TraitRef>,
39}
40
41/// A quantified trait predicate, e.g. `for<'a> Type<'a>: Trait<'a, Args>`.
42pub type PolyTraitDeclRef = RegionBinder<TraitDeclRef>;
43
44/// .0 outlives .1
45#[derive(
46    Debug,
47    Clone,
48    PartialEq,
49    Eq,
50    PartialOrd,
51    Ord,
52    Hash,
53    SerializeState,
54    DeserializeState,
55    Drive,
56    DriveMut,
57    DriveTwo,
58)]
59pub struct OutlivesPred<T, U>(pub T, pub U);
60
61pub type RegionOutlives = OutlivesPred<Region, Region>;
62pub type TypeOutlives = OutlivesPred<Ty, Region>;
63
64/// A constraint over a trait associated type.
65///
66/// Example:
67/// ```text
68/// T : Foo<S = String>
69///         ^^^^^^^^^^
70/// ```
71#[derive(
72    Debug,
73    Clone,
74    PartialEq,
75    Eq,
76    PartialOrd,
77    Ord,
78    Hash,
79    SerializeState,
80    DeserializeState,
81    Drive,
82    DriveMut,
83    DriveTwo,
84)]
85pub struct TraitTypeConstraint {
86    pub trait_ref: TraitRef,
87    pub type_id: AssocTypeId,
88    pub ty: Ty,
89}
90
91pub type BoxedArgs = Box<GenericArgs>;
92
93/// Generic parameters for a declaration, including predicates.
94#[derive(
95    Default,
96    Clone,
97    PartialEq,
98    Eq,
99    PartialOrd,
100    Ord,
101    Hash,
102    SerializeState,
103    DeserializeState,
104    Drive,
105    DriveMut,
106    DriveTwo,
107)]
108pub struct GenericParams {
109    #[serde_state(stateless)]
110    pub regions: IndexVec<RegionId, RegionParam>,
111    #[serde_state(stateless)]
112    pub types: IndexVec<TypeVarId, TypeParam>,
113    pub const_generics: IndexVec<ConstGenericVarId, ConstGenericParam>,
114    // TODO: rename to match [GenericArgs]?
115    pub trait_clauses: IndexVec<TraitClauseId, TraitParam>,
116    /// The first region in the pair outlives the second region
117    pub regions_outlive: Vec<RegionBinder<RegionOutlives>>,
118    /// The type outlives the region
119    pub types_outlive: Vec<RegionBinder<TypeOutlives>>,
120    /// Constraints over trait associated types
121    pub trait_type_constraints: IndexVec<TraitTypeConstraintId, RegionBinder<TraitTypeConstraint>>,
122}
123
124#[derive(
125    Debug,
126    Clone,
127    PartialEq,
128    Eq,
129    PartialOrd,
130    Ord,
131    Hash,
132    SerializeState,
133    DeserializeState,
134    Drive,
135    DriveMut,
136    DriveTwo,
137)]
138#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("BK"))]
139pub enum BinderKind {
140    /// The parameters of a generic associated type.
141    TraitType(TraitDeclId, AssocTypeId),
142    /// The parameters of a trait method. Used in the `methods` lists in trait decls and trait
143    /// impls.
144    TraitMethod(TraitDeclId, TraitMethodId),
145    /// The parameters bound in a non-trait `impl` block. Used in the `Name`s of inherent methods.
146    InherentImplBlock,
147    /// Binder used for `dyn Trait` existential predicates.
148    Dyn,
149    /// Some other use of a binder outside the main Charon ast.
150    Other,
151}
152
153/// A value of type `T` bound by generic parameters. Used in any context where we're adding generic
154/// parameters that aren't on the top-level item, e.g. `for<'a>` clauses (uses `RegionBinder` for
155/// now), trait methods, GATs (TODO).
156#[derive(
157    Debug,
158    Clone,
159    PartialEq,
160    Eq,
161    PartialOrd,
162    Ord,
163    Hash,
164    SerializeState,
165    DeserializeState,
166    Drive,
167    DriveMut,
168    DriveTwo,
169)]
170pub struct Binder<T> {
171    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_params"))]
172    pub params: GenericParams,
173    /// Named this way to highlight accesses to the inner value that might be handling parameters
174    /// incorrectly. Prefer using helper methods.
175    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))]
176    pub skip_binder: T,
177    /// The kind of binder this is.
178    #[cfg_attr(feature = "charon_on_charon", charon::opaque)]
179    pub kind: BinderKind,
180}
181
182/// A value of type `T` bound by regions. We should use `binder` instead but this causes name clash
183/// issues in the derived ocaml visitors.
184#[derive(
185    Debug,
186    Clone,
187    PartialEq,
188    Eq,
189    PartialOrd,
190    Ord,
191    Hash,
192    SerializeState,
193    DeserializeState,
194    Drive,
195    DriveMut,
196    DriveTwo,
197)]
198pub struct RegionBinder<T> {
199    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_regions"))]
200    #[serde_state(stateless)]
201    pub regions: IndexVec<RegionId, RegionParam>,
202    /// Named this way to highlight accesses to the inner value that might be handling parameters
203    /// incorrectly. Prefer using helper methods.
204    #[cfg_attr(feature = "charon_on_charon", charon::rename("binder_value"))]
205    pub skip_binder: T,
206}
207
208impl GenericArgs {
209    pub fn len(&self) -> usize {
210        let GenericArgs {
211            regions,
212            types,
213            const_generics,
214            trait_refs,
215        } = self;
216        regions.len() + types.len() + const_generics.len() + trait_refs.len()
217    }
218
219    pub fn is_empty(&self) -> bool {
220        self.len() == 0
221    }
222    /// Whether this has any explicit arguments (types, regions or const generics).
223    pub fn has_explicits(&self) -> bool {
224        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
225    }
226    /// Whether this has any implicit arguments (trait refs).
227    pub fn has_implicits(&self) -> bool {
228        !self.trait_refs.is_empty()
229    }
230
231    pub fn empty() -> Self {
232        GenericArgs {
233            regions: Default::default(),
234            types: Default::default(),
235            const_generics: Default::default(),
236            trait_refs: Default::default(),
237        }
238    }
239
240    pub fn new(
241        regions: IndexVec<RegionId, Region>,
242        types: IndexVec<TypeVarId, Ty>,
243        const_generics: IndexVec<ConstGenericVarId, ConstantExpr>,
244        trait_refs: IndexVec<TraitClauseId, TraitRef>,
245    ) -> Self {
246        Self {
247            regions,
248            types,
249            const_generics,
250            trait_refs,
251        }
252    }
253    pub fn new_types(types: IndexVec<TypeVarId, Ty>) -> Self {
254        Self {
255            types,
256            ..Self::empty()
257        }
258    }
259    pub fn new_lifetimes(regions: IndexVec<RegionId, Region>) -> Self {
260        Self {
261            regions,
262            ..Self::empty()
263        }
264    }
265
266    /// Check whether this matches the given `GenericParams`.
267    /// TODO: check more things, e.g. that the trait refs use the correct trait and generics.
268    pub fn matches(&self, params: &GenericParams) -> bool {
269        params.regions.len() == self.regions.len()
270            && params.types.len() == self.types.len()
271            && params.const_generics.len() == self.const_generics.len()
272            && params.trait_clauses.len() == self.trait_refs.len()
273    }
274
275    /// Return the same generics, but where we pop the first type arguments.
276    /// This is useful for trait references (for pretty printing for instance),
277    /// because the first type argument is the type for which the trait is
278    /// implemented.
279    pub fn pop_first_type_arg(&self) -> (Ty, Self) {
280        let mut generics = self.clone();
281        let mut it = mem::take(&mut generics.types).into_iter();
282        let ty = it.next().unwrap();
283        generics.types = it.collect();
284        (ty, generics)
285    }
286
287    /// Concatenate this set of arguments with another one. Use with care, you must manage the
288    /// order of arguments correctly.
289    pub fn concat(mut self, other: &Self) -> Self {
290        let Self {
291            regions,
292            types,
293            const_generics,
294            trait_refs,
295        } = other;
296        self.regions.clone_extend_from_other(regions);
297        self.types.clone_extend_from_other(types);
298        self.const_generics.clone_extend_from_other(const_generics);
299        self.trait_refs.clone_extend_from_other(trait_refs);
300        self
301    }
302}
303
304impl GenericParams {
305    pub fn empty() -> Self {
306        Self::default()
307    }
308
309    pub fn is_empty(&self) -> bool {
310        self.len() == 0
311    }
312    /// Whether this has any explicit arguments (types, regions or const generics).
313    pub fn has_explicits(&self) -> bool {
314        !self.regions.is_empty() || !self.types.is_empty() || !self.const_generics.is_empty()
315    }
316    /// Whether this has any implicit arguments (trait clauses, outlives relations, associated type
317    /// equality constraints).
318    pub fn has_predicates(&self) -> bool {
319        !self.trait_clauses.is_empty()
320            || !self.types_outlive.is_empty()
321            || !self.regions_outlive.is_empty()
322            || !self.trait_type_constraints.is_empty()
323    }
324
325    /// Run some sanity checks.
326    pub fn check_consistency(&self) {
327        // Sanity check: check the clause ids are consistent.
328        assert!(
329            self.trait_clauses
330                .iter()
331                .enumerate()
332                .all(|(i, c)| c.clause_id.index() == i)
333        );
334
335        // Sanity check: region names are pairwise distinct (this caused trouble when generating
336        // names for the backward functions in Aeneas): at some point, Rustc introduced names equal
337        // to `Some("'_")` for the anonymous regions, instead of using `None` (we now check in
338        // [translate_region_name] and ignore names equal to "'_").
339        let mut s = HashSet::new();
340        for r in &self.regions {
341            if let Some(name) = &r.name {
342                assert!(
343                    !s.contains(name),
344                    "Name \"{}\" reused for two different lifetimes",
345                    name
346                );
347                s.insert(name);
348            }
349        }
350    }
351
352    pub fn len(&self) -> usize {
353        let GenericParams {
354            regions,
355            types,
356            const_generics,
357            trait_clauses,
358            regions_outlive,
359            types_outlive,
360            trait_type_constraints,
361        } = self;
362        regions.len()
363            + types.len()
364            + const_generics.len()
365            + trait_clauses.len()
366            + regions_outlive.len()
367            + types_outlive.len()
368            + trait_type_constraints.len()
369    }
370
371    /// Construct a set of generic arguments in the scope of `self` that matches `self` and feeds
372    /// each required parameter with itself. E.g. given parameters for `<T, U> where U:
373    /// PartialEq<T>`, the arguments would be `<T, U>[TraitClause0]`.
374    pub fn identity_args(&self) -> GenericArgs {
375        self.identity_args_at_depth(DeBruijnId::zero())
376    }
377
378    /// Like `identity_args` but uses variables bound at the given depth.
379    pub fn identity_args_at_depth(&self, depth: DeBruijnId) -> GenericArgs {
380        GenericArgs {
381            regions: self
382                .regions
383                .map_ref_indexed(|id, _| Region::Var(DeBruijnVar::bound(depth, id))),
384            types: self
385                .types
386                .map_ref_indexed(|id, _| TyKind::TypeVar(DeBruijnVar::bound(depth, id)).into_ty()),
387            const_generics: self.const_generics.map_ref_indexed(|id, c| {
388                ConstantExpr::new(
389                    ConstantExprKind::Var(DeBruijnVar::bound(depth, id)),
390                    c.ty.clone(),
391                )
392            }),
393            trait_refs: self
394                .trait_clauses
395                .map_ref(|clause| clause.identity_tref_at_depth(depth)),
396        }
397    }
398
399    /// Take the predicates from the another `GenericParams`. This assumes the clause ids etc are
400    /// already consistent.
401    pub fn take_predicates_from(&mut self, other: GenericParams) {
402        assert!(!other.has_explicits());
403        let num_clauses = self.trait_clauses.len();
404        let GenericParams {
405            regions: _,
406            types: _,
407            const_generics: _,
408            trait_clauses,
409            regions_outlive,
410            types_outlive,
411            trait_type_constraints,
412        } = other;
413        self.trait_clauses
414            .extend(trait_clauses.into_iter().update(|clause| {
415                clause.clause_id += num_clauses;
416            }));
417        self.regions_outlive.extend(regions_outlive);
418        self.types_outlive.extend(types_outlive);
419        self.trait_type_constraints.extend(trait_type_constraints);
420    }
421
422    /// Take the predicates from the another `GenericParams`. This assumes that the two
423    /// `GenericParams` are independent, hence will shift clause ids if `other` has any
424    /// trait refs that reference its own clauses.
425    pub fn merge_predicates_from(&mut self, mut other: GenericParams) {
426        // Drop the explicits params.
427        other.types.clear();
428        other.regions.clear();
429        other.const_generics.clear();
430        // The contents of `other` may refer to its own trait clauses, so we must shift clause ids.
431        struct ShiftClausesVisitor(usize);
432        impl VarsVisitor for ShiftClausesVisitor {
433            fn visit_clause_var(&mut self, v: ClauseDbVar) -> Option<TraitRefKind> {
434                if let DeBruijnVar::Bound(DeBruijnId::ZERO, clause_id) = v {
435                    // Replace clause 0 and decrement the others.
436                    Some(TraitRefKind::Clause(DeBruijnVar::Bound(
437                        DeBruijnId::ZERO,
438                        clause_id + self.0,
439                    )))
440                } else {
441                    None
442                }
443            }
444        }
445        let num_clauses = self.trait_clauses.len();
446        other.visit_vars(&mut ShiftClausesVisitor(num_clauses));
447        self.take_predicates_from(other);
448    }
449}
450
451impl<T> Binder<T> {
452    /// Wrap the value in an empty binder, shifting variables appropriately.
453    pub fn empty(kind: BinderKind, x: T) -> Self
454    where
455        T: TyVisitable,
456    {
457        Binder {
458            params: Default::default(),
459            skip_binder: x.move_under_binder(),
460            kind,
461        }
462    }
463    pub fn new(kind: BinderKind, params: GenericParams, skip_binder: T) -> Self {
464        Self {
465            params,
466            skip_binder,
467            kind,
468        }
469    }
470
471    /// Whether this binder binds any variables.
472    pub fn binds_anything(&self) -> bool {
473        !self.params.is_empty()
474    }
475
476    /// Retreive the contents of this binder if the binder binds no variables. This is the invers
477    /// of `Binder::empty`.
478    pub fn get_if_binds_nothing(&self) -> Option<T>
479    where
480        T: TyVisitable + Clone,
481    {
482        self.params
483            .is_empty()
484            .then(|| self.skip_binder.clone().move_from_under_binder().unwrap())
485    }
486
487    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
488        Binder {
489            params: self.params,
490            skip_binder: f(self.skip_binder),
491            kind: self.kind,
492        }
493    }
494
495    pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> Binder<U> {
496        Binder {
497            params: self.params.clone(),
498            skip_binder: f(&self.skip_binder),
499            kind: self.kind.clone(),
500        }
501    }
502
503    /// Substitute the provided arguments for the variables bound in this binder and return the
504    /// substituted inner value.
505    pub fn apply(self, args: &GenericArgs) -> T
506    where
507        T: TyVisitable,
508    {
509        self.skip_binder.substitute(args)
510    }
511
512    /// Like `apply`, but also keep the parameters: predicates mention them and therefore need to
513    /// be substituted before use too.
514    pub fn apply_keep_params(self, args: &GenericArgs) -> (GenericParams, T)
515    where
516        T: TyVisitable,
517    {
518        (
519            self.params.substitute(args),
520            self.skip_binder.substitute(args),
521        )
522    }
523}
524
525impl<T: AstVisitable> Binder<Binder<T>> {
526    /// Flatten two levels of binders into a single one.
527    pub fn flatten(self) -> Binder<T> {
528        #[derive(Visitor)]
529        struct FlattenVisitor<'a> {
530            shift_by: &'a GenericParams,
531            binder_depth: DeBruijnId,
532        }
533        impl VisitorWithBinderDepth for FlattenVisitor<'_> {
534            fn binder_depth_mut(&mut self) -> &mut DeBruijnId {
535                &mut self.binder_depth
536            }
537        }
538        impl VisitAstMut for FlattenVisitor<'_> {
539            fn visit<T: AstVisitable>(&mut self, x: &mut T) -> ControlFlow<Self::Break> {
540                VisitWithBinderDepth::new(self).visit(x)
541            }
542
543            fn enter_de_bruijn_id(&mut self, db_id: &mut DeBruijnId) {
544                if *db_id > self.binder_depth {
545                    // We started visiting at the inner binder, so in this branch we're either
546                    // mentioning the outer binder or a binder further beyond. Either way we
547                    // decrease the depth; variables that point to the outer binder don't have to
548                    // be shifted.
549                    *db_id = db_id.decr();
550                }
551            }
552            fn enter_region(&mut self, x: &mut Region) {
553                if let Region::Var(var) = x
554                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
555                {
556                    *id += self.shift_by.regions.len();
557                }
558            }
559            fn enter_ty_kind(&mut self, x: &mut TyKind) {
560                if let TyKind::TypeVar(var) = x
561                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
562                {
563                    *id += self.shift_by.types.len();
564                }
565            }
566            fn enter_constant_expr_kind(&mut self, kind: &mut ConstantExprKind) {
567                if let ConstantExprKind::Var(var) = kind
568                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
569                {
570                    *id += self.shift_by.const_generics.len();
571                }
572            }
573            fn enter_trait_ref_kind(&mut self, x: &mut TraitRefKind) {
574                if let TraitRefKind::Clause(var) = x
575                    && let Some(id) = var.bound_at_depth_mut(self.binder_depth)
576                {
577                    *id += self.shift_by.trait_clauses.len();
578                }
579            }
580        }
581
582        // We will concatenate both sets of params.
583        let mut outer_params = self.params;
584
585        // The inner value needs to change:
586        // - at binder level 0 we shift all variable ids to match the concatenated params;
587        // - at binder level > 0 we decrease binding level because there's one fewer binder.
588        let mut bound_value = self.skip_binder.skip_binder;
589        let _ = bound_value.drive_mut(&mut FlattenVisitor {
590            shift_by: &outer_params,
591            binder_depth: Default::default(),
592        });
593
594        // The inner params must also be updated, as they can refer to themselves and the outer
595        // one.
596        let mut inner_params = self.skip_binder.params;
597        let _ = inner_params.drive_mut(&mut FlattenVisitor {
598            shift_by: &outer_params,
599            binder_depth: Default::default(),
600        });
601        inner_params
602            .regions
603            .iter_mut()
604            .for_each(|v| v.index += outer_params.regions.len());
605        inner_params
606            .types
607            .iter_mut()
608            .for_each(|v| v.index += outer_params.types.len());
609        inner_params
610            .const_generics
611            .iter_mut()
612            .for_each(|v| v.index += outer_params.const_generics.len());
613        inner_params
614            .trait_clauses
615            .iter_mut()
616            .for_each(|v| v.clause_id += outer_params.trait_clauses.len());
617
618        let GenericParams {
619            regions,
620            types,
621            const_generics,
622            trait_clauses,
623            regions_outlive,
624            types_outlive,
625            trait_type_constraints,
626        } = &inner_params;
627        outer_params.regions.clone_extend_from_other(regions);
628        outer_params.types.clone_extend_from_other(types);
629        outer_params
630            .const_generics
631            .clone_extend_from_other(const_generics);
632        outer_params
633            .trait_clauses
634            .clone_extend_from_other(trait_clauses);
635        outer_params
636            .regions_outlive
637            .extend_from_slice(regions_outlive);
638        outer_params.types_outlive.extend_from_slice(types_outlive);
639        outer_params
640            .trait_type_constraints
641            .clone_extend_from_other(trait_type_constraints);
642
643        Binder {
644            params: outer_params,
645            skip_binder: bound_value,
646            kind: BinderKind::Other,
647        }
648    }
649}
650
651impl<T> RegionBinder<T> {
652    /// Wrap the value in an empty region binder, shifting variables appropriately.
653    pub fn empty(x: T) -> Self
654    where
655        T: TyVisitable,
656    {
657        RegionBinder {
658            regions: Default::default(),
659            skip_binder: x.move_under_binder(),
660        }
661    }
662
663    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> RegionBinder<U> {
664        RegionBinder {
665            regions: self.regions,
666            skip_binder: f(self.skip_binder),
667        }
668    }
669
670    pub fn map_ref<U>(&self, f: impl FnOnce(&T) -> U) -> RegionBinder<U> {
671        RegionBinder {
672            regions: self.regions.clone(),
673            skip_binder: f(&self.skip_binder),
674        }
675    }
676
677    /// Substitute the bound variables with the given lifetimes.
678    pub fn apply(self, regions: IndexVec<RegionId, Region>) -> T
679    where
680        T: TyVisitable,
681    {
682        assert_eq!(regions.len(), self.regions.len());
683        let args = GenericArgs {
684            regions,
685            ..GenericArgs::empty()
686        };
687        self.skip_binder.substitute_inner_binder(&args)
688    }
689
690    /// Substitute the bound variables with erased lifetimes.
691    pub fn erase(self) -> T
692    where
693        T: TyVisitable,
694    {
695        let regions = self.regions.map_ref_indexed(|_, _| Region::Erased);
696        self.apply(regions)
697    }
698}
699
700pub trait HasIdxVecOf<Id: Idx>: std::ops::Index<Id, Output: Sized> {
701    fn get_idx_vec(&self) -> &IndexVec<Id, Self::Output>;
702    fn get_idx_vec_mut(&mut self) -> &mut IndexVec<Id, Self::Output>;
703}
704
705/// Delegate `Index` implementations to subfields.
706macro_rules! mk_index_impls {
707    ($ty:ident.$field:ident[$idx:ty]: $output:ty) => {
708        impl std::ops::Index<$idx> for $ty {
709            type Output = $output;
710            fn index(&self, index: $idx) -> &Self::Output {
711                &self.$field[index]
712            }
713        }
714        impl std::ops::IndexMut<$idx> for $ty {
715            fn index_mut(&mut self, index: $idx) -> &mut Self::Output {
716                &mut self.$field[index]
717            }
718        }
719        impl HasIdxVecOf<$idx> for $ty {
720            fn get_idx_vec(&self) -> &IndexVec<$idx, Self::Output> {
721                &self.$field
722            }
723            fn get_idx_vec_mut(&mut self) -> &mut IndexVec<$idx, Self::Output> {
724                &mut self.$field
725            }
726        }
727    };
728}
729mk_index_impls!(GenericArgs.regions[RegionId]: Region);
730mk_index_impls!(GenericArgs.types[TypeVarId]: Ty);
731mk_index_impls!(GenericArgs.const_generics[ConstGenericVarId]: ConstantExpr);
732mk_index_impls!(GenericArgs.trait_refs[TraitClauseId]: TraitRef);
733mk_index_impls!(GenericParams.regions[RegionId]: RegionParam);
734mk_index_impls!(GenericParams.types[TypeVarId]: TypeParam);
735mk_index_impls!(GenericParams.const_generics[ConstGenericVarId]: ConstGenericParam);
736mk_index_impls!(GenericParams.trait_clauses[TraitClauseId]: TraitParam);
charon_lib/ast/type_level.rs

charon_lib/ast/
type_level.rs
