diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index e2f349e6ecfad62f3a27eecc575c0477832306a3..ad972d9e986509ccf873e6c49c07d546f2acee67 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -762,7 +762,8 @@ and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
       in
       let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
       let p_quantified =
-        let loc = Some (loc :> Cil_types.location) in
+        (* [loc] prevents a type error with eta-expansion and label *)
+        let loc = Some loc in
         let call f = f ?loc (Logic_const.here_label, t') in
         match name with
         | "valid" -> call Logic_const.pvalid