There is no simple way to solve any of these questions, so I don't expect the OCaml language to improve on your example on the short/medium term. After thinking of these issues a bit more, I would personally support adding a notion of "pure arrow" ('a => 'b), giving your interface the type
( **> ) : 'c => ('a, 'b) hlist => ('c -> 'a, 'b) hlist
which would make any term built solely of ( **> ) and empty (and Empty and Cons) generalizable. However, this feature would be very limited in scope (due to the inherent difficulty of tracking effect) and suitable generalization require advanced type system features (effect systems, for example as found in Koka or F*). I think a minimal, advanced-uses-only feature (just a separation of pure and impure arrow) would already be a nice feature to have (also for functors), but there is no clear consensus on the question.