fix(engine/lib): import associated item projection on generic bounds

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -1337,6 +1337,10 @@ struct
                       | _ -> .)
                     args ) );
         ]
+    | GCProjection _ ->
+        Error.unimplemented ~issue_id:549
+          ~details:"Projections of an associated type is not yet supported."
+          span
     | _ -> .
 
   let pgeneric (span : Ast.span) (generics : AST.generics) :

engine/backends/fstar/fstar_backend.ml

@@ -656,11 +656,14 @@ struct
       | GCLifetime _ -> .
       | GCType { goal; name } ->
           let typ = c_trait_goal span goal in
-          { kind = Tcresolve; ident = F.id name; typ }
+          Some { kind = Tcresolve; ident = F.id name; typ }
+      | GCProjection _ ->
+          (* TODO: Not yet implemented, see https://github.com/hacspec/hax/issues/785 *)
+          None
 
     let of_generics span generics : t list =
       List.map ~f:(of_generic_param span) generics.params
-      @ List.mapi ~f:(of_generic_constraint span) generics.constraints
+      @ List.filter_mapi ~f:(of_generic_constraint span) generics.constraints
 
     let of_typ span (nth : int) typ : t =
       let ident = F.id ("x" ^ Int.to_string nth) in
@@ -1278,13 +1281,16 @@ struct
         in
         let constraints_fields : FStar_Parser_AST.tycon_record =
           generics.constraints
-          |> List.map ~f:(fun c ->
-                 let bound, id =
-                   match c with GCType { goal; name } -> (goal, name) | _ -> .
-                 in
-                 let name = "_super_" ^ id in
-                 let typ = pgeneric_constraint_type e.span c in
-                 (F.id name, None, [ F.Attrs.no_method ], typ))
+          |> List.filter_map ~f:(fun c ->
+                 match c with
+                 | GCType { goal = bound; name = id } ->
+                     let name = "_super_" ^ id in
+                     let typ = pgeneric_constraint_type e.span c in
+                     Some (F.id name, None, [ F.Attrs.no_method ], typ)
+                 | GCProjection _ ->
+                     (* TODO: Not yet implemented, see https://github.com/hacspec/hax/issues/785 *)
+                     None
+                 | _ -> .)
         in
         let fields : FStar_Parser_AST.tycon_record =
           constraints_fields @ fields

engine/lib/ast.ml

@@ -164,8 +164,22 @@ functor
               {- An argument that introduces a variable [name] that inhabits [goal].}
           }
       *)
-    (* TODO: ADD SPAN! *)
 
+    and projection_predicate = {
+      impl : impl_expr;
+      assoc_item : concrete_ident;
+      typ : ty;
+    }
+    (** Expresses a constraints over an associated type.
+        For instance:
+        [
+        fn f<T : Foo<S = String>>(...)
+                    ^^^^^^^^^^
+        ]
+        (provided the trait `Foo` has an associated type `S`).
+      *)
+
+    (* TODO: ADD SPAN! *)
     and pat' =
       | PWild
       | PAscription of { typ : ty; typ_span : span; pat : pat }
@@ -335,6 +349,7 @@ functor
     and generic_constraint =
       | GCLifetime of todo * F.lifetime
       | GCType of impl_ident
+      | GCProjection of projection_predicate
           (** Trait or lifetime constraints. For instance, `A` and `B` in
     `fn f<T: A + B>()`. *)
     [@@deriving show, yojson, hash, eq]

engine/lib/concrete_ident/impl_infos.ml

@@ -32,6 +32,7 @@ let lookup span (impl : Concrete_ident.t) : t option =
       Import_thir.import_clause span binder
     in
     List.filter_map ~f clauses
-    |> List.map ~f:(fun (i : Ast.Rust.impl_ident) -> i.goal)
+    |> List.filter_map ~f:(fun (c : Ast.Rust.generic_constraint) ->
+           match c with GCType i -> Some i.goal | _ -> None)
   in
   Some { trait_goal; typ; clauses }

engine/lib/import_thir.ml

@@ -229,7 +229,7 @@ module type EXPR = sig
   val c_trait_item' : Thir.trait_item -> Thir.trait_item_kind -> trait_item'
   val c_trait_ref : Thir.span -> Thir.trait_ref -> trait_goal
   val c_impl_expr : Thir.span -> Thir.impl_expr -> impl_expr
-  val c_clause : Thir.span -> Thir.clause -> impl_ident option
+  val c_clause : Thir.span -> Thir.clause -> generic_constraint option
 end
 
 (* BinOp to [core::ops::*] overloaded functions *)
@@ -1086,15 +1086,23 @@ end) : EXPR = struct
     let attrs = c_attrs param.attributes in
     { ident; span; attrs; kind }
 
-  let c_clause_kind span id (kind : Thir.clause_kind) : impl_ident option =
+  let c_clause_kind span id (kind : Thir.clause_kind) :
+      generic_constraint option =
     match kind with
     | Trait { is_positive = true; trait_ref } ->
         let args = List.map ~f:(c_generic_value span) trait_ref.generic_args in
         let trait = Concrete_ident.of_def_id Trait trait_ref.def_id in
-        Some { goal = { trait; args }; name = id }
+        Some (GCType { goal = { trait; args }; name = id })
+    | Projection { impl_expr; assoc_item; ty } ->
+        let impl = c_impl_expr span impl_expr in
+        let assoc_item =
+          Concrete_ident.of_def_id (AssociatedItem Type) assoc_item.def_id
+        in
+        let typ = c_ty span ty in
+        Some (GCProjection { impl; assoc_item; typ })
     | _ -> None
 
-  let c_clause span (p : Thir.clause) : impl_ident option =
+  let c_clause span (p : Thir.clause) : generic_constraint option =
     let ({ kind; id } : Thir.clause) = p in
     c_clause_kind span id kind.value
 
@@ -1109,10 +1117,7 @@ end) : EXPR = struct
     aux []
 
   let c_generics (generics : Thir.generics) : generics =
-    let bounds =
-      List.filter_map ~f:(c_clause generics.span) generics.bounds
-      |> List.map ~f:(fun impl_ident -> GCType impl_ident)
-    in
+    let bounds = List.filter_map ~f:(c_clause generics.span) generics.bounds in
     {
       params = List.map ~f:c_generic_param generics.params;
       constraints = bounds |> list_dedup equal_generic_constraint;
@@ -1139,7 +1144,11 @@ end) : EXPR = struct
         in
         TIFn (TArrow (inputs, output))
     | Type (bounds, None) ->
-        let bounds = List.filter_map ~f:(c_clause span) bounds in
+        let bounds =
+          List.filter_map ~f:(c_clause span) bounds
+          |> List.filter_map ~f:(fun bound ->
+                 match bound with GCType impl -> Some impl | _ -> None)
+        in
         TIType bounds
     | Type (_, Some _) ->
         unimplemented [ span ]
@@ -1156,7 +1165,8 @@ include struct
   let import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal =
     c_trait_ref
 
-  let import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option =
+  let import_clause :
+      Types.span -> Types.clause -> Ast.Rust.generic_constraint option =
     c_clause
 end
 
@@ -1577,9 +1587,13 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                                  parent_bounds =
                                    List.filter_map
                                      ~f:(fun (clause, impl_expr, span) ->
-                                       let* trait_goal = c_clause span clause in
-                                       Some
-                                         (c_impl_expr span impl_expr, trait_goal))
+                                       let* bound = c_clause span clause in
+                                       match bound with
+                                       | GCType trait_goal ->
+                                           Some
+                                             ( c_impl_expr span impl_expr,
+                                               trait_goal )
+                                       | _ -> None)
                                      parent_bounds;
                                });
                        ii_ident;
@@ -1589,8 +1603,11 @@ and c_item_unwrapped ~ident ~drop_body (item : Thir.item) : item list =
                parent_bounds =
                  List.filter_map
                    ~f:(fun (clause, impl_expr, span) ->
-                     let* trait_goal = c_clause span clause in
-                     Some (c_impl_expr span impl_expr, trait_goal))
+                     let* bound = c_clause span clause in
+                     match bound with
+                     | GCType trait_goal ->
+                         Some (c_impl_expr span impl_expr, trait_goal)
+                     | _ -> None)
                    parent_bounds;
              }
     | Use ({ span = _; res; segments; rename }, _) ->

engine/lib/import_thir.mli

@@ -1,6 +1,8 @@
 val import_ty : Types.span -> Types.ty -> Ast.Rust.ty
 val import_trait_ref : Types.span -> Types.trait_ref -> Ast.Rust.trait_goal
-val import_clause : Types.span -> Types.clause -> Ast.Rust.impl_ident option
+
+val import_clause :
+  Types.span -> Types.clause -> Ast.Rust.generic_constraint option
 
 val import_item :
   drop_body:bool ->

engine/lib/phases/phase_drop_references.ml

@@ -135,11 +135,21 @@ struct
       in
       Some B.{ ident; kind; attrs; span }
 
+    and dprojection_predicate (span : span) (r : A.projection_predicate) :
+        B.projection_predicate =
+      {
+        impl = dimpl_expr span r.impl;
+        assoc_item = r.assoc_item;
+        typ = dty span r.typ;
+      }
+
     let dgeneric_constraint (span : span) (p : A.generic_constraint) :
         B.generic_constraint option =
       match p with
       | GCLifetime _ -> None
       | GCType idents -> Some (B.GCType (dimpl_ident span idents))
+      | GCProjection projection ->
+          Some (B.GCProjection (dprojection_predicate span projection))
 
     let dgenerics (span : span) (g : A.generics) : B.generics =
       {

engine/lib/print_rust.ml

@@ -397,6 +397,10 @@ module Raw = struct
     match p with
     | GCLifetime _ -> !"'unk: 'unk"
     | GCType { goal; _ } -> !"_:" & ptrait_goal span goal
+    | GCProjection { assoc_item; typ; _ } ->
+        !"_:_<_>::"
+        & !(Concrete_ident_view.show assoc_item)
+        & !"==" & pty span typ
 
   let pgeneric_constraints span (constraints : generic_constraint list) =
     if List.is_empty constraints then empty

engine/lib/subtype.ml

@@ -54,6 +54,14 @@ struct
   and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident =
     { goal = dtrait_goal span r.goal; name = r.name }
 
+  and dprojection_predicate (span : span) (r : A.projection_predicate) :
+      B.projection_predicate =
+    {
+      impl = dimpl_expr span r.impl;
+      assoc_item = r.assoc_item;
+      typ = dty span r.typ;
+    }
+
   and dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr =
     match i with
     | Self -> Self
@@ -343,6 +351,8 @@ struct
       match generic_constraint with
       | GCLifetime (lf, witness) -> B.GCLifetime (lf, S.lifetime span witness)
       | GCType impl_ident -> B.GCType (dimpl_ident span impl_ident)
+      | GCProjection projection ->
+          B.GCProjection (dprojection_predicate span projection)
 
     let dgenerics (span : span) (g : A.generics) : B.generics =
       {