Translate variance information

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.224"
+let supported_charon_version = "0.1.225"

charon-ml/src/generated/Generated_OfJson.ml

@@ -1106,11 +1106,18 @@ and region_param_of_json (ctx : of_json_ctx) (js : json) :
     (region_param, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("index", index); ("name", name); ("mutability", mutability) ] ->
+    | `Assoc
+        [
+          ("index", index);
+          ("name", name);
+          ("variance", variance);
+          ("mutability", mutability);
+        ] ->
         let* index = region_id_of_json ctx index in
         let* name = option_of_json string_of_json ctx name in
+        let* variance = variance_of_json ctx variance in
         let* mutability = lifetime_mutability_of_json ctx mutability in
-        Ok ({ index; name; mutability } : region_param)
+        Ok ({ index; name; variance; mutability } : region_param)
     | _ -> Error "")
 
 and rvalue_of_json (ctx : of_json_ctx) (js : json) : (rvalue, string) result =
@@ -1478,10 +1485,11 @@ and type_param_of_json (ctx : of_json_ctx) (js : json) :
     (type_param, string) result =
   combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("index", index); ("name", name) ] ->
+    | `Assoc [ ("index", index); ("name", name); ("variance", variance) ] ->
         let* index = type_var_id_of_json ctx index in
         let* name = string_of_json ctx name in
-        Ok ({ index; name } : type_param)
+        let* variance = variance_of_json ctx variance in
+        Ok ({ index; name; variance } : type_param)
     | _ -> Error "")
 
 and type_pattern_of_json (ctx : of_json_ctx) (js : json) :
@@ -1548,6 +1556,17 @@ and unsizing_metadata_of_json (ctx : of_json_ctx) (js : json) :
     | `String "Unknown" -> Ok MetaUnknown
     | _ -> Error "")
 
+and variance_of_json (ctx : of_json_ctx) (js : json) : (variance, string) result
+    =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `String "Covariant" -> Ok Covariant
+    | `String "Invariant" -> Ok Invariant
+    | `String "Contravariant" -> Ok Contravariant
+    | `String "Bivariant" -> Ok Bivariant
+    | `String "Unknown" -> Ok VaUnknown
+    | _ -> Error "")
+
 and variant_id_of_json (ctx : of_json_ctx) (js : json) :
     (variant_id, string) result =
   combine_error_msgs js __FUNCTION__

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1027,8 +1027,9 @@ and region_param_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
   combine_error_msgs st __FUNCTION__
     (let* index = region_id_of_postcard ctx st in
      let* name = option_of_postcard string_of_postcard ctx st in
+     let* variance = variance_of_postcard ctx st in
      let* mutability = lifetime_mutability_of_postcard ctx st in
-     Ok ({ index; name; mutability } : region_param))
+     Ok ({ index; name; variance; mutability } : region_param))
 
 and rvalue_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
     (rvalue, string) result =
@@ -1327,7 +1328,8 @@ and type_param_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
   combine_error_msgs st __FUNCTION__
     (let* index = type_var_id_of_postcard ctx st in
      let* name = string_of_postcard ctx st in
-     Ok ({ index; name } : type_param))
+     let* variance = variance_of_postcard ctx st in
+     Ok ({ index; name; variance } : type_param))
 
 and type_pattern_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
     (type_pattern, string) result =
@@ -1393,6 +1395,18 @@ and unsizing_metadata_of_postcard (ctx : of_postcard_ctx) (st : postcard_state)
      | 3 -> Ok MetaUnknown
      | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
 
+and variance_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
+    (variance, string) result =
+  combine_error_msgs st __FUNCTION__
+    (let* __tag = int_of_postcard ctx st in
+     match __tag with
+     | 0 -> Ok Covariant
+     | 1 -> Ok Invariant
+     | 2 -> Ok Contravariant
+     | 3 -> Ok Bivariant
+     | 4 -> Ok VaUnknown
+     | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag))
+
 and variant_id_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) :
     (variant_id, string) result =
   combine_error_msgs st __FUNCTION__ (VariantId.id_of_postcard ctx st)

charon-ml/src/generated/Generated_Types.ml

@@ -580,6 +580,7 @@ and region_param = {
       (** Index identifying the variable among other variables bound at the same
           level. *)
   name : string option;  (** Region name *)
+  variance : variance;  (** Variance of this parameter. *)
   mutability : lifetime_mutability;
       (** Whether this lifetime is (recursively) used in a [&'a mut T] type.
           Only [true] if this lifetime parameter belongs to an ADT. This is a
@@ -838,6 +839,7 @@ and type_param = {
       (** Index identifying the variable among other variables bound at the same
           level. *)
   name : string;  (** Variable name *)
+  variance : variance;  (** Variance of this parameter. *)
 }
 
 (** A type-level pattern used by [[TyKind::Pattern]]. *)
@@ -861,6 +863,17 @@ and unsizing_metadata =
           [dyn Trait -> dyn Sized]), we keep the current vtable. *)
   | MetaUnknown
 
+(** The variance of a lifetime or type parameter. *)
+and variance =
+  | Covariant
+  | Invariant
+  | Contravariant
+  | Bivariant
+  | VaUnknown
+      (** Variance was not sensible (e.g. on impls), not available (e.g. on
+          higher-kinded predicates), or not computed (e.g. on parameters that
+          Charon invents). *)
+
 and variant_id = (VariantId.id[@visitors.opaque])
 [@@deriving
   show,

charon/Cargo.toml

@@ -25,7 +25,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.224"
+version = "0.1.225"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/src/ast/types/vars.rs

@@ -100,6 +100,32 @@ generate_index_type!(ConstGenericVarId, "Const");
 generate_index_type!(TraitClauseId, "TraitClause");
 generate_index_type!(TraitTypeConstraintId, "TraitTypeConstraint");
 
+/// The variance of a lifetime or type parameter.
+#[derive(
+    Debug,
+    Clone,
+    Copy,
+    PartialEq,
+    Eq,
+    PartialOrd,
+    Ord,
+    Hash,
+    Serialize,
+    Deserialize,
+    Drive,
+    DriveMut,
+)]
+pub enum Variance {
+    Covariant,
+    Invariant,
+    Contravariant,
+    Bivariant,
+    /// Variance was not sensible (e.g. on impls), not available (e.g. on higher-kinded
+    /// predicates), or not computed (e.g. on parameters that Charon invents).
+    #[cfg_attr(feature = "charon_on_charon", charon::rename("VaUnknown"))]
+    Unknown,
+}
+
 /// A type variable in a signature or binder.
 #[derive(
     Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize, Drive, DriveMut,
@@ -110,6 +136,9 @@ pub struct TypeParam {
     /// Variable name
     #[drive(skip)]
     pub name: String,
+    /// Variance of this parameter.
+    #[drive(skip)]
+    pub variance: Variance,
 }
 
 /// A region variable in a signature or binder.
@@ -122,6 +151,9 @@ pub struct RegionParam {
     /// Region name
     #[drive(skip)]
     pub name: Option<String>,
+    /// Variance of this parameter.
+    #[drive(skip)]
+    pub variance: Variance,
     /// Whether this lifetime is (recursively) used in a `&'a mut T` type. Only `true` if this
     /// lifetime parameter belongs to an ADT. This is a global analysis that looks even into opaque
     /// items. When unsure, err on the side of assuming mutability.
@@ -316,16 +348,21 @@ where
 }
 
 impl TypeParam {
-    pub fn new(index: TypeVarId, name: String) -> Self {
-        Self { index, name }
+    pub fn new(index: TypeVarId, name: String, variance: Variance) -> Self {
+        Self {
+            index,
+            name,
+            variance,
+        }
     }
 }
 
 impl RegionParam {
-    pub fn new(index: RegionId, name: Option<String>) -> Self {
+    pub fn new(index: RegionId, name: Option<String>, variance: Variance) -> Self {
         Self {
             index,
             name,
+            variance,
             mutability: LifetimeMutability::Unknown,
         }
     }

charon/src/bin/charon-driver/hax/rustc_utils.rs

@@ -1,12 +1,145 @@
-use std::collections::HashSet;
+use std::collections::{HashMap, HashSet};
 
 use rustc_hir::def::DefKind as RDefKind;
+use rustc_middle::ty::relate::{
+    Relate, RelateResult, TypeRelation, relate_args_with_variances, structurally_relate_consts,
+    structurally_relate_tys,
+};
 use rustc_middle::{mir, ty};
 use rustc_span::kw;
 use rustc_type_ir::Interner;
 
 use crate::hax::prelude::*;
 
+/// Computes the variance of each region bound by `sig`.
+///
+/// This follows rustc's `FunctionalVariances` helper from the `impl_trait_overcaptures` lint.
+pub fn fn_sig_bound_region_variances<'tcx>(
+    tcx: ty::TyCtxt<'tcx>,
+    sig: ty::PolyFnSig<'tcx>,
+) -> HashMap<ty::BoundVar, ty::Variance> {
+    struct FunctionalVariances<'tcx> {
+        tcx: ty::TyCtxt<'tcx>,
+        variances: HashMap<ty::BoundVar, ty::Variance>,
+        ambient_variance: ty::Variance,
+        target_binder: ty::DebruijnIndex,
+    }
+
+    impl<'tcx> TypeRelation<ty::TyCtxt<'tcx>> for FunctionalVariances<'tcx> {
+        fn cx(&self) -> ty::TyCtxt<'tcx> {
+            self.tcx
+        }
+
+        fn relate_ty_args(
+            &mut self,
+            a_ty: ty::Ty<'tcx>,
+            _: ty::Ty<'tcx>,
+            def_id: rustc_hir::def_id::DefId,
+            a_args: ty::GenericArgsRef<'tcx>,
+            b_args: ty::GenericArgsRef<'tcx>,
+            _: impl FnOnce(ty::GenericArgsRef<'tcx>) -> ty::Ty<'tcx>,
+        ) -> RelateResult<'tcx, ty::Ty<'tcx>> {
+            relate_args_with_variances(self, self.tcx.variances_of(def_id), a_args, b_args)?;
+            Ok(a_ty)
+        }
+
+        fn relate_with_variance<T: Relate<ty::TyCtxt<'tcx>>>(
+            &mut self,
+            variance: ty::Variance,
+            _: ty::VarianceDiagInfo<ty::TyCtxt<'tcx>>,
+            a: T,
+            b: T,
+        ) -> RelateResult<'tcx, T> {
+            let old_variance = self.ambient_variance;
+            self.ambient_variance = self.ambient_variance.xform(variance);
+            let result = self.relate(a, b);
+            self.ambient_variance = old_variance;
+            result
+        }
+
+        fn tys(&mut self, a: ty::Ty<'tcx>, b: ty::Ty<'tcx>) -> RelateResult<'tcx, ty::Ty<'tcx>> {
+            structurally_relate_tys(self, a, b)
+        }
+
+        fn regions(
+            &mut self,
+            a: ty::Region<'tcx>,
+            _: ty::Region<'tcx>,
+        ) -> RelateResult<'tcx, ty::Region<'tcx>> {
+            if let ty::ReBound(ty::BoundVarIndexKind::Bound(binder), ty::BoundRegion { var, .. }) =
+                a.kind()
+                && binder == self.target_binder
+            {
+                self.variances
+                    .entry(var)
+                    .and_modify(|old| *old = unify_variances(*old, self.ambient_variance))
+                    .or_insert(self.ambient_variance);
+            }
+            Ok(a)
+        }
+
+        fn consts(
+            &mut self,
+            a: ty::Const<'tcx>,
+            b: ty::Const<'tcx>,
+        ) -> RelateResult<'tcx, ty::Const<'tcx>> {
+            structurally_relate_consts(self, a, b)
+        }
+
+        fn binders<T>(
+            &mut self,
+            a: ty::Binder<'tcx, T>,
+            b: ty::Binder<'tcx, T>,
+        ) -> RelateResult<'tcx, ty::Binder<'tcx, T>>
+        where
+            T: Relate<ty::TyCtxt<'tcx>>,
+        {
+            let old_target_binder = self.target_binder;
+            self.target_binder = self.target_binder.shifted_in(1);
+            let result = self.relate(a.skip_binder(), b.skip_binder());
+            self.target_binder = old_target_binder;
+            result?;
+            Ok(a)
+        }
+    }
+
+    fn unify_variances(a: ty::Variance, b: ty::Variance) -> ty::Variance {
+        match (a, b) {
+            (ty::Bivariant, other) | (other, ty::Bivariant) => other,
+            (ty::Invariant, _) | (_, ty::Invariant) => ty::Invariant,
+            (ty::Contravariant, ty::Covariant) | (ty::Covariant, ty::Contravariant) => {
+                ty::Invariant
+            }
+            (ty::Contravariant, ty::Contravariant) => ty::Contravariant,
+            (ty::Covariant, ty::Covariant) => ty::Covariant,
+        }
+    }
+
+    let mut relation = FunctionalVariances {
+        tcx,
+        variances: HashMap::new(),
+        // `Relate for FnSig` makes inputs contravariant. We are computing the variance of the
+        // signature's own bound parameters, so cancel that outer function-type variance. Nested
+        // function types still introduce their own contravariance as usual.
+        ambient_variance: ty::Contravariant,
+        target_binder: ty::INNERMOST,
+    };
+    relation
+        .relate(sig.skip_binder(), sig.skip_binder())
+        .expect("a signature must relate to itself");
+
+    // A bound region that does not occur in the signature is bivariant.
+    for (index, var) in sig.bound_vars().iter().enumerate() {
+        if matches!(var, ty::BoundVariableKind::Region(_)) {
+            relation
+                .variances
+                .entry(ty::BoundVar::from_usize(index))
+                .or_insert(ty::Bivariant);
+        }
+    }
+    relation.variances
+}
+
 pub fn inst_binder<'tcx, T>(
     tcx: ty::TyCtxt<'tcx>,
     typing_env: ty::TypingEnv<'tcx>,