Your problem starts with this definition
that makes the type of elements existentially quantified. Notice in particular, that the first parameter of the type constructor is never specified: it is a is phantom type parameter. Consequently a value of type (_, 'nat) t is a list of elements of unknown types with length equal to the integer represented by 'nat.
Since the type of the elements of the list is unknown (and can never be recovered), elements of the list can only be manipulated by polymorphic functions which is not what you wanted.
The solution is thus to avoid hiding type information by introducing existential types. This means that the types of the elements of the list must be reflected in the type of the lists. If we remove the peano encoding of the list length, your first definition can be simplified to
type void = |
type 'a hlist =
| []: void hlist
| (::): 'a * 'b hlist -> ?? hlist
The important point is then that the type of the hlist constructed by (::) needs to keep track of both the type of the inner list and the type of the first element.
The simpler solution is thus to concatenate the two types with *:
type 'a hlist =
| [ ]: void hlist
| (::): 'a * 'b hlist -> ('a * 'b) hlist
(which is unsurprisingly building a list of types at the type level).