# GADT and polymorphic recursion

**URL:** <https://discuss.ocaml.org/t/gadt-and-polymorphic-recursion/9183>\
**Category:** Learning\
**Tags:** polymorphism, gadt\
**Created:** [January 19, 2022, 2:56pm UTC](https://discuss.ocaml.org/t/gadt-and-polymorphic-recursion/9183 "2022-01-19T14:56:46Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Kakadu](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/kakadu/32/1204_2.png) [@Kakadu](https://discuss.ocaml.org/u/Kakadu)\
**Post date:** [January 19, 2022, 2:56pm UTC](https://discuss.ocaml.org/t/gadt-and-polymorphic-recursion/9183/1 "2022-01-19T14:56:46Z")

</div>

I’m writing some code about OCaml’s typedtree, my current result is too long and complex, and _I want to make it better_.

Right now I have solutions that use 1) locally abstract types, and 2) non-prenex polymorphism via record, or 2) open recursion. Is it possible to abandon records for non-prenex polymorphism?

This one has all three features:

```ocaml
  (* OCaml 3.12.1 *)
  open Typedtree
  type ttt = { self : 'a . 'a pattern_desc pattern_data -> bool}

  (* Kind of what I want but long *)
  let _hack =
    let helper (type a)
        (self : ttt)
        (p1: a Typedtree.pattern_desc pattern_data) =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all self.self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all self.self a1
      | Tpat_value v1 ->
          self.self
            (v1 :> Typedtree.pattern)
      | Tpat_exception _
      | _ -> false
    in
    let rec ans = { self = (fun eta -> helper ans eta) } in
    ans

```

If I abondon only open recursion it compiles too:

```ocaml
  let _hack_no_open_recursion =
    let rec helper = { self = (fun (type a) (p1: a Typedtree.pattern_desc pattern_data) ->
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all helper.self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all helper.self a1
      | Tpat_value v1 ->
          helper.self
            (v1 :> Typedtree.pattern)
      | Tpat_exception _
      | _ -> false
    )}
    in
    helper

```

If I abandone non-prenex polymorphism and open recursion, I would get a wrong type

```ocaml
  (* `value general_pattern -> bool` Not what I want *)
  let rec _hack_bad2 (type a) (p1: a Typedtree.pattern_desc pattern_data) =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all _hack_bad2 t1
      | Tpat_construct (_, cd1, a1) -> List.for_all _hack_bad2 a1
      | Tpat_value v1 ->
          _hack_bad2
            (v1 :> value Typedtree.pattern_desc Typedtree.pattern_data) 
      | Tpat_exception _
      | _ -> false

```

And when I abondon only non-prenex polymorphism I get compilation error

```ocaml
  let _hack_bad =
    let helper (type a)
        (self : a pattern_desc pattern_data -> bool)
        (p1: a Typedtree.pattern_desc pattern_data) =
      match p1.pat_desc with
      | Tpat_any
      | Tpat_var _ -> true
      | Tpat_constant c1 -> true
      | Tpat_tuple t1 -> List.for_all self t1
      | Tpat_construct (_, cd1, a1) -> List.for_all self a1
      | Tpat_value v1 ->
          self
            (v1 :> value Typedtree.pattern_desc Typedtree.pattern_data)
          (*
          Error: This expression has type value Typedtree.pattern_desc pattern_data
                but an expression was expected of type
                  a Typedtree.pattern_desc pattern_data
                Type value is not compatible with type a
          *)
      | Tpat_exception _
      | _ -> false
    in
    let rec ans eta = helper ans eta in
    ans

```

---

<div class="post-metadata">

**Author:** ![thierry-martinez](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/thierry-martinez/32/1481_2.png) [@thierry-martinez](https://discuss.ocaml.org/u/thierry-martinez)\
**Post date:** [January 19, 2022, 3:14pm UTC](https://discuss.ocaml.org/t/gadt-and-polymorphic-recursion/9183/2 "2022-01-19T15:14:29Z")

</div>

You may use the [polymorphic syntax for locally abstract type](https://ocaml.org/manual/locallyabstract.html#p:polymorpic-locally-abstract), which allows you to use polymorphic recursion directly.

```auto
let rec check : type a . a pattern_desc pattern_data -> bool = fun p1 ->
  match p1.pat_desc with
  | Tpat_any
  | Tpat_var _ -> true
  | Tpat_constant _c1 -> true
  | Tpat_tuple t1 -> List.for_all check t1
  | Tpat_construct (_, _cd1, a1) -> List.for_all check a1
  | Tpat_value v1 ->
      check (v1 :> Typedtree.pattern)
  | Tpat_exception _
  | _ -> false

```