diff --git a/changelog/1964 b/changelog/1964
new file mode 100644
index 0000000000000000000000000000000000000000..fb6d095b6d41778dfc1bda3fcf319f0f0743aeae
--- /dev/null
+++ b/changelog/1964
@@ -0,0 +1,5 @@
+author: er433
+description: ''
+merge_request: '1964'
+title: 'Monomorphisation: forall eta expand in monomorphisation'
+type: fixed
diff --git a/src/passes/13-self_ast_aggregated/monomorphisation.ml b/src/passes/13-self_ast_aggregated/monomorphisation.ml
index 17156a89e6587443bf2715edfcd7f41746094498..5664e012fda9fc777f82ee96770f13ad81681bb0 100644
--- a/src/passes/13-self_ast_aggregated/monomorphisation.ml
+++ b/src/passes/13-self_ast_aggregated/monomorphisation.ml
@@ -171,6 +171,7 @@ let rec mono_polymorphic_expression ~raise : Data.t -> AST.expression -> Data.t
       let data, result = self data result in
       data, return (E_recursive { fun_name ; fun_type ; lambda = { binder ; output_type ; result } })
    | E_let_in { let_binder ; rhs ; let_result ; attr } -> (
+      let rhs = AST.Combinators.forall_expand rhs in
       let type_vars, rhs = AST.Combinators.get_type_abstractions rhs in
       let data, let_result = self data let_result in
       let binder_instances = Data.instances_lookup (Binder.get_var let_binder) data in
diff --git a/src/stages/6-ast_aggregated/combinators.ml b/src/stages/6-ast_aggregated/combinators.ml
index f48fe314ebe519724fd0a1d239831ecb1294d6b7..13cac5fc75f0b5d49e6f67929edc78e79753468c 100644
--- a/src/stages/6-ast_aggregated/combinators.ml
+++ b/src/stages/6-ast_aggregated/combinators.ml
@@ -340,3 +340,33 @@ let get_type_abstractions (e : expression) =
   | Some { type_binder ; result } ->
      aux (type_binder :: tv) result in
   aux [] e
+
+(* This function re-builds a term prefixed with E_type_abstraction:
+   given an expression e and a list of type variables [t1; ...; tn],
+   it constructs an expression /\ t1 . ... . /\ tn . e *)
+let build_type_abstractions init =
+  let t_for_all ty_binder kind type_ = t_for_all { ty_binder ; kind ; type_ } () in
+  let f e abs_var = { e with expression_content = E_type_abstraction { type_binder = abs_var ; result = e } ;
+                             type_expression = t_for_all abs_var Type e.type_expression } in
+  List.fold_left ~init ~f
+
+(* This function re-builds a term prefixed with E_type_inst:
+   given an expression e and a list of type variables [t1; ...; tn],
+   it constructs an expression e@{t1}@...@{tn} *)
+let build_type_insts init =
+  let f av forall =
+      let Abstraction.{ ty_binder ; type_ = t ; kind = _ } = Option.value_exn @@ get_t_for_all forall.type_expression in
+      let type_ = t_variable av () in
+      (make_e (E_type_inst {forall ; type_ }) (Helpers.subst_type ty_binder type_ t)) in
+  List.fold_right ~init ~f
+
+(* This function expands a function with a type T_for_all but not with
+   the same amount of E_type_abstraction *)
+let forall_expand (e : expression) =
+  let tvs, _ = Helpers.destruct_for_alls e.type_expression in
+  let evs, e_without_type_abs = get_type_abstractions e in
+  if List.equal Ligo_prim.Type_var.equal tvs evs then
+    e
+  else
+    let e = build_type_insts e_without_type_abs tvs in
+    build_type_abstractions e tvs