Repository: cryspen/hax (language: rust)

Issue:
Frontend: supposely unreachable place: `CallNotTyFnDef`
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e137,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] },
                  temp_lifetime: Some(
                      Node(141),
                  ),
                  span: src/word_splitters.rs:165:52: 165:65 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] }
   --> src/word_splitters.rs:165:52
    |
165 |             WordSplitter::Custom(splitter_func) => splitter_func(word),
    |                                                    ^^^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```



<details><summary>Crate `textwrap@0.16.1`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e137,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] },
                  temp_lifetime: Some(
                      Node(141),
                  ),
                  span: src/word_splitters.rs:165:52: 165:65 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] }
   --> src/word_splitters.rs:165:52
    |
165 |             WordSplitter::Custom(splitter_func) => splitter_func(word),
    |                                                    ^^^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `combine@4.6.7`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e0,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), "'_") mut Input/#0) -> std::result::Result<(O/#1, error::Commit<()>), error::Commit<error::Tracked<Alias(Projection, AliasTy { args: [Input/#0], def_id: DefId(0:1131 ~ combine[01d7]::stream::StreamOnce::Error), .. })>>>, bound_vars: [Region(BrNamed(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), '_))] },
                  temp_lifetime: Some(
                      Node(13),
                  ),
                  span: src/parser/function.rs:92:9: 92:13 (#0),
              }
               - ty_kind: &'{erased} mut Binder { value: fn(&'^0.Named(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), "'_") mut Input/#0) -> std::result::Result<(O/#1, error::Commit<()>), error::Commit<error::Tracked<Alias(Projection, AliasTy { args: [Input/#0], def_id: DefId(0:1131 ~ combine[01d7]::stream::StreamOnce::Error), .. })>>>, bound_vars: [Region(BrNamed(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), '_))] }
  --> src/parser/function.rs:92:9
   |
92 |         self(input).into()
   |         ^^^^
   |
   = note: ⚠️ This is a bug in Hax's frontend.
           Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `yansi@1.0.1`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e3,
                  },
                  ty: Binder { value: fn() -> bool, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(12),
                  ),
                  span: src/style.rs:136:41: 136:42 (#0),
              }
               - ty_kind: condition::Condition
   --> src/style.rs:136:41
    |
136 |         self.condition.map_or(true, |c| c())
    |                                         ^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `pyo3@0.22.5`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e170,
                  },
                  ty: Binder { value: fn() -> impl_::pymethods::PyMethodDefType, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(152),
                  ),
                  span: src/impl_/pyclass/lazy_type_object.rs:156:40: 156:47 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn() -> impl_::pymethods::PyMethodDefType, bound_vars: [] }
   --> src/impl_/pyclass/lazy_type_object.rs:156:40
    |
156 |                         built_method = builder();
    |                                        ^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `pyo3-macros-backend@0.22.5`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e2,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), "'_") utils::Ctx) -> proc_macro2::TokenStream, bound_vars: [Region(BrNamed(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), '_))] },
                  temp_lifetime: Some(
                      Node(25),
                  ),
                  span: src/pymethod.rs:1644:9: 1644:14 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), "'_") utils::Ctx) -> proc_macro2::TokenStream, bound_vars: [Region(BrNamed(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), '_))] }
    --> src/pymethod.rs:1644:9
     |
1644 |         (gen)(ctx).to_tokens(tokens)
     |         ^^^^^
     |
     = note: ⚠️ This is a bug in Hax's frontend.
             Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `proptest@1.5.0`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e0,
                  },
                  ty: Binder { value: fn() -> T/#0, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(7),
                  ),
                  span: src/strategy/just.rs:143:9: 143:13 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn() -> T/#0, bound_vars: [] }
   --> src/strategy/just.rs:143:9
    |
143 |         self()
    |         ^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `napi@2.16.13`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e399,
                  },
                  ty: Binder { value: unsafe fn(*mut napi_sys::napi_env__) -> std::result::Result<*mut napi_sys::napi_value__, error::Error<status::Status>>, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(699),
                  ),
                  span: src/bindgen_runtime/module_register.rs:346:29: 346:37 (#0),
              }
               - ty_kind: &'{erased} Binder { value: unsafe fn(*mut napi_sys::napi_env__) -> std::result::Result<*mut napi_sys::napi_value__, error::Error<status::Status>>, bound_vars: [] }
   --> src/bindgen_runtime/module_register.rs:346:29
    |
346 |             if let Err(e) = callback(env).and_then(|v| {
    |                             ^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `winit@0.30.5`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e59,
                  },
                  ty: Binder { value: unsafe extern "C { unwind: false }" fn(*mut xkbcommon_dl::xkb_context, *const i8, xkbcommon_dl::xkb_compose_compile_flags) -> *mut xkbcommon_dl::xkb_compose_table, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(116),
                  ),
                  span: src/platform_impl/linux/common/xkb/compose.rs:33:13: 33:54 (#0),
              }
               - ty_kind: libloading::safe::Symbol<'{erased}, Binder { value: unsafe extern "C { unwind: false }" fn(*mut xkbcommon_dl::xkb_context, *const i8, xkbcommon_dl::xkb_compose_compile_flags) -> *mut xkbcommon_dl::xkb_compose_table, bound_vars: [] }>
  --> src/platform_impl/linux/common/xkb/compose.rs:33:13
   |
33 |             (XKBCH.xkb_compose_table_new_from_locale)(
   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: ⚠️ This is a bug in Hax's frontend.
           Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `tera@1.20.0`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e1147,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), "'_") str) -> std::string::String, bound_vars: [Region(BrNamed(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), '_))] },
                  temp_lifetime: Some(
                      Node(1163),
                  ),
                  span: src/renderer/processor.rs:446:26: 446:51 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), "'_") str) -> std::string::String, bound_vars: [Region(BrNamed(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), '_))] }
   --> src/renderer/processor.rs:446:26
    |
446 |                 to_value(self.tera.get_escape_fn()(res.as_str().unwrap())).map_err(Error::json)?,
    |                          ^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `wasmtime@26.0.0`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e158,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), "'_") wasmtime_environ::component::InterfaceType, &'^1.Named(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), "'_") runtime::component::matching::InstanceType<'^2.Named(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), "'_")>) -> core::result::Result<(), anyhow::Error>, bound_vars: [Region(BrNamed(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), '_)), Region(BrNamed(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), '_)), Region(BrNamed(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), '_))] },
                  temp_lifetime: Some(
                      Node(148),
                  ),
                  span: src/runtime/component/func/typed.rs:1739:17: 1739:22 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), "'_") wasmtime_environ::component::InterfaceType, &'^1.Named(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), "'_") runtime::component::matching::InstanceType<'^2.Named(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), "'_")>) -> core::result::Result<(), anyhow::Error>, bound_vars: [Region(BrNamed(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), '_)), Region(BrNamed(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), '_)), Region(BrNamed(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), '_))] }
    --> src/runtime/component/func/typed.rs:1739:17
     |
1739 |                 check(ty, types)?;
     |                 ^^^^^
     |
     = note: ⚠️ This is a bug in Hax's frontend.
             Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `async-graphql@7.0.11`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e60,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), "'_") validation::visitor::VisitorContext<'^1.Named(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), "'_")>, &'^2.Named(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), "'_") [async_graphql_parser::Positioned<async_graphql_parser::types::VariableDefinition>], &'^3.Named(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), "'_") async_graphql_parser::types::Field, usize) -> std::result::Result<usize, error::ServerError>, bound_vars: [Region(BrNamed(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), '_)), Region(BrNamed(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), '_)), Region(BrNamed(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), '_)), Region(BrNamed(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), '_))] },
                  temp_lifetime: Some(
                      Node(126),
                  ),
                  span: src/validation/visitors/complexity.rs:61:27: 61:28 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), "'_") validation::visitor::VisitorContext<'^1.Named(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), "'_")>, &'^2.Named(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), "'_") [async_graphql_parser::Positioned<async_graphql_parser::types::VariableDefinition>], &'^3.Named(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), "'_") async_graphql_parser::types::Field, usize) -> std::result::Result<usize, error::ServerError>, bound_vars: [Region(BrNamed(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), '_)), Region(BrNamed(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), '_)), Region(BrNamed(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), '_)), Region(BrNamed(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), '_))] }
  --> src/validation/visitors/complexity.rs:61:27
   |
61 |                     match f(
   |                           ^
   |
   = note: ⚠️ This is a bug in Hax's frontend.
           Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `neon@1.0.0`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e34,
                  },
                  ty: Binder { value: fn(*mut sys::bindings::types::Env__, *mut u32) -> sys::bindings::types::Status, bound_vars: [] },
                  temp_lifetime: Some(
                      Node(108),
                  ),
                  span: src/sys/bindings/functions.rs:427:16: 427:27 (#0),
              }
               - ty_kind: libloading::Symbol<'{erased}, Binder { value: fn(*mut sys::bindings::types::Env__, *mut u32) -> sys::bindings::types::Status, bound_vars: [] }>
   --> src/sys/bindings/functions.rs:427:16
    |
427 |     assert_eq!(get_version(env, &mut version as *mut _), Status::Ok,);
    |                ^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>

<details><summary>Crate `kube-runtime@0.96.0`</summary>
  
  
```
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.
              
              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e55,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), "'_") Alias(Projection, AliasTy { args: [S/#0], def_id: DefId(34:71 ~ futures_core[3a68]::stream::Stream::Item), .. })) -> bool, bound_vars: [Region(BrNamed(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), '_))] },
                  temp_lifetime: Some(
                      Node(68),
                  ),
                  span: src/utils/mod.rs:84:20: 84:46 (#0),
              }
               - ty_kind: &'{erased} mut Binder { value: fn(&'^0.Named(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), "'_") Alias(Projection, AliasTy { args: [S/#0], def_id: DefId(34:71 ~ futures_core[3a68]::stream::Stream::Item), .. })) -> bool, bound_vars: [Region(BrNamed(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), '_))] }
  --> src/utils/mod.rs:84:20
   |
84 |                 if (this.should_consume_item)(x_ref) {
   |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: ⚠️ This is a bug in Hax's frontend.
           Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!


```
</details>



Discussion / hints:

Fix patch:
diff --git a/frontend/exporter/src/types/thir.rs b/frontend/exporter/src/types/thir.rs
index 2f742adcb..381620a76 100644
--- 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),


Test patch:
diff --git a/test-harness/src/snapshots/toolchain__functions into-fstar.snap b/test-harness/src/snapshots/toolchain__functions into-fstar.snap
index 21a6f688a..df12b8b6e 100644
--- 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
index 215bd726c..e430cbdf8 100644
--- 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
index f3c4b4801..8d80d6ad1 100644
--- 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()
+    }
+}