title: Existential types for inline record constructors with constraints
body: <p>I'm trying to represent a set of productions of a grammar in OCaml and existential types would be very useful to model the semantic actions of grammar rules. I've been looking into Menhir source code and existential types are also used to model the semantic actions. Consider the following:</p>
  
  <pre><code>type 'a 'b production = { name: string; rule: 'a expr; action: 'a -&gt; 'b }
  </code></pre>
  
  <p>A production has a name, a rule that returns <code>'a</code> and an action that receives <code>'a</code> and returns <code>'b</code>. The problem with simple parametric types is that a list of productions could not be polymorphic at all, so I can have an action of <code>string_of_float</code> and another of <code>string_of_int</code> in the same list; which is a common issue that can be solved with explicit <code>Ɐ</code>, for example, action could be:</p>
  
  <pre><code>action: 'a 'b. 'a -&gt; 'b
  </code></pre>
  
  <p>But I also need to have a constraint based on the parameter of <code>expr</code>, where <code>'a</code> of <code>action</code> unifies to <code>'a</code> of <code>expr</code>, so, as long as we can have inline record constructors in algebraic data types, we should be able to have them in generalized algebraic data types too, right?</p>
  
  <pre><code>type production = (* Ɐ a. b. *)
    | Production: { name: string; rule: 'a expr; action: 'a -&gt; 'b } -&gt; production
  </code></pre>
  
  <p>But this is not a valid form. The solution I found for now is making the rule also have the action type, for example:</p>
  
  <pre><code>type 'a expr =
    | Terminal of string * ('a -&gt; 'a)
    | Sequence of 'a expr list * ('a list -&gt; 'a)
  </code></pre>
  
  <p>But this kind of monomorphism is still very restrictive. How can I model existential types inside records with shared constraints, so I could have different return types in different productions where a compile-time checking of application is still possible (via exhaustive pattern-matching)?</p>
  
  <p>Using the same logic, If I'd like to have a list of functions from <code>'a 'b. -&gt; 'a -&gt; 'b</code>, would I need to use an existential type constructor to do that (like in <code>[string_of_int; string_of_float]</code>)?</p>
  
  <p>I believe I need some sort of kind restriction (they both are <code>* -&gt; *</code>), but I came from Haskell and still didn't figure out how to do that in OCaml.</p>