fix(engine/backend): import trait goal in concrete impl_expr

engine/backends/fstar/fstar_backend.ml

@@ -343,7 +343,7 @@ struct
     let some = Option.some in
     let hax_unstable_impl_exprs = false in
     match ie with
-    | Concrete tr -> c_trait_goal span tr |> some
+    | Concrete { impl = tr; _ } -> c_trait_goal span tr |> some
     | LocalBound { id } ->
         let local_ident =
           Local_ident.{ name = id; id = Local_ident.mk_id Expr 0 }

engine/lib/ast.ml

@@ -143,7 +143,7 @@ functor
 
     and impl_expr =
       | Self
-      | Concrete of trait_goal
+      | Concrete of { trait : trait_goal; impl : trait_goal }
       | LocalBound of { id : string }
       | Parent of { impl : impl_expr; ident : impl_ident }
       | Projection of {

engine/lib/import_thir.ml

@@ -1026,7 +1026,7 @@ end) : EXPR = struct
   (* fun _ -> Ok Bool *)
 
   and c_impl_expr (span : Thir.span) (ie : Thir.impl_expr) : impl_expr =
-    let impl = c_impl_expr_atom span ie.impl in
+    let impl = c_impl_expr_atom span ie.trait ie.impl in
     match ie.args with
     | [] -> impl
     | args ->
@@ -1038,8 +1038,8 @@ end) : EXPR = struct
     let args = List.map ~f:(c_generic_value span) tr.generic_args in
     { trait; args }
 
-  and c_impl_expr_atom (span : Thir.span) (ie : Thir.impl_expr_atom) : impl_expr
-      =
+  and c_impl_expr_atom (span : Thir.span) (trait : Types.trait_ref)
+      (ie : Thir.impl_expr_atom) : impl_expr =
     let browse_path (impl : impl_expr) (chunk : Thir.impl_expr_path_chunk) =
       match chunk with
       | AssocItem
@@ -1062,9 +1062,13 @@ end) : EXPR = struct
     in
     match ie with
     | Concrete { id; generics } ->
-        let trait = Concrete_ident.of_def_id Impl id in
-        let args = List.map ~f:(c_generic_value span) generics in
-        Concrete { trait; args }
+        let trait = c_trait_ref span trait in
+        let impl =
+          let trait = Concrete_ident.of_def_id Impl id in
+          let args = List.map ~f:(c_generic_value span) generics in
+          { trait; args }
+        in
+        Concrete { trait; impl }
     | LocalBound { predicate_id; path; _ } ->
         let init = LocalBound { id = predicate_id } in
         List.fold ~init ~f:browse_path path

engine/lib/phases/phase_reconstruct_question_marks.ml

@@ -53,7 +53,10 @@ module%inlined_contents Make (FA : Features.T) = struct
       let expect_residual_impl_result (impl : impl_expr) : impl_expr option =
         match impl with
         | ImplApp
-            { impl = Concrete { trait; _ }; args = [ _; _; _; from_impl ] }
+            {
+              impl = Concrete { impl = { trait; _ }; _ };
+              args = [ _; _; _; from_impl ];
+            }
           when Concrete_ident.eq_name Core__result__Impl_27 trait ->
             Some from_impl
         | _ -> None

engine/lib/phases/phase_simplify_question_marks.ml

@@ -53,7 +53,10 @@ module%inlined_contents Make (FA : Features.T) = struct
       let expect_residual_impl_result (impl : impl_expr) : impl_expr option =
         match impl with
         | ImplApp
-            { impl = Concrete { trait; _ }; args = [ _; _; _; from_impl ] }
+            {
+              impl = Concrete { impl = { trait; _ }; _ };
+              args = [ _; _; _; from_impl ];
+            }
           when Concrete_ident.eq_name Core__result__Impl_27 trait ->
             Some from_impl
         | _ -> None

engine/lib/subtype.ml

@@ -80,7 +80,9 @@ struct
   and dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr =
     match i with
     | Self -> Self
-    | Concrete tr -> Concrete (dtrait_goal span tr)
+    | Concrete { trait; impl } ->
+        Concrete
+          { trait = dtrait_goal span trait; impl = dtrait_goal span impl }
     | LocalBound { id } -> LocalBound { id }
     | Parent { impl; ident } ->
         Parent { impl = dimpl_expr span impl; ident = dimpl_ident span ident }

test-harness/src/snapshots/toolchain__traits into-fstar.snap

@@ -195,6 +195,7 @@ let _ =
   (* This module has implicit dependencies, here we make them explicit. *)
   (* The implicit dependencies arise from typeclasses instances. *)
   let open Traits.Implicit_dependencies_issue_667_.Impl_type in
+  let open Traits.Implicit_dependencies_issue_667_.Trait_definition in
   ()
 
 let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit =