Repository: cryspen/hax (language: rust)

Issue:
Question mark simplification phase: inserts no type arguments on `from` call
```rust
trait MyFrom<T> {
    fn my_from(x: T) -> Self;
}

impl MyFrom<u8> for u16 {
    fn my_from(x: u8) -> u16 {
        x as u16
    }
}

fn f(x: u8) -> Result<u16, u16> {
    Err(1u8)?;
    Ok(u16::my_from(x))
}
```
[Open this code snippet in the playground](https://hax-playground.cryspen.com/#fstar/d3313f9a7f/gist=30ce570dd9fa0a43e8176a3d4949f893)



Discussion / hints:

Fix patch:
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 26e826bbf..1c149404f 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -890,7 +890,8 @@ module Make (F : Features.T) = struct
         (Concrete_ident.of_name (Constructor { is_struct }) constructor_name))
       is_struct args span ret_typ
 
-  let call' ?impl f (args : expr list) span ret_typ =
+  let call' ?impl f ?(generic_args = []) ?(impl_generic_args = [])
+      (args : expr list) span ret_typ =
     let typ = TArrow (List.map ~f:(fun arg -> arg.typ) args, ret_typ) in
     let e = GlobalVar f in
     {
@@ -899,17 +900,18 @@ module Make (F : Features.T) = struct
           {
             f = { e; typ; span };
             args;
-            generic_args = [];
+            generic_args;
             bounds_impls = [];
-            trait = Option.map ~f:(fun impl -> (impl, [])) impl;
+            trait = Option.map ~f:(fun impl -> (impl, impl_generic_args)) impl;
           };
       typ = ret_typ;
       span;
     }
 
-  let call ?(kind : Concrete_ident.Kind.t = Value) ?impl
-      (f_name : Concrete_ident.name) (args : expr list) span ret_typ =
-    call' ?impl
+  let call ?(kind : Concrete_ident.Kind.t = Value) ?(generic_args = [])
+      ?(impl_generic_args = []) ?impl (f_name : Concrete_ident.name)
+      (args : expr list) span ret_typ =
+    call' ?impl ~generic_args ~impl_generic_args
       (`Concrete (Concrete_ident.of_name kind f_name))
       args span ret_typ
 
diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml
index 87ae111a4..3cda9ad7f 100644
--- a/engine/lib/phases/phase_simplify_question_marks.ml
+++ b/engine/lib/phases/phase_simplify_question_marks.ml
@@ -87,9 +87,10 @@ module%inlined_contents Make (FA : Features.T) = struct
         let* impl = expect_residual_impl_result impl in
         let*? _ = [%eq: ty] error_src error_dest |> not in
         let from_typ = TArrow ([ error_src ], error_dest) in
+        let impl_generic_args = [ GType error_dest; GType error_src ] in
         Some
-          (UA.call ~kind:(AssociatedItem Value) ~impl Core__convert__From__from
-             [ e ] e.span from_typ)
+          (UA.call ~impl_generic_args ~kind:(AssociatedItem Value) ~impl
+             Core__convert__From__from [ e ] e.span from_typ)
 
       (** [map_err e error_dest impl] creates the expression
       [e.map_err(from)] with the proper types and impl


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index a75b44a71..e03cc7117 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
@@ -27,6 +27,37 @@ stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
 diagnostics = []
 
 [stdout.files]
+"Side_effects.Issue_1083_.fst" = '''
+module Side_effects.Issue_1083_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+class t_MyFrom (v_Self: Type0) (v_T: Type0) = {
+  f_my_from_pre:v_T -> Type0;
+  f_my_from_post:v_T -> v_Self -> Type0;
+  f_my_from:x0: v_T -> Prims.Pure v_Self (f_my_from_pre x0) (fun result -> f_my_from_post x0 result)
+}
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: t_MyFrom u16 u8 =
+  {
+    f_my_from_pre = (fun (x: u8) -> true);
+    f_my_from_post = (fun (x: u8) (out: u16) -> true);
+    f_my_from = fun (x: u8) -> cast (x <: u8) <: u16
+  }
+
+let f (x: u8) : Core.Result.t_Result u16 u16 =
+  match Core.Result.Result_Err 1uy <: Core.Result.t_Result Prims.unit u8 with
+  | Core.Result.Result_Ok _ ->
+    Core.Result.Result_Ok (f_my_from #u16 #u8 #FStar.Tactics.Typeclasses.solve x)
+    <:
+    Core.Result.t_Result u16 u16
+  | Core.Result.Result_Err err ->
+    Core.Result.Result_Err (Core.Convert.f_from #u16 #u8 #FStar.Tactics.Typeclasses.solve err)
+    <:
+    Core.Result.t_Result u16 u16
+'''
 "Side_effects.fst" = '''
 module Side_effects
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -156,7 +187,7 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
   match y with
   | Core.Result.Result_Ok hoist1 -> Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err ->
-    Core.Result.Result_Err (Core.Convert.f_from #FStar.Tactics.Typeclasses.solve err)
+    Core.Result.Result_Err (Core.Convert.f_from #u32 #u16 #FStar.Tactics.Typeclasses.solve err)
     <:
     Core.Result.t_Result i8 u32
 
@@ -397,7 +428,7 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
         <:
         Core.Result.t_Result u32 u32
       | Core.Result.Result_Err err ->
-        Core.Result.Result_Err (Core.Convert.f_from #FStar.Tactics.Typeclasses.solve err)
+        Core.Result.Result_Err (Core.Convert.f_from #u32 #u8 #FStar.Tactics.Typeclasses.solve err)
         <:
         Core.Result.t_Result u32 u32
     else
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
index 401de5fc8..80a576172 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
+++ b/test-harness/src/snapshots/toolchain__side-effects into-ssprove.snap
@@ -126,6 +126,8 @@ Notation "'Build_t_Foo' '[' x ']' '(' 'f_bar' ':=' y ')'" := (Build_t_Foo (f_x :
 
 (*Not implemented yet? todo(item)*)
 
+(*Not implemented yet? todo(item)*)
+
 Equations add3 {L1 : {fset Location}} {L2 : {fset Location}} {L3 : {fset Location}} {I1 : Interface} {I2 : Interface} {I3 : Interface} (x : both L1 I1 int32) (y : both L2 I2 int32) (z : both L3 I3 int32) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32 :=
   add3 x y z  :=
     solve_lift (impl__u32__wrapping_add (impl__u32__wrapping_add x y) z) : both (L1 :|: L2 :|: L3) (I1 :|: I2 :|: I3) int32.
@@ -301,3 +303,49 @@ Equations simplifiable_return {L1 : {fset Location}} {L2 : {fset Location}} {L3
     ControlFlow_Continue x)) : both (L1 :|: L2 :|: L3 :|: fset [x_loc]) (I1 :|: I2 :|: I3) int32.
 Fail Next Obligation.
 '''
+"Side_effects_Issue_1083_.v" = '''
+(* File automatically generated by Hacspec *)
+Set Warnings "-notation-overridden,-ambiguous-paths".
+From Crypt Require Import choice_type Package Prelude.
+Import PackageNotation.
+From extructures Require Import ord fset.
+From mathcomp Require Import word_ssrZ word.
+From Jasmin Require Import word.
+
+From Coq Require Import ZArith.
+From Coq Require Import Strings.String.
+Import List.ListNotations.
+Open Scope list_scope.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+From Hacspec Require Import ChoiceEquality.
+From Hacspec Require Import LocationUtility.
+From Hacspec Require Import Hacspec_Lib_Comparable.
+From Hacspec Require Import Hacspec_Lib_Pre.
+From Hacspec Require Import Hacspec_Lib.
+
+Open Scope hacspec_scope.
+Import choice.Choice.Exports.
+
+Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations.
+
+Class t_MyFrom (Self : choice_type) := {
+  f_my_from_loc : {fset Location} ;
+  f_my_from : (forall {L1 I1}, both L1 I1 v_T -> both (L1 :|: f_my_from_loc) I1 v_Self) ;
+}.
+Hint Unfold f_my_from_loc.
+
+#[global] Program Instance int16_t_MyFrom : t_MyFrom int16 int8 :=
+  let f_my_from := fun  {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) => solve_lift (cast_int (WS2 := _) x) : both (L1 :|: fset []) I1 int16 in
+  {| f_my_from_loc := (fset [] : {fset Location});
+  f_my_from := (@f_my_from)|}.
+Fail Next Obligation.
+Hint Unfold int16_t_MyFrom.
+
+Equations f {L1 : {fset Location}} {I1 : Interface} (x : both L1 I1 int8) : both L1 I1 (t_Result int16 int16) :=
+  f x  :=
+    solve_lift (run (letm[choice_typeMonad.result_bind_code int16] _ := impl__map_err (Result_Err (ret_both (1 : int8))) f_from in
+    Result_Ok (Result_Ok (f_my_from x)))) : both L1 I1 (t_Result int16 int16).
+Fail Next Obligation.
+'''
diff --git a/tests/side-effects/src/lib.rs b/tests/side-effects/src/lib.rs
index 7bef76cb4..c7db53f22 100644
--- a/tests/side-effects/src/lib.rs
+++ b/tests/side-effects/src/lib.rs
@@ -156,3 +156,20 @@ fn assign_non_trivial_lhs(mut foo: Foo) -> Foo {
     foo.y.1[3].b.0[5].0 = true;
     foo
 }
+
+mod issue_1083 {
+    trait MyFrom<T> {
+        fn my_from(x: T) -> Self;
+    }
+
+    impl MyFrom<u8> for u16 {
+        fn my_from(x: u8) -> u16 {
+            x as u16
+        }
+    }
+
+    fn f(x: u8) -> Result<u16, u16> {
+        Err(1u8)?;
+        Ok(u16::my_from(x))
+    }
+}