diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 2a515162b..28d187185 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -865,7 +865,7 @@ end) : EXPR = struct
 
   and c_pointer e typ span cast source =
     match cast with
-    | ReifyFnPointer ->
+    | ClosureFnPointer Normal | ReifyFnPointer ->
         (* we have arrow types, we do not distinguish between top-level functions and closures *)
         (c_expr source).e
     | Unsize ->
diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap
index 8cce81b2b..f1ba1ef5d 100644
--- a/test-harness/src/snapshots/toolchain__literals into-coq.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap	
@@ -53,6 +53,11 @@ Definition casts (x8 : int8) (x16 : int16) (x32 : int32) (x64 : int64) (xs : uin
   let (_ : int8) := ((((cast x8).+(cast x16)).+(cast x32)).+(cast x64)).+(cast xs) : int8 in
   tt.
 
+Definition fn_pointer_cast (_ : unit) : unit :=
+  let (f : int32 -> int32) := fun x =>
+      x : int32 -> int32 in
+  tt.
+
 Definition numeric (_ : unit) : unit :=
   let (_ : uint_size) := (@repr WORDSIZE32 123) : uint_size in
   let (_ : uint_size) := (@repr WORDSIZE32 42) : uint_size in
diff --git a/test-harness/src/snapshots/toolchain__literals into-fstar.snap b/test-harness/src/snapshots/toolchain__literals into-fstar.snap
index 3851e91eb..15c8b19b3 100644
--- a/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__literals into-fstar.snap	
@@ -104,6 +104,11 @@ let casts (x8: u8) (x16: u16) (x32: u32) (x64: u64) (xs: usize) : Prims.unit =
   in
   ()
 
+/// https://github.com/hacspec/hax/issues/500
+let fn_pointer_cast (_: Prims.unit) : Prims.unit =
+  let (f: (u32 -> u32)): u32 -> u32 = fun x -> x in
+  ()
+
 let numeric (_: Prims.unit) : Prims.unit =
   let (_: usize):usize = sz 123 in
   let (_: isize):isize = isz (-42) in
diff --git a/tests/literals/src/lib.rs b/tests/literals/src/lib.rs
index 1d522c7fc..b82e937f0 100644
--- a/tests/literals/src/lib.rs
+++ b/tests/literals/src/lib.rs
@@ -76,3 +76,8 @@ fn casts(x8: u8, x16: u16, x32: u32, x64: u64, xs: usize) {
 pub fn empty_array() {
     let _: &[u8] = &[];
 }
+
+/// https://github.com/hacspec/hax/issues/500
+fn fn_pointer_cast() {
+    let f: fn(&u32) -> &u32 = |x| x;
+}