# Explicitly polymorphic function inside a universally quantified record field (e.g., an effect handler)? **URL:** \ **Category:** Learning\ **Tags:** polymorphism, gadt, effects\ **Created:** [January 17, 2024, 2:09pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889 "2024-01-17T14:09:59Z")\ **Posts on this page:** 7\ **Page:** 1
**Author:** ![Zeta](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zeta/32/6003_2.png) [@Zeta](https://discuss.ocaml.org/u/Zeta)\ **Post date:** [January 17, 2024, 2:09pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/1 "2024-01-17T14:09:59Z")
How do I define an explicitly polymorphic function inside a universally quantified record field, e.g., inside an effect handler? Here is a MWE: ```ocaml open Effect open Effect.Deep type _ Effect.t += Eff : ('a -> 'a) t let rec handler = (* let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in (* <-- Does not work here... *) *) { effc = (fun (type a) (eff : a t) -> (* let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in (* <-- ...nor here *) *) match eff with | Eff -> Some (fun (k : (a, _) continuation) -> continue k tricky) | _ -> None); } (* But the following works: *) and tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler let comp () = let id = perform Eff in id () let () = try_with comp () handler ``` With `tricky` inside the record field, I get an error ```auto 10 | let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler in ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: This definition has type 'b -> 'b which is less general than 'b0. 'b0 -> 'b0 ``` but when I take it out of the `handler` definition, the code type-checks. I also tried wrapping `tricky` as a universally quantified object method, but it didn’t work as well. My guess is that there is a problem unifying a monomorphized(?) `tricky` inside `continue k tricky` with the explicitly polymorphic definition inside `handler`. 1. What is the exact cause of the issue of defining `tricky` inside `handler`? I read [Chapter 6](https://v2.ocaml.org/manual/polymorphism.html) and [Chapter 7](https://v2.ocaml.org/manual/gadts-tutorial.html) of the OCaml manual multiple times without much success. 2. Is my workaround the best solution? Is there a way to put `tricky` in `handler` and satisfy the type-checker? Thank you. ---
**Author:** ![vlaviron](https://avatars.discourse-cdn.com/v4/letter/v/ec9cab/32.png) [@vlaviron](https://discuss.ocaml.org/u/vlaviron)\ **Post date:** [January 17, 2024, 2:26pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/2 "2024-01-17T14:26:11Z")
I suspect that the issue is that `handler` has a non-polymorphic type inside its own definition, but a polymorphic one outside. Can you try adding an annotation `let rec handler : 'a . 'a effect_handler` and see if it changes anything ? ---
**Author:** ![SkySkimmer](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/skyskimmer/32/1672_2.png) [@SkySkimmer](https://discuss.ocaml.org/u/SkySkimmer)\ **Post date:** [January 17, 2024, 2:32pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/3 "2024-01-17T14:32:26Z")
> [@Zeta](#): > > `type _ Effect.t += Eff : ('a -> 'a) t` This is not an effect returning a polymorphic function, it’s an effect returning a monomorphic function at an existential type. Maybe you want ```auto type poly_fun = { f : 'a. 'a -> 'a } type _ Effect.t += Eff : poly_fun t ``` ? IDK if that helps your compilation issues. ---
**Author:** ![Zeta](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zeta/32/6003_2.png) [@Zeta](https://discuss.ocaml.org/u/Zeta)\ **Post date:** [January 17, 2024, 2:44pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/4 "2024-01-17T14:44:29Z")
Yes, it works like charm! So a value needs to be explicitly polymorphic in order to have some other polymorphic value type-check… ---
**Author:** ![Zeta](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zeta/32/6003_2.png) [@Zeta](https://discuss.ocaml.org/u/Zeta)\ **Post date:** [January 17, 2024, 2:47pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/5 "2024-01-17T14:47:58Z")
Thank you for correcting that `type _ Effect.t += Eff : ('a -> 'a) t` is not a function returning a polymorphic function, you are correct indeed! ---
**Author:** ![Zeta](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zeta/32/6003_2.png) [@Zeta](https://discuss.ocaml.org/u/Zeta)\ **Post date:** [January 17, 2024, 2:49pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/6 "2024-01-17T14:49:03Z")
So here is the correct code reflecting the comments from @vlaviron and @SkySkimmer: ```ocaml open Effect open Effect.Deep type poly_fun = { f : 'a. 'a -> 'a } type _ Effect.t += Eff : poly_fun t let rec handler : 'a. 'a effect_handler = { effc = (fun (type a) (eff : a t) -> match eff with | Eff -> Some (fun (k : (a, _) continuation) -> continue k { f = (fun v -> try_with Fun.id v handler) }) | _ -> None); } let comp () = let id = perform Eff in id.f () let () = try_with comp () handler ``` Thanks again! ---
**Author:** ![vlaviron](https://avatars.discourse-cdn.com/v4/letter/v/ec9cab/32.png) [@vlaviron](https://discuss.ocaml.org/u/vlaviron)\ **Post date:** [January 17, 2024, 2:58pm UTC](https://discuss.ocaml.org/t/explicitly-polymorphic-function-inside-a-universally-quantified-record-field-e-g-an-effect-handler/13889/7 "2024-01-17T14:58:04Z")
In this case, the definition of `tricky` depends on `handler`: ```ocaml let tricky : 'b. 'b -> 'b = fun v -> try_with Fun.id v handler ``` If you assume that `handler` has type `alpha effect_handler` for some `alpha`, then `tricky` has type `alpha -> alpha`. You cannot generalize this to a fully polymorphic type because the `alpha` comes from outside the definition of `tricky`. This is more or less what happens if you let the type-checker infer the type of `handler`. But if you know that `handler` has type `'a. 'a effect_handler`, then the definition of `tricky` gets a type that is still something like `alpha -> alpha`, but with an `alpha` that was created during type inference of `tricky`, so it can be generalized to `'b. 'b -> 'b`. I think that the section of the manual on polymorphic recursion ([here](https://v2.ocaml.org/manual/polymorphism.html#s%3Apolymorphic-recursion)) is the most relevant to your case, although this is the first time I’ve seen a need for polymorphic recursion annotations on non-functional values.