Merge pull request #1052 from hacspec/fix-1042

fix(exporter/thir): fix #1048
cryspen · Oct 28, 2024 · 9559048 · 9559048
2 parents 2054cee + 5c79ab3
commit 9559048
Show file tree

Hide file tree

Showing 4 changed files with 55 additions and 8 deletions.
diff --git a/frontend/exporter/src/types/thir.rs b/frontend/exporter/src/types/thir.rs
@@ -579,8 +579,7 @@ pub enum ExprKind {
     #[map({
         let e = gstate.thir().exprs[*fun].unroll_scope(gstate);
         let (generic_args, r#trait, bounds_impls);
-        // A function is any expression whose type is something callable
-        let fun = match ty.kind() {
+        let fun = match e.ty.kind() {
             rustc_middle::ty::TyKind::FnDef(def_id, generics) => {
                 let (hir_id, attributes) = e.hir_id_and_attributes(gstate);
                 let hir_id = hir_id.map(|hir_id| hir_id.index());
@@ -613,11 +612,15 @@ pub enum ExprKind {
                 r#trait = None; // A function pointer is not a method
                 e.sinto(gstate)
             },
-            ty_kind => supposely_unreachable_fatal!(
-                gstate[e.span],
-                "CallNotTyFnDef";
-                {e, ty_kind}
-            )
+            ty_kind => {
+                let ty_norm: Ty = gstate.base().tcx.normalize_erasing_regions(gstate.param_env(), *ty).sinto(gstate);
+                let ty_kind_sinto = ty_kind.sinto(gstate);
+                supposely_unreachable_fatal!(
+                    gstate[e.span],
+                    "CallNotTyFnDef";
+                    {e, ty_kind, ty_kind_sinto, ty_norm}
+                );
+            }
         };
         TO_TYPE::Call {
             ty: ty.sinto(gstate),

diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap
@@ -26,6 +26,34 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Functions.Issue_1048_.fst" = '''
+module Functions.Issue_1048_
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+type t_CallableViaDeref = | CallableViaDeref : t_CallableViaDeref
+
+[@@ FStar.Tactics.Typeclasses.tcinstance]
+let impl: Core.Ops.Deref.t_Deref t_CallableViaDeref =
+  {
+    f_Target = Prims.unit -> bool;
+    f_deref_pre = (fun (self: t_CallableViaDeref) -> true);
+    f_deref_post = (fun (self: t_CallableViaDeref) (out: (Prims.unit -> bool)) -> true);
+    f_deref
+    =
+    fun (self: t_CallableViaDeref) ->
+      fun temp_0_ ->
+        let _:Prims.unit = temp_0_ in
+        true
+  }
+
+let call_via_deref (_: Prims.unit) : bool =
+  Core.Ops.Deref.f_deref #t_CallableViaDeref
+    #FStar.Tactics.Typeclasses.solve
+    (CallableViaDeref <: t_CallableViaDeref)
+    ()
+'''
 "Functions.fst" = '''
 module Functions
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"

diff --git a/tests/functions/Cargo.toml b/tests/functions/Cargo.toml
@@ -7,4 +7,4 @@ edition = "2021"
 hax-lib = { path = "../../hax-lib" }
 
 [package.metadata.hax-tests]
-into."fstar+coq" = { snapshot = "stdout" }
+into."fstar" = { snapshot = "stdout" }
diff --git a/tests/functions/src/lib.rs b/tests/functions/src/lib.rs
@@ -4,3 +4,19 @@ fn calling_function_pointer() {
     let f_ptr = f::<i32>;
     f_ptr();
 }
+
+mod issue_1048 {
+    pub struct CallableViaDeref;
+
+    impl core::ops::Deref for CallableViaDeref {
+        type Target = fn() -> bool;
+
+        fn deref(&self) -> &Self::Target {
+            &((|| true) as fn() -> bool)
+        }
+    }
+
+    pub fn call_via_deref() -> bool {
+        CallableViaDeref()
+    }
+}